summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Test/livevars/Answer4
-rw-r--r--Test/livevars/NestedOneDimensionalMap.bpl29
-rw-r--r--Test/livevars/TwoDimensionalMap.bpl29
-rw-r--r--Test/livevars/runtest.bat3
4 files changed, 64 insertions, 1 deletions
diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index 1a0327f6..958fc852 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -411,3 +411,7 @@ Execution trace:
stack_overflow.bpl(97935,3): inline$storm_thread_completion$0$Return#1
Boogie program verifier finished with 0 verified, 1 error
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/livevars/NestedOneDimensionalMap.bpl b/Test/livevars/NestedOneDimensionalMap.bpl
new file mode 100644
index 00000000..411316ac
--- /dev/null
+++ b/Test/livevars/NestedOneDimensionalMap.bpl
@@ -0,0 +1,29 @@
+var k: int;
+var AllMaps__1: [int][int]int;
+
+procedure PoirotMain.Main_trace_1_trace_1()
+modifies k, AllMaps__1;
+{
+ var $tmp4: int;
+ var local_0: int;
+
+ lab0:
+ k := 1;
+ goto lab1, lab2;
+
+
+lab1:
+ assume k == 0;
+ goto lab3;
+
+lab2:
+ assume k == 1;
+ $tmp4 := local_0;
+ goto lab3;
+
+lab3:
+ AllMaps__1[$tmp4][0] := 1;
+ assert AllMaps__1[local_0][0] == 1;
+}
+
+
diff --git a/Test/livevars/TwoDimensionalMap.bpl b/Test/livevars/TwoDimensionalMap.bpl
new file mode 100644
index 00000000..25e24b23
--- /dev/null
+++ b/Test/livevars/TwoDimensionalMap.bpl
@@ -0,0 +1,29 @@
+var k: int;
+var AllMaps__1: [int,int]int;
+
+procedure PoirotMain.Main_trace_1_trace_1()
+modifies k, AllMaps__1;
+{
+ var $tmp4: int;
+ var local_0: int;
+
+ lab0:
+ k := 1;
+ goto lab1, lab2;
+
+
+lab1:
+ assume k == 0;
+ goto lab3;
+
+lab2:
+ assume k == 1;
+ $tmp4 := local_0;
+ goto lab3;
+
+lab3:
+ AllMaps__1[$tmp4,0] := 1;
+ assert AllMaps__1[local_0,0] == 1;
+}
+
+
diff --git a/Test/livevars/runtest.bat b/Test/livevars/runtest.bat
index 3269a354..dbd3cb8c 100644
--- a/Test/livevars/runtest.bat
+++ b/Test/livevars/runtest.bat
@@ -8,4 +8,5 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
%BGEXE% %* /noinfer /useArrayTheory daytona_bug2_ioctl_example_1.bpl
%BGEXE% %* /noinfer /useArrayTheory daytona_bug2_ioctl_example_2.bpl
%BGEXE% %* /noinfer /useArrayTheory stack_overflow.bpl
-
+%BGEXE% %* /noinfer /useArrayTheory NestedOneDimensionalMap.bpl
+%BGEXE% %* /noinfer /useArrayTheory TwoDimensionalMap.bpl