summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/AbsInt/IntervalDomain.cs2
-rw-r--r--Test/aitest0/Answer7
-rw-r--r--Test/aitest0/Intervals.bpl18
3 files changed, 25 insertions, 2 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 3d83bb5c..be62eb58 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -667,7 +667,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
Lo = 1 - hi;
}
if (lo != null) {
- Hi = -lo;
+ Hi = 1 - lo;
}
}
else if (op.Op == UnaryOperator.Opcode.Not) {
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 18359b2e..dabe9710 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -119,5 +119,10 @@ Execution trace:
Intervals.bpl(68,5): anon0
Intervals.bpl(69,3): anon3_LoopHead
Intervals.bpl(69,3): anon3_LoopDone
+Intervals.bpl(92,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(87,5): anon0
+ Intervals.bpl(88,3): loop_head
+ Intervals.bpl(91,3): after_loop
-Boogie program verifier finished with 4 verified, 2 errors
+Boogie program verifier finished with 5 verified, 3 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 7ed2c3d2..4520a032 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -73,3 +73,21 @@ procedure Thresholds4()
assert i * 2 == 400; // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200
}
+procedure UnaryNegation0() returns (x: int) // this was once buggy
+{
+ x := -1;
+ loop_head:
+ x := x;
+ goto loop_head, after_loop;
+ after_loop:
+ assert x == -1;
+}
+procedure UnaryNegation1() returns (x: int) // this was once buggy
+{
+ x := -1;
+ loop_head:
+ x := x;
+ goto loop_head, after_loop;
+ after_loop:
+ assert x == 1; // error
+}