diff options
| author |  schaef <unknown> | 2009-11-18 15:23:19 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2009-11-18 15:23:19 +0000 |
| commit | 62069bee7147d2f5ef620c0309ef1048ca95d0a7 (patch) | |
| tree | b0bff0f8f8e789d0f2b24588cf14255b0e46fe78 /Test/doomed/doomed.bpl | |
| parent | d64c97865ea76d67e0c9a0590a9a3b26bba10c9e (diff) | |
modified the doom checking. It is now able to report only the relevant statements and writes them the stdout. Line numbers are only displayed for bpl input.
Diffstat (limited to 'Test/doomed/doomed.bpl')
| -rw-r--r-- | Test/doomed/doomed.bpl | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl new file mode 100644 index 00000000..a153e468 --- /dev/null +++ b/Test/doomed/doomed.bpl @@ -0,0 +1,27 @@ +
+procedure a(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+procedure b(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+ assert y!=2;
+}
+
+
|