From c5c2c9465a53e4b35a20ad5efe73882dc6a5af34 Mon Sep 17 00:00:00 2001 From: Unknown Date: Sat, 23 Feb 2013 12:07:20 -0800 Subject: removed call forall and * args to calls --- Test/test20/Answer | 3 +-- Test/test20/PolyProcs0.bpl | 11 ----------- 2 files changed, 1 insertion(+), 13 deletions(-) (limited to 'Test/test20') 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(heap : [ref, Field a]a, obj0 : ref, obj1 : ref, f : Fi requires obj0 != obj1; ensures heap[obj0, f] != heap[obj1, f]; -procedure testCallForall(heap : [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; -- cgit v1.2.3