summaryrefslogtreecommitdiff
path: root/Test/test1/Answer
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-23 12:07:20 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-23 12:07:20 -0800
commitc5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (patch)
tree9336173498839860956d21178bbf622d1bc22e77 /Test/test1/Answer
parentc7f74de7fae661883ca13bb09d557272de659e03 (diff)
removed call forall and * args to calls
Diffstat (limited to 'Test/test1/Answer')
-rw-r--r--Test/test1/Answer10
1 files changed, 3 insertions, 7 deletions
diff --git a/Test/test1/Answer b/Test/test1/Answer
index 94bf2d9a..70b7ea80 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -107,8 +107,6 @@ UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type
UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)
UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)
12 type checking errors detected in UpdateExprTyping.bpl
-CallForallResolve.bpl(15,2): Error: call forall is allowed only on procedures with no modifies clause: Q
-1 type checking errors detected in CallForallResolve.bpl
MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m
MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)
MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)
@@ -127,10 +125,8 @@ MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot
15 type checking errors detected in MapsTypeErrors.bpl
Orderings.bpl(6,19): Error: parent of constant has incompatible type (int instead of C)
1 type checking errors detected in Orderings.bpl
-EmptyCallArgs.bpl(15,17): Error: invalid type for argument 0 in call to P: int (expected: bool)
-EmptyCallArgs.bpl(26,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
-EmptyCallArgs.bpl(28,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
-3 type checking errors detected in EmptyCallArgs.bpl
+EmptyCallArgs.bpl(19,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
+1 type checking errors detected in EmptyCallArgs.bpl
FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)
FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)
FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)
@@ -163,4 +159,4 @@ IntReal.bpl(32,6): Error: argument type int does not match expected type real
IntReal.bpl(33,6): Error: argument type real does not match expected type int
IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div
IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod
-18 type checking errors detected in IntReal.bpl \ No newline at end of file
+18 type checking errors detected in IntReal.bpl