summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/AbsyCmd.cs28
-rw-r--r--Source/Core/BoogiePL.atg11
-rw-r--r--Source/Core/Parser.cs19
-rw-r--r--Test/test2/Answer23
-rw-r--r--Test/test2/FreeCall.bpl96
-rw-r--r--Test/test2/runtest.bat4
6 files changed, 163 insertions, 18 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b0c7cdb6..ae051b40 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1625,6 +1625,16 @@ namespace Microsoft.Boogie {
public abstract class CallCommonality : SugaredCmd {
public QKeyValue Attributes;
+ private bool isFree = false;
+ public bool IsFree {
+ get {
+ return isFree;
+ }
+ set {
+ isFree = value;
+ }
+ }
+
protected CallCommonality(IToken tok, QKeyValue kv)
: base(tok) {
Contract.Requires(tok != null);
@@ -1753,7 +1763,11 @@ namespace Microsoft.Boogie {
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
- stream.Write(this, level, "call ");
+ stream.Write(this, level, "");
+ if (IsFree) {
+ stream.Write("free ");
+ }
+ stream.Write("call ");
EmitAttributes(stream, Attributes);
string sep = "";
if (Outs.Count > 0) {
@@ -2029,7 +2043,7 @@ namespace Microsoft.Boogie {
Expr preConjunction = null;
for (int i = 0; i < this.Proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
- if (!req.Free) {
+ if (!req.Free && !IsFree) {
if (hasWildcard) {
Expr pre = Substituter.Apply(s, req.Condition);
if (preConjunction == null) {
@@ -2211,7 +2225,11 @@ namespace Microsoft.Boogie {
}
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
- stream.Write(this, level, "call ");
+ stream.Write(this, level, "");
+ if (IsFree) {
+ stream.Write("free ");
+ }
+ stream.Write("call ");
EmitAttributes(stream, Attributes);
stream.Write("forall ");
stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
@@ -2355,7 +2373,7 @@ namespace Microsoft.Boogie {
Expr preConjunction = null;
for (int i = 0; i < this.Proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
- if (!req.Free) {
+ if (!req.Free && !IsFree) {
Expr pre = Substituter.Apply(s, req.Condition);
if (preConjunction == null) {
preConjunction = pre;
@@ -2957,4 +2975,4 @@ namespace Microsoft.Boogie {
return visitor.VisitGotoCmd(this);
}
}
-} \ No newline at end of file
+}
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index b1fbd609..7519fb4c 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -905,7 +905,10 @@ CallCmd<out Cmd/*!*/ c>
QKeyValue kv = null;
Expr en; List<Expr> args;
c = dummyCmd;
+ bool isFree = false;
.)
+ [ "free" (. isFree = true; .)
+ ]
"call" (. x = t; .)
{ Attribute<ref kv> }
( Ident<out first>
@@ -914,7 +917,7 @@ CallCmd<out Cmd/*!*/ c>
{ "," CallForallArg<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
|
(. ids.Add(new IdentifierExpr(first, first.val)); .)
[ "," CallOutIdent<out p> (.
@@ -938,7 +941,7 @@ CallCmd<out Cmd/*!*/ c>
{ "," CallForallArg<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
)
| "forall"
Ident<out first> "(" (. args = new List<Expr>(); .)
@@ -946,7 +949,7 @@ CallCmd<out Cmd/*!*/ c>
{ "," CallForallArg<out en> (. args.Add(en); .)
}
]
- ")" (. c = new CallForallCmd(x, first.val, args, kv); .)
+ ")" (. c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; .)
| "*"
(. ids.Add(null); .)
[ "," CallOutIdent<out p> (.
@@ -970,7 +973,7 @@ CallCmd<out Cmd/*!*/ c>
{ "," CallForallArg<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
)
.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 9c208b86..34f43896 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1013,7 +1013,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
c = new HavocCmd(x,ids);
- } else if (la.kind == 48) {
+ } else if (la.kind == 33 || la.kind == 48) {
CallCmd(out cn);
Expect(7);
c = cn;
@@ -1194,7 +1194,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
QKeyValue kv = null;
Expr en; List<Expr> args;
c = dummyCmd;
+ bool isFree = false;
+ if (la.kind == 33) {
+ Get();
+ isFree = true;
+ }
Expect(48);
x = t;
while (la.kind == 25) {
@@ -1214,7 +1219,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
} else if (la.kind == 11 || la.kind == 47) {
ids.Add(new IdentifierExpr(first, first.val));
if (la.kind == 11) {
@@ -1250,7 +1255,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
} else SynErr(103);
} else if (la.kind == 49) {
Get();
@@ -1267,7 +1272,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
}
Expect(9);
- c = new CallForallCmd(x, first.val, args, kv);
+ c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree;
} else if (la.kind == 42) {
Get();
ids.Add(null);
@@ -1304,7 +1309,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
} else SynErr(104);
}
@@ -2028,8 +2033,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
diff --git a/Test/test2/Answer b/Test/test2/Answer
index f9d9a92e..da75f4f5 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -399,6 +399,29 @@ Execution trace:
Boogie program verifier finished with 1 verified, 4 errors
+-------------------- FreeCall.bpl --------------------
+FreeCall.bpl(37,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(8,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(37,5): anon0
+FreeCall.bpl(42,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(6,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(42,5): anon0
+FreeCall.bpl(59,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(16,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(59,5): anon0
+FreeCall.bpl(66,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(14,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(66,5): anon0
+FreeCall.bpl(87,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ FreeCall.bpl(85,5): anon0
+
+Boogie program verifier finished with 8 verified, 5 errors
+
-------------------- Arrays.bpl /typeEncoding:m --------------------
Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
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;
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index c9d4feac..3dc7d0c3 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
strings-no-where.bpl strings-where.bpl
Structured.bpl Where.bpl UpdateExpr.bpl
NeverPattern.bpl NullaryMaps.bpl Implies.bpl
- IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl) do (
+ IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl FreeCall.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /noinfer %%f
@@ -24,7 +24,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
)
echo -------------------- sk_hack.bpl --------------------
-%BGEXE% %* /noinfer /bv:z sk_hack.bpl
+%BGEXE% %* /noinfer /bv:z sk_hack.bpl
for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
echo.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 12:57:03 +0000