From 46b654cd5c5a0dc3df37d9a593fa5c81c59ab83f Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 7 Aug 2009 17:18:14 +0000
Subject: Fixed problem where nullary function with definition had caused a
 crash.

---
 Test/inline/Answer      |  7 +++++++
 Test/inline/runtest.bat |  5 +++++
 Test/inline/test0.bpl   | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 60 insertions(+)
 create mode 100644 Test/inline/test0.bpl

(limited to 'Test/inline')

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();
+}
-- 
cgit v1.2.3