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/NestedOneDimensionalMap.bpl | |
| parent | 7d68816537f6eca458636a5bfbef1e08844f61fe (diff) | |
added more regressions to livevars
Diffstat (limited to 'Test/livevars/NestedOneDimensionalMap.bpl')
| -rw-r--r-- | Test/livevars/NestedOneDimensionalMap.bpl | 29 |
1 files changed, 29 insertions, 0 deletions
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;
+}
+
+
|