diff options
| author |  stefanheule <unknown> | 2012-06-03 21:07:00 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-06-03 21:07:00 +0200 |
| commit | d98e8dd279357cb3789ff679a21273170ee3823f (patch) | |
| tree | 0e28f093586c67b2f9dc3f472a7a02194d28bda4 /Chalice | |
| parent | d8b33fa2c014cc881e02192e56252648663b0ed0 (diff) | |
Chalice: Add regression test case for disallowed 'waitlevel' in predicates.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10222.chalice | 8 | ||||
| -rw-r--r-- | Chalice/tests/regressions/workitem-10222.output.txt | 4 |
2 files changed, 12 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/workitem-10222.chalice b/Chalice/tests/regressions/workitem-10222.chalice new file mode 100644 index 00000000..a01253c9 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10222.chalice @@ -0,0 +1,8 @@ +class Test { + var t: Test; + + // previously, mentioning "waitlevel" in a predicate did not cause an error + predicate inv { + acc(t) && acc(t.mu) && t.mu << waitlevel + } +} diff --git a/Chalice/tests/regressions/workitem-10222.output.txt b/Chalice/tests/regressions/workitem-10222.output.txt new file mode 100644 index 00000000..eac18363 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10222.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10222.chalice using parameters=""
+
+The program did not typecheck.
+6.9: predicate body is not allowed to mention 'waitlevel'
|