diff options
| author |  akashlal <unknown> | 2013-05-27 12:33:41 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-05-27 12:33:41 +0530 |
| commit | 2dd2705130709f633325fef6a8813df24817da1b (patch) | |
| tree | ac98fd13ffe13ece362dc46bb9e7c021497be962 /Test | |
| parent | e6241dfdc9743cbbf3f1ae9fb61f3e3179a417f9 (diff) | |
| parent | 0b5af50545d93128256acabcd09ec09996f495f6 (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/AbsHoudini/Answer | 48 | ||||
| -rw-r--r-- | Test/AbsHoudini/pred5.bpl | 24 | ||||
| -rw-r--r-- | Test/AbsHoudini/quant1.bpl | 7 | ||||
| -rw-r--r-- | Test/AbsHoudini/quant2.bpl | 24 | ||||
| -rw-r--r-- | Test/AbsHoudini/quant3.bpl | 7 | ||||
| -rw-r--r-- | Test/AbsHoudini/quant4.bpl | 7 | ||||
| -rw-r--r-- | Test/AbsHoudini/quant5.bpl | 11 | ||||
| -rw-r--r-- | Test/AbsHoudini/runtest.bat | 8 |
8 files changed, 135 insertions, 1 deletions
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index 58da416e..db2f6631 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -439,3 +439,51 @@ function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : boo }
Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred5.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant1.bpl --------------------
+function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
+{
+ x >= 0 && x <= 2
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant2.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+ x >= 0 && x <= 1
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant3.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+ x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant4.bpl --------------------
+function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
+{
+ true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant5.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+ x >= 5 && x <= 5
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl new file mode 100644 index 00000000..6940e820 --- /dev/null +++ b/Test/AbsHoudini/pred5.bpl @@ -0,0 +1,24 @@ +function {:existential true} b1(x: bool) : bool;
+
+procedure main()
+{
+ var i: int;
+ var x: int;
+ var arr: [int] int;
+
+ i := 0;
+
+ while(*)
+ invariant b1((i >= 0) && (forall j: int :: (0 <= j && j < i) ==> arr[j] == 0));
+ {
+ havoc x;
+ assume x == 0;
+
+ arr[i] := x;
+ i := i + 1;
+ }
+
+ havoc x;
+ assume x >= 0 && x < i;
+ assert b1(arr[x] == 0);
+}
diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl new file mode 100644 index 00000000..e12525b6 --- /dev/null +++ b/Test/AbsHoudini/quant1.bpl @@ -0,0 +1,7 @@ +function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;
+
+procedure foo ()
+{
+ assert (forall x: int :: (0 <= x && x <= 2) ==> b1(x));
+}
+
diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl new file mode 100644 index 00000000..5a491877 --- /dev/null +++ b/Test/AbsHoudini/quant2.bpl @@ -0,0 +1,24 @@ +function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
+
+procedure main()
+{
+ var i: int;
+ var x: int;
+ var arr: [int] int;
+
+ i := 0;
+
+ while(*)
+ invariant (i >= 0) && (forall j: int :: (0 <= j && j < i) ==> b1(arr[j]));
+ {
+ havoc x;
+ assume x == 0 || x == 1;
+
+ arr[i] := x;
+ i := i + 1;
+ }
+
+ havoc x;
+ assume x >= 0 && x < i;
+ assert arr[x] == 0 || arr[x] == 1;
+}
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl new file mode 100644 index 00000000..cc0ef79e --- /dev/null +++ b/Test/AbsHoudini/quant3.bpl @@ -0,0 +1,7 @@ +function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
+
+procedure foo ()
+{
+ assert (exists x: int :: (0 <= x && x <= 2) && b1(x));
+}
+
diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl new file mode 100644 index 00000000..55947f1f --- /dev/null +++ b/Test/AbsHoudini/quant4.bpl @@ -0,0 +1,7 @@ +function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;
+
+procedure foo ()
+{
+ assert (exists x: int :: (0 <= x && x <= 2) && b1());
+}
+
diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl new file mode 100644 index 00000000..dfc44e47 --- /dev/null +++ b/Test/AbsHoudini/quant5.bpl @@ -0,0 +1,11 @@ +function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
+
+procedure foo ()
+{
+ var arr: [int] int;
+ assume (forall x: int :: arr[x] == 0);
+ arr[5] := 1;
+
+ assert (exists x: int :: arr[x] == 1 && b1(x));
+}
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat index 0bc74dfc..4d70be0e 100644 --- a/Test/AbsHoudini/runtest.bat +++ b/Test/AbsHoudini/runtest.bat @@ -15,8 +15,14 @@ for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do ( %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f
)
-for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl) do (
+for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do (
echo .
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:PredicateAbs %%f
)
+
+for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /z3opt:MBQI=true %%f
+)
|