summaryrefslogtreecommitdiff
path: root/Test/inline/test4.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/inline/test4.bpl')
-rw-r--r--Test/inline/test4.bpl108
1 files changed, 54 insertions, 54 deletions
diff --git a/Test/inline/test4.bpl b/Test/inline/test4.bpl
index 7743c498..2a646b58 100644
--- a/Test/inline/test4.bpl
+++ b/Test/inline/test4.bpl
@@ -1,55 +1,55 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-procedure main(x:int)
-{
- var A:[int]int;
- var i:int;
- var b:bool;
- var size:int;
-
- call i,b := find(A, size, x);
-
- if(b) {
- assert(i > 0 && A[i] == x);
- }
-
- return;
-}
-
-procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
-{
- var i:int;
- var b:bool;
-
- ret := -1;
- b := false;
- found := b;
- i := 0;
-
- while(i < size) {
- call b := check(A, i, x);
- if(b) {
- ret := i;
- found := b;
- break;
- }
-
- }
-
- return;
-
-}
-
-
-procedure {:inline 3} check (A:[int]int, i:int, c:int) returns (ret:bool)
- requires i >= 0;
- ensures (old(A[i]) > c) ==> ret == true;
-{
- if(A[i] == c) {
- ret := true;
- } else {
- ret := false;
- }
- return;
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure main(x:int)
+{
+ var A:[int]int;
+ var i:int;
+ var b:bool;
+ var size:int;
+
+ call i,b := find(A, size, x);
+
+ if(b) {
+ assert(i > 0 && A[i] == x);
+ }
+
+ return;
+}
+
+procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
+{
+ var i:int;
+ var b:bool;
+
+ ret := -1;
+ b := false;
+ found := b;
+ i := 0;
+
+ while(i < size) {
+ call b := check(A, i, x);
+ if(b) {
+ ret := i;
+ found := b;
+ break;
+ }
+
+ }
+
+ return;
+
+}
+
+
+procedure {:inline 3} check (A:[int]int, i:int, c:int) returns (ret:bool)
+ requires i >= 0;
+ ensures (old(A[i]) > c) ==> ret == true;
+{
+ if(A[i] == c) {
+ ret := true;
+ } else {
+ ret := false;
+ }
+ return;
} \ No newline at end of file