diff options
| author |  rustanleino <unknown> | 2009-08-07 17:18:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-08-07 17:18:14 +0000 |
| commit | 46b654cd5c5a0dc3df37d9a593fa5c81c59ab83f (patch) | |
| tree | 8378d2b9e5140c19154e8ceac7ff29e5495efffd /Test/inline | |
| parent | 8c24db1994be20528fd0285844ee6a32b847d2aa (diff) | |
Fixed problem where nullary function with definition had caused a crash.
Diffstat (limited to 'Test/inline')
| -rw-r--r-- | Test/inline/Answer | 7 | ||||
| -rw-r--r-- | Test/inline/runtest.bat | 5 | ||||
| -rw-r--r-- | Test/inline/test0.bpl | 48 |
3 files changed, 60 insertions, 0 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer index 39d5a5b4..8bbe0b98 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1,3 +1,10 @@ +-------------------- test0.bpl --------------------
+test0.bpl(30,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ test0.bpl(26,3): anon0
+ test0.bpl(30,5): anon3_Then
+
+Boogie program verifier finished with 1 verified, 1 error
-------------------- test1.bpl --------------------
procedure Main();
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index 3040d5b0..209845e6 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -3,6 +3,11 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
+for %%f in (test0.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% %* %%f
+)
+
for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* /inline:b /print:- /env:0 /printInlined /noinfer %%f
diff --git a/Test/inline/test0.bpl b/Test/inline/test0.bpl new file mode 100644 index 00000000..1b46f8c7 --- /dev/null +++ b/Test/inline/test0.bpl @@ -0,0 +1,48 @@ +// inlined functions
+
+function Twice(x: int) returns (int)
+{
+ x + x
+}
+
+function {:inline} Double(x: int) returns (int)
+{
+ 3 * x - x
+}
+
+function f(int) returns (int);
+function g(int) returns (int);
+function h(int) returns (int);
+function k(int) returns (int);
+axiom (forall x: int :: Twice(x) == f(x)); // here, Twice(x) and f(x) are both triggers
+axiom (forall x: int :: Double(x) == g(x)); // since Double is inlined, the trigger here is just g(x)
+axiom (forall x: int :: { f(x) } f(x) < h(x) );
+axiom (forall x: int :: { g(x) } g(x) < k(x) );
+
+procedure P(a: int, b: int, c: int)
+{
+ // The following is provable, because Twice triggers its definition and the resulting f(a)
+ // triggers the relation to h(a).
+ assert Twice(a) < h(a);
+ if (*) {
+ // The following is NOT provable, because Double is inlined and thus no g(b) term is ever
+ // created
+ assert Double(b) < k(b); // error
+ } else {
+ // The following IS provable, because the explicit g(c) will cause both of the necessary
+ // quantifiers to trigger
+ assert g(c) == 2*c;
+ assert Double(c) < k(c);
+ }
+}
+
+// nullary functions
+
+function Five() returns (int) { 5 }
+
+function {:inline} Eight() returns (e: int) { 8 }
+
+procedure Q()
+{
+ assert 8 * Five() == 5 * Eight();
+}
|