diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-23 12:07:20 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-23 12:07:20 -0800 |
| commit | c5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (patch) | |
| tree | 9336173498839860956d21178bbf622d1bc22e77 /Test/test20 | |
| parent | c7f74de7fae661883ca13bb09d557272de659e03 (diff) | |
removed call forall and * args to calls
Diffstat (limited to 'Test/test20')
| -rw-r--r-- | Test/test20/Answer | 3 | ||||
| -rw-r--r-- | Test/test20/PolyProcs0.bpl | 11 |
2 files changed, 1 insertions, 13 deletions
diff --git a/Test/test20/Answer b/Test/test20/Answer index fa33507e..5e4481ca 100644 --- a/Test/test20/Answer +++ b/Test/test20/Answer @@ -55,8 +55,7 @@ PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)
PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
-PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)
-7 type checking errors detected in PolyProcs0.bpl
+6 type checking errors detected in PolyProcs0.bpl
TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl index 609f1167..06d4206c 100644 --- a/Test/test20/PolyProcs0.bpl +++ b/Test/test20/PolyProcs0.bpl @@ -30,15 +30,4 @@ procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Fi requires obj0 != obj1;
ensures heap[obj0, f] != heap[obj1, f];
-procedure testCallForall(heap : <a>[ref, Field a]a) {
- var f1 : Field int; var f2 : Field bool;
-
- start:
- call forall injective(heap, *, *, f1);
- call forall injective(heap, *, *, f2);
- call forall injective(heap, *, *, *);
-
- call forall injective(heap, *, f1, *); // error: wrong argument type
-}
-
type ref;
|