diff options
| author |  schaef <unknown> | 2009-11-20 09:24:55 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2009-11-20 09:24:55 +0000 |
| commit | 1ea222005d9d4722457f70cbd771fde5eed4d76f (patch) | |
| tree | ed216de603d9ae0f5664d91775e7a684492a448a | |
| parent | 97c46034da2f75ee0ee081ab2782260ac27ea04f (diff) | |
| -rw-r--r-- | Source/VCGeneration/DoomCheck.ssc | 6 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 11 |
2 files changed, 14 insertions, 3 deletions
diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc index cdbdcb6a..ecefedea 100644 --- a/Source/VCGeneration/DoomCheck.ssc +++ b/Source/VCGeneration/DoomCheck.ssc @@ -313,7 +313,7 @@ namespace VC ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Blue;
- Console.WriteLine("Assert false was detected, but ignored");
+ Console.WriteLine("Assert false or PossiblyUnreachable was detected, but ignored");
Console.ForegroundColor = col;
currentNode.HasBeenChecked = true;
@@ -365,12 +365,12 @@ namespace VC }
return false;
}
-
+
private bool BlockContainsAssertFalse(Block! b) {
foreach (Cmd! c in b.Cmds) {
AssertCmd ac = c as AssertCmd;
if (ac!=null) {
- if (IsFalse(ac.Expr) ) {
+ if (IsFalse(ac.Expr) || QKeyValue.FindBoolAttribute(ac.Attributes, "PossiblyUnreachable") ) {
return true;
}
}
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl index 86bf76d1..eb60536f 100644 --- a/Test/doomed/notdoomed.bpl +++ b/Test/doomed/notdoomed.bpl @@ -23,6 +23,17 @@ procedure b(x:int) }
+procedure c(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ assert {:PossiblyUnreachable} false;
+ }
+}
|