diff options
Diffstat (limited to 'Test/test2/AssumeEnsures.bpl')
-rw-r--r-- | Test/test2/AssumeEnsures.bpl | 142 |
1 files changed, 71 insertions, 71 deletions
diff --git a/Test/test2/AssumeEnsures.bpl b/Test/test2/AssumeEnsures.bpl index 74789135..2c5ad6a2 100644 --- a/Test/test2/AssumeEnsures.bpl +++ b/Test/test2/AssumeEnsures.bpl @@ -1,71 +1,71 @@ -// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int;
-
-procedure Foo() returns ();
- modifies g;
- free ensures 0 <= g;
-
-implementation Foo() returns ()
-{
- entry:
- g := g + 1;
- return;
-}
-
-procedure BarGood() returns ()
- modifies g;
-{
- entry:
- call Foo();
- assert 0 <= g;
- return;
-}
-
-procedure BarBad() returns ()
- modifies g;
-{
- entry:
- call Foo();
- assert 0 < g;
- return;
-}
-
-// ----- Free preconditions
-
-procedure Proc() returns ();
- free requires g == 15;
-
-implementation Proc() returns ()
-{
- entry:
- assert g > 10; // yes, this condition can be used here
- return;
-}
-
-implementation Proc() returns ()
-{
- entry:
- assert g < 10; // error
- return;
-}
-
-procedure Caller0() returns ()
-{
- entry:
- call Proc(); // yes, legal, since the precondition is not checked
- return;
-}
-
-procedure Caller1() returns ()
-{
- entry:
- call Proc();
- assert g > 10; // error, because:
- // Free preconditions are ignored (that is, treated as "skip") for the caller.
- // This is a BoogiePL design choice. Another alternative would be to treat free
- // preconditions as assume commands also on the caller side, either in the order
- // that all preconditions are given, or before or after all the checked preconditions
- // have been checked.
- return;
-}
+// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var g: int; + +procedure Foo() returns (); + modifies g; + free ensures 0 <= g; + +implementation Foo() returns () +{ + entry: + g := g + 1; + return; +} + +procedure BarGood() returns () + modifies g; +{ + entry: + call Foo(); + assert 0 <= g; + return; +} + +procedure BarBad() returns () + modifies g; +{ + entry: + call Foo(); + assert 0 < g; + return; +} + +// ----- Free preconditions + +procedure Proc() returns (); + free requires g == 15; + +implementation Proc() returns () +{ + entry: + assert g > 10; // yes, this condition can be used here + return; +} + +implementation Proc() returns () +{ + entry: + assert g < 10; // error + return; +} + +procedure Caller0() returns () +{ + entry: + call Proc(); // yes, legal, since the precondition is not checked + return; +} + +procedure Caller1() returns () +{ + entry: + call Proc(); + assert g > 10; // error, because: + // Free preconditions are ignored (that is, treated as "skip") for the caller. + // This is a BoogiePL design choice. Another alternative would be to treat free + // preconditions as assume commands also on the caller side, either in the order + // that all preconditions are given, or before or after all the checked preconditions + // have been checked. + return; +} |