diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:16:02 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:16:02 -0700 |
| commit | 19c70cd0d7a65c46bcaafa66b13bde43316bc081 (patch) | |
| tree | ec00ed370707ec35e818bdaacf45924b4dfaf9c8 /Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect | |
| parent | dd4f127f36ec24fbcedaaae0e61e0894b2bf5e83 (diff) | |
Add tests for quantifier splitting and trigger generation
Diffstat (limited to 'Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect')
| -rw-r--r-- | Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect new file mode 100644 index 00000000..c8e1a5fa --- /dev/null +++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect @@ -0,0 +1,32 @@ +splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y > 0}:
+ (!) No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y < 0}:
+ (!) No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y > 0}:
+ (!) No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y < 0}:
+ (!) No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location
+Execution trace:
+ (0,0): anon0
+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,25): Related location
+Execution trace:
+ (0,0): anon0
+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+
+Dafny program verifier finished with 4 verified, 4 errors
|