diff options
| author |  stefanheule <unknown> | 2012-02-25 03:43:44 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:43:44 -0800 |
| commit | ab61f647466f3cdc049041aa7d8f18968756a099 (patch) | |
| tree | 306de0f5e8aee61e52f56f536e065aa838813138 /Chalice/tests/predicates | |
| parent | 42db923e160097a3e99c4adcb406925d3685035d (diff) | |
Chalice: add missing reference files for two tests.
Diffstat (limited to 'Chalice/tests/predicates')
| -rw-r--r-- | Chalice/tests/predicates/aux-info.output.txt | 5 | ||||
| -rw-r--r-- | Chalice/tests/predicates/mutual-dependence.output.txt | 5 |
2 files changed, 10 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/aux-info.output.txt b/Chalice/tests/predicates/aux-info.output.txt new file mode 100644 index 00000000..97794a51 --- /dev/null +++ b/Chalice/tests/predicates/aux-info.output.txt @@ -0,0 +1,5 @@ +Verification of aux-info.chalice using parameters=""
+
+ 21.5: Assertion might not hold. The expression at 21.12 might not evaluate to true. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/predicates/mutual-dependence.output.txt b/Chalice/tests/predicates/mutual-dependence.output.txt new file mode 100644 index 00000000..a35556a9 --- /dev/null +++ b/Chalice/tests/predicates/mutual-dependence.output.txt @@ -0,0 +1,5 @@ +Verification of mutual-dependence.chalice using parameters=""
+
+ 16.5: Assertion might not hold. The expression at 16.12 might not evaluate to true. + +Boogie program verifier finished with 1 errors and 0 smoke test warnings.
|