Boogie: Get rid of {:inline} attributes on axioms

6 files changed, 20 insertions, 63 deletions

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 72ba1170..ae632f79 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1448,26 +1448,15 @@ Execution trace:
     test5.bpl(34,10): anon0$2

 

 Boogie program verifier finished with 4 verified, 1 error

--------------------- expansion.bpl --------------------

-expansion.bpl(29,14): Error: invalid type for argument 0 in application of foo1: bool (expected: int)

-expansion.bpl(13,16): Error: expansion: {:inline ...} expects either true or false as the argument

-expansion.bpl(14,22): Error: expansion: identifier was not quantified over

-expansion.bpl(15,22): Error: expansion: identifier was not quantified over

-expansion.bpl(16,22): Error: expansion: more variables quantified over, than used in function

-expansion.bpl(18,21): Error: expansion: axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))

-expansion.bpl(19,53): Error: expansion: only identifiers supported as function arguments

-expansion.bpl(33,22): Error: expansion: an identifier was used more than once

-8 type checking errors detected in expansion.bpl

 -------------------- expansion3.bpl --------------------

 *** detected expansion loop on foo3

 *** detected expansion loop on foo3

 *** detected expansion loop on foo3

-*** more than one possible expansion for x1

-expansion3.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    expansion3.bpl(18,3): anon0

 

-Boogie program verifier finished with 1 verified, 1 error

+Boogie program verifier finished with 1 verified, 0 errors

+-------------------- expansion4.bpl --------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

 -------------------- Elevator.bpl --------------------

 Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

 Execution trace:

diff --git a/Test/inline/expansion.bpl b/Test/inline/expansion.bpl
deleted file mode 100644
index 41acfb44..00000000
--- a/Test/inline/expansion.bpl
+++ /dev/null
@@ -1,33 +0,0 @@
-const q : int;

-const p : bool;

-function foo(x:int, y:bool) returns(bool);

-function foo1(x:int, y:bool) returns(bool);

-function foo2(x:int, y:bool) returns(bool);

-function foo3(x:int, y:bool) returns(bool);

-// OK

-axiom {:inline false} (forall x:int, y:bool :: foo(x,p) <==> x > 10 && y);

-axiom {:inline true} (forall x:int, y:bool :: foo1(x,y) == (x > 10 && y));

-axiom {:inline true} (forall x:int, y:bool :: foo2(x,y) == (q > 10 && y));

-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));

-// fail

-axiom {:inline 1} (forall x:int, y:bool :: foo(x,y) <==> x > 10 && y);

-axiom {:inline true} (forall x:int, y:bool :: foo(x,p) <==> x > 10 && y);

-axiom {:inline true} (forall y:bool :: foo(q,y) == (q > 10 && y));

-axiom {:inline true} (forall x:int, y:bool, z:int :: foo(x,y) == (q > 10 && y));

-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == (q > 10 && y));

-axiom {:inline true} true;

-axiom {:inline true} (forall y:bool, x:int :: foo3(x,true) == (q > 10 && y));

-

-

-procedure baz1()

-{

-  assert foo3(1,true);

-}

-

-procedure baz2()

-{

-  assert foo1(true,true);

-}

-

-function foo4(x:int, y:int) returns(bool);

-axiom {:inline true} (forall x:int,z:int :: foo4(x,x) == (x > 0));

diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl
index fc14a0eb..b6ed19ed 100644
--- a/Test/inline/expansion2.bpl
+++ b/Test/inline/expansion2.bpl
@@ -1,7 +1,7 @@
-function xxgz(x:int) returns(bool);

-function xxf1(x:int,y:bool) returns(int);

-axiom {:inline true} (forall x:int :: xxgz(x) <==> x > 0);

-axiom {:inline true} (forall x:int, y:bool :: xxf1(x,y) == x+1);

+function {:inline true} xxgz(x:int) returns(bool)

+ { x > 0 }

+function {:inline true} xxf1(x:int,y:bool) returns(int)

+  { x + 1 }

 

 axiom (forall z:int :: z>12 ==> xxgz(z));

 axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);

diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl
index 1fd3d853..2b1f0caa 100644
--- a/Test/inline/expansion3.bpl
+++ b/Test/inline/expansion3.bpl
@@ -1,5 +1,5 @@
-function foo3(x:int, y:bool) returns(bool);

-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));

+function {:inline true} foo3(x:int, y:bool) returns(bool)

+ { foo3(x,y) }

 

 axiom foo3(1,false);

 

@@ -9,11 +9,3 @@ procedure baz1()
   assume foo3(1,true);

 }

 

-function x1(x:int) returns(bool);

-axiom {:inline true} (forall x:int :: x1(x) <==> x > 0);

-axiom {:inline true} (forall x:int :: x1(x) <==> x >= 1);

-

-procedure bar()

-{

-  assert x1(3);

-}

diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl
new file mode 100644
index 00000000..be11a391
--- /dev/null
+++ b/Test/inline/expansion4.bpl
@@ -0,0 +1,9 @@
+function foo(x:int) : int

+  { if x <= 0 then 1 else foo(x - 1) + 2 }

+

+procedure bar()

+{

+  assert foo(0) == 1;

+  assert foo(1) == 3;

+  assert foo(2) == 5;

+}

diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index f04b84da..f56d55a0 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -13,7 +13,7 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do (
   %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f

 )

 

-for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (

+for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (

   echo -------------------- %%f --------------------

   %BGEXE% %* %%f

 )