diff options
| author |  qadeer <unknown> | 2013-09-04 15:07:23 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-09-04 15:07:23 -0700 |
| commit | b06cff3aa1491d0b2e5885a6e801c1d924af2e11 (patch) | |
| tree | 701f467991d936fdf164e37b98e67fd58f162dc7 /Test | |
| parent | 0ce0ad111d6454475f47b56a6315b6134b869400 (diff) | |
fixed the linear type checking related to globals
fixed the modset analysis so that it infers the stable predicate also
added more information to type error messages
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/linear/Answer | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/Test/linear/Answer b/Test/linear/Answer index e6df2e87..9ba244e5 100644 --- a/Test/linear/Answer +++ b/Test/linear/Answer @@ -1,22 +1,23 @@ -------------------- typecheck.bpl --------------------
-typecheck.bpl(6,22): Error: a linear domain must be consistently attached to variables of a particular type
+typecheck.bpl(6,22): Error: Linear domain A must be consistently attached to variables of one type
typecheck.bpl(18,22): Error: a linear domain can be attached to either a set or a scalar type
-typecheck.bpl(31,9): Error: Only simple assignment allowed on linear sets
-typecheck.bpl(33,6): Error: Only variable can be assigned to a linear variable
-typecheck.bpl(35,6): Error: Only linear variable can be assigned to another linear variable
-typecheck.bpl(39,6): Error: Variable of one domain being assigned to a variable of another domain
-typecheck.bpl(45,9): Error: A linear variable can occur only once in the rhs
-typecheck.bpl(49,4): Error: A linear set can occur only once as an in parameter
-typecheck.bpl(51,4): Error: Only variable can be assigned to a linear variable
+typecheck.bpl(31,9): Error: Only simple assignment allowed on linear variable b
+typecheck.bpl(33,6): Error: Only variable can be assigned to linear variable a
+typecheck.bpl(35,6): Error: Only linear variable can be assigned to linear variable a
+typecheck.bpl(39,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D
+typecheck.bpl(45,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
+typecheck.bpl(49,4): Error: Linear variable a can occur only once as an input parameter
+typecheck.bpl(51,4): Error: Only variable can be passed to linear parameter b
typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same
typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same
-typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter
-typecheck.bpl(61,4): Error: A linear set can occur only once as an in parameter
-typecheck.bpl(66,6): Error: output variable must be available at a return
-typecheck.bpl(75,4): Error: Linear global variable cannot be read from
-typecheck.bpl(81,4): Error: Linear global variable cannot be written to
-16 type checking errors detected in typecheck.bpl
+typecheck.bpl(57,4): Error: Only a linear argument can be passed to linear parameter a
+typecheck.bpl(61,4): Error: Linear variable a can occur only once as an input parameter
+typecheck.bpl(66,6): Error: Output variable d must be available at a return
+typecheck.bpl(75,4): Error: Global variable g must be available at a return
+typecheck.bpl(81,7): Error: unavailable source for a linear read
+typecheck.bpl(81,4): Error: Output variable r must be available at a return
+17 type checking errors detected in typecheck.bpl
-------------------- list.bpl --------------------
|