diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-06-14 09:57:07 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-06-14 09:57:07 -0700 |
| commit | ebd1d66fbc01cfb942463223c138135cc53a038b (patch) | |
| tree | 225ab9f270a2493ba7b91eff8f27032a86dacdcb /Test/livevars | |
| parent | 7d68816537f6eca458636a5bfbef1e08844f61fe (diff) | |
added more regressions to livevars
Diffstat (limited to 'Test/livevars')
| -rw-r--r-- | Test/livevars/Answer | 4 | ||||
| -rw-r--r-- | Test/livevars/NestedOneDimensionalMap.bpl | 29 | ||||
| -rw-r--r-- | Test/livevars/TwoDimensionalMap.bpl | 29 | ||||
| -rw-r--r-- | Test/livevars/runtest.bat | 3 |
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
|