diff options
Diffstat (limited to 'Test/AbsHoudini/f1.bpl')
-rw-r--r-- | Test/AbsHoudini/f1.bpl | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl index e5ed85ef..b7ee9011 100644 --- a/Test/AbsHoudini/f1.bpl +++ b/Test/AbsHoudini/f1.bpl @@ -1,32 +1,32 @@ -var g: int;
-
-procedure {:entrypoint} main()
- modifies g;
-{
- var x: int;
- var c: bool;
-
- g := 1;
-
- if(c) {
- g := g + 1;
- } else {
- g := 3;
- }
-
- call foo();
-
- if(old(g) == 0) { g := 1; }
-}
-
-procedure foo()
- modifies g;
-{
- g := g + 1;
-}
-
-procedure {:template} summaryTemplate();
- ensures {:post} g == old(g) + 1;
- ensures {:post} g == old(g) + 2;
- ensures {:post} g == old(g) + 3;
- ensures {:pre} old(g) == 0;
+var g: int; + +procedure {:entrypoint} main() + modifies g; +{ + var x: int; + var c: bool; + + g := 1; + + if(c) { + g := g + 1; + } else { + g := 3; + } + + call foo(); + + if(old(g) == 0) { g := 1; } +} + +procedure foo() + modifies g; +{ + g := g + 1; +} + +procedure {:template} summaryTemplate(); + ensures {:post} g == old(g) + 1; + ensures {:post} g == old(g) + 2; + ensures {:post} g == old(g) + 3; + ensures {:pre} old(g) == 0; |