diff options
| author |  wuestholz <unknown> | 2011-09-14 16:28:25 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-09-14 16:28:25 +0200 |
| commit | c250f55e7af88a3671262e2c0522664f299ef2f2 (patch) | |
| tree | 26755b6bff316c4d656d70cf69dc6ca6bdfbe589 /Test/test2/FreeCall.bpl | |
| parent | 23a94e0bbd32c8c612cb79a6745b5bee4dd667dd (diff) | |
Added "free call" statements that don't check the precondition in the caller.
Diffstat (limited to 'Test/test2/FreeCall.bpl')
| -rw-r--r-- | Test/test2/FreeCall.bpl | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl new file mode 100644 index 00000000..06eb737e --- /dev/null +++ b/Test/test2/FreeCall.bpl @@ -0,0 +1,96 @@ +// Test the implementation of free calls. These calls don't check the preconditions of the
+// called procedure in the caller.
+
+
+procedure Uncallable(i: int)
+ requires 0 <= i;
+ free requires true;
+ requires false;
+{
+
+}
+
+procedure UncallableReturn(i: int) returns (b: bool)
+ requires 0 <= i;
+ free requires true;
+ requires false;
+{
+ b := true;
+}
+
+function T(b: bool) : bool
+{
+ b == true
+}
+
+procedure TestCallForall(b: bool)
+ requires T(b);
+ free requires true;
+ ensures T(b);
+{
+
+}
+
+
+procedure NormalCall0()
+{
+ call Uncallable(0); // error: precondition violation
+}
+
+procedure NormalCall1()
+{
+ call Uncallable(-1); // error: precondition violation
+}
+
+procedure FreeCall0()
+{
+ free call Uncallable(0);
+}
+
+procedure FreeCall1()
+{
+ free call Uncallable(-1);
+}
+
+procedure NormalCall2()
+{
+ var b: bool;
+
+ call b := UncallableReturn(0); // error: precondition violation
+}
+
+procedure NormalCall3()
+{
+ var b: bool;
+
+ call b := UncallableReturn(-1); // error: precondition violation
+}
+
+procedure FreeCall3()
+{
+ var b: bool;
+
+ free call b := UncallableReturn(0);
+}
+
+procedure FreeCall4()
+{
+ var b: bool;
+
+ free call b := UncallableReturn(-1);
+}
+
+procedure NormalCall5()
+{
+ call forall TestCallForall(*);
+ assert T(true);
+ assert T(false); // error
+}
+
+procedure FreeCall5()
+{
+ free call forall TestCallForall(*);
+ assert T(true);
+ assert T(false);
+ assert false;
+}
|