summaryrefslogtreecommitdiff
path: root/Test/doomed
diff options
context:
space:
mode:
authorGravatar schaef <unknown>2010-01-28 15:56:09 +0000
committerGravatar schaef <unknown>2010-01-28 15:56:09 +0000
commit2638d7607aa02c36c0ec6a5228049c643b3696e3 (patch)
tree54b3a58ce7de7ae89c7f01da319bafd790d61b32 /Test/doomed
parent623893309558450f7ecca692ef0bb6af69df9e3d (diff)
Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebug.bpl
Diffstat (limited to 'Test/doomed')
-rw-r--r--Test/doomed/doomdebug.bpl44
1 files changed, 44 insertions, 0 deletions
diff --git a/Test/doomed/doomdebug.bpl b/Test/doomed/doomdebug.bpl
new file mode 100644
index 00000000..0f45c13c
--- /dev/null
+++ b/Test/doomed/doomdebug.bpl
@@ -0,0 +1,44 @@
+procedure badtrace(x:int, y:int, z:int)
+{
+ var xin : int;
+ xin := x+z;
+
+
+ if (y>5) {
+ xin:=5;
+ } else {
+ assert xin != x;
+ }
+}
+
+procedure baddiamond(x:int, y:int, z:int)
+{
+ var xin : int;
+ var yin : int;
+ var zin : int;
+ xin := x;
+ yin := y;
+ zin := z;
+
+ if (y<5) {
+ xin := xin -3;
+ } else {
+ zin := zin +10;
+ xin := 0;
+ }
+
+ if (x<100) {
+ yin := 3;
+ } else {
+ zin := 5;
+ }
+
+ if (z>5) {
+ yin := yin - 2;
+ xin := xin + 3;
+ }
+
+ zin:=zin+yin;
+
+ assert xin!=x;
+}