diff options
| -rw-r--r-- | Source/Core/AbsyExpr.ssc | 94 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 10 | ||||
| -rw-r--r-- | Source/Core/Parser.ssc | 234 | ||||
| -rw-r--r-- | Source/Core/Scanner.ssc | 18 | ||||
| -rw-r--r-- | Source/Provers/Isabelle/Prover.ssc | 6 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.ssc | 7 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.ssc | 4 | ||||
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.ssc | 13 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.ssc | 11 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.ssc | 29 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTPrinter.ssc | 5 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.ssc | 4 | ||||
| -rw-r--r-- | Test/test1/Answer | 4 | ||||
| -rw-r--r-- | Test/test1/IfThenElse0.bpl | 8 | ||||
| -rw-r--r-- | Test/test1/runtest.bat | 1 | ||||
| -rw-r--r-- | Test/test2/Answer | 10 | ||||
| -rw-r--r-- | Test/test2/IfThenElse1.bpl | 34 | ||||
| -rw-r--r-- | Test/test2/runtest.bat | 3 |
18 files changed, 372 insertions, 123 deletions
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index c07db23b..ebc594f3 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -843,6 +843,8 @@ namespace Microsoft.Boogie T Visit(MapStore! mapStore);
T Visit(TypeCoercion! typeCoercion);
+
+ T Visit(IfThenElse! ifThenElse);
}
public interface IAppliable
@@ -2895,6 +2897,97 @@ namespace Microsoft.Boogie }
}
+
+
+ public class IfThenElse : IAppliable, AI.IFunctionSymbol {
+
+ public IToken! tok;
+
+ public IfThenElse(IToken! tok) {
+ this.tok = tok;
+ }
+
+ public string! FunctionName { get {
+ return "if-then-else";
+ } }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj)
+ {
+ if (!(obj is IfThenElse)) return false;
+ return true;
+ }
+
+ [Pure]
+ public override int GetHashCode()
+ {
+ return 1;
+ }
+
+ public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(ref this.tok);
+ assert args.Length == 3;
+ stream.Write("(if ");
+ ((!)args[0]).Emit(stream, 0x00, false);
+ stream.Write(" then ");
+ ((!)args[1]).Emit(stream, 0x00, false);
+ stream.Write(" else ");
+ ((!)args[2]).Emit(stream, 0x00, false);
+ stream.Write(")");
+ }
+
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ // PR: nothing?
+ }
+
+ public int ArgumentCount { get {
+ return 3;
+ } }
+
+ public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
+ {
+ assert args.Length == 3;
+ // the default; the only binary operator with a type parameter is equality, but right
+ // we don't store this parameter because it does not appear necessary
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+ Expr arg0 = (!)args[0];
+ Expr arg1 = (!)args[1];
+ Expr arg2 = (!)args[2];
+
+ if (!((!)arg0.Type).Unify(Type.Bool)) {
+ tc.Error(this.tok, "the first argument to if-then-else should be bool, not {0}", arg0.Type);
+ } else if (!((!)arg1.Type).Unify((!)arg2.Type)) {
+ tc.Error(this.tok, "branches of if-then-else have incompatible types {0} and {1}", arg1.Type, arg2.Type);
+ } else {
+ return arg1.Type;
+ }
+
+ return null;
+ }
+
+ /// <summary>
+ /// Returns the result type of the IAppliable, supposing the argument are of the correct types.
+ /// </summary>
+ public Type! ShallowType(ExprSeq! args) {
+ return ((!)args[1]).ShallowType;
+ }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol { get { return this; } }
+
+ public AI.AIType! AIType {
+ [Rep][ResultNotNewlyAllocated]
+ get {
+ return AI.Value.FunctionType(3);
+ } }
+
+ public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ return visitor.Visit(this);
+ }
+ }
+
+
+
public class BlockExpr : Expr
{
public VariableSeq! LocVars;
@@ -3254,3 +3347,4 @@ namespace Microsoft.Boogie }
}
}
+
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index eab10ff9..ab7e6c81 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1291,6 +1291,7 @@ AtomExpression<out Expr! e> e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)
)
")"
+ | IfThenElseExpression<out e>
)
.
@@ -1352,6 +1353,15 @@ AttributeParameter<out object! o> )
.
+IfThenElseExpression<out Expr! e>
+= (. IToken! tok;
+ Expr! e0, e1, e2;
+ e = dummyExpr; .)
+ "if" (. tok = token; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>
+ (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .)
+ .
+
+
QuantifierBody<IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
out QKeyValue kv, out Trigger trig, out Expr! body>
= (. trig = null; typeParams = new TypeVariableSeq ();
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc index a7453d09..95eb1a76 100644 --- a/Source/Core/Parser.ssc +++ b/Source/Core/Parser.ssc @@ -1,8 +1,3 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
using PureCollections;
using System.Collections;
using System.Collections.Generic;
@@ -16,7 +11,7 @@ using Microsoft.Contracts; namespace BoogiePL {
public class Parser {
- const int maxT = 85;
+ const int maxT = 86;
const bool T = true;
const bool x = false;
@@ -299,7 +294,7 @@ private class BvBounds : Expr { Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, "", retTy);
- } else Error(86);
+ } else Error(87);
if (t.kind == 25) {
Get();
Expression(out tmp);
@@ -307,7 +302,7 @@ private class BvBounds : Expr { Expect(26);
} else if (t.kind == 7) {
Get();
- } else Error(87);
+ } else Error(88);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));
@@ -451,7 +446,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null);
- } else Error(88);
+ } else Error(89);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -555,7 +550,7 @@ private class BvBounds : Expr { ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
} else if (t.kind == 15 || t.kind == 17) {
MapType(out ty);
- } else Error(89);
+ } else Error(90);
}
static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {
@@ -602,7 +597,7 @@ private class BvBounds : Expr { Get();
Type(out ty);
Expect(9);
- } else Error(90);
+ } else Error(91);
}
static void Ident(out IToken! x) {
@@ -631,7 +626,7 @@ private class BvBounds : Expr { } else if (t.kind == 15 || t.kind == 17) {
MapType(out ty);
ts.Add(ty);
- } else Error(91);
+ } else Error(92);
}
static void MapType(out Bpl.Type! ty) {
@@ -803,7 +798,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecPrePost(true, pre, post);
} else if (t.kind == 34 || t.kind == 35) {
SpecPrePost(false, pre, post);
- } else Error(92);
+ } else Error(93);
}
static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {
@@ -831,7 +826,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecBody(out locals, out blocks);
Expect(7);
pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv));
- } else Error(93);
+ } else Error(94);
} else if (t.kind == 35) {
Get();
tok = token;
@@ -846,8 +841,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecBody(out locals, out blocks);
Expect(7);
post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv));
- } else Error(94);
- } else Error(95);
+ } else Error(95);
+ } else Error(96);
}
static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {
@@ -898,7 +893,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(token,e));
- } else Error(96);
+ } else Error(97);
Expect(7);
}
@@ -942,7 +937,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { CallCmd(out cn);
Expect(7);
c = cn;
- } else Error(97);
+ } else Error(98);
}
static void StmtList(out StmtList! stmtList) {
@@ -1026,7 +1021,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 45) {
BreakCmd(out bcmd);
ec = bcmd;
- } else Error(98);
+ } else Error(99);
}
static void TransferCmd(out TransferCmd! tc) {
@@ -1044,7 +1039,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 39) {
Get();
tc = new ReturnCmd(token);
- } else Error(99);
+ } else Error(100);
Expect(7);
}
@@ -1069,7 +1064,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
StmtList(out els);
elseOption = els;
- } else Error(100);
+ } else Error(101);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1128,7 +1123,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(101);
+ } else Error(102);
Expect(9);
}
@@ -1166,7 +1161,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(7);
c = new AssignCmd(x, lhss, rhss);
- } else Error(102);
+ } else Error(103);
}
static void CallCmd(out Cmd! c) {
@@ -1229,7 +1224,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(9);
c = new CallCmd(x, first.val, es, ids);
- } else Error(103);
+ } else Error(104);
} else if (t.kind == 51) {
Get();
Ident(out first);
@@ -1283,7 +1278,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(9);
c = new CallCmd(x, first.val, es, ids);
- } else Error(104);
+ } else Error(105);
}
static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {
@@ -1323,7 +1318,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (StartOf(5)) {
Expression(out e);
exprOptional = e;
- } else Error(105);
+ } else Error(106);
}
static void CallOutIdent(out IToken id) {
@@ -1335,7 +1330,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 1) {
Ident(out p);
id = p;
- } else Error(106);
+ } else Error(107);
}
static void Expressions(out ExprSeq! es) {
@@ -1380,7 +1375,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 53) {
Get();
- } else Error(107);
+ } else Error(108);
}
static void LogicalExpression(out Expr! e0) {
@@ -1418,7 +1413,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 55) {
Get();
- } else Error(108);
+ } else Error(109);
}
static void ExpliesOp() {
@@ -1426,7 +1421,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 57) {
Get();
- } else Error(109);
+ } else Error(110);
}
static void RelationalExpression(out Expr! e0) {
@@ -1444,7 +1439,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 59) {
Get();
- } else Error(110);
+ } else Error(111);
}
static void OrOp() {
@@ -1452,7 +1447,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 61) {
Get();
- } else Error(111);
+ } else Error(112);
}
static void BvTerm(out Expr! e0) {
@@ -1519,7 +1514,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { x = token; op=BinaryOperator.Opcode.Ge;
break;
}
- default: Error(112); break;
+ default: Error(113); break;
}
}
@@ -1551,7 +1546,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 72) {
Get();
x = token; op=BinaryOperator.Opcode.Sub;
- } else Error(113);
+ } else Error(114);
}
static void UnaryExpression(out Expr! e) {
@@ -1570,7 +1565,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(12)) {
CoercionExpression(out e);
- } else Error(114);
+ } else Error(115);
}
static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {
@@ -1584,7 +1579,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 74) {
Get();
x = token; op=BinaryOperator.Opcode.Mod;
- } else Error(115);
+ } else Error(116);
}
static void NegOp() {
@@ -1592,7 +1587,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 76) {
Get();
- } else Error(116);
+ } else Error(117);
}
static void CoercionExpression(out Expr! e) {
@@ -1616,7 +1611,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else Error(117);
+ } else Error(118);
}
}
@@ -1726,7 +1721,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new NAryExpr(x, new FunctionCall(id), es);
} else if (t.kind == 9) {
e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
- } else Error(118);
+ } else Error(119);
Expect(9);
}
break;
@@ -1747,23 +1742,27 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { if (e is BvBounds)
SemErr("parentheses around bitvector bounds " +
"are not allowed");
- } else if (t.kind == 51 || t.kind == 80) {
+ } else if (t.kind == 51 || t.kind == 81) {
Forall();
x = token;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
- } else if (t.kind == 81 || t.kind == 82) {
+ } else if (t.kind == 82 || t.kind == 83) {
Exists();
x = token;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else Error(119);
+ } else Error(120);
Expect(9);
break;
}
- default: Error(120); break;
+ case 40: {
+ IfThenElseExpression(out e);
+ break;
+ }
+ default: Error(121); break;
}
}
@@ -1786,9 +1785,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { static void Forall() {
if (t.kind == 51) {
Get();
- } else if (t.kind == 80) {
+ } else if (t.kind == 81) {
Get();
- } else Error(121);
+ } else Error(122);
}
static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
@@ -1805,7 +1804,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
} else if (t.kind == 1) {
BoundVars(q, out ds);
- } else Error(122);
+ } else Error(123);
QSep();
while (t.kind == 25) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1814,11 +1813,25 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
static void Exists() {
- if (t.kind == 81) {
+ if (t.kind == 82) {
Get();
- } else if (t.kind == 82) {
+ } else if (t.kind == 83) {
Get();
- } else Error(123);
+ } else Error(124);
+ }
+
+ static void IfThenElseExpression(out Expr! e) {
+ IToken! tok;
+ Expr! e0, e1, e2;
+ e = dummyExpr;
+ Expect(40);
+ tok = token;
+ Expression(out e0);
+ Expect(80);
+ Expression(out e1);
+ Expect(41);
+ Expression(out e2);
+ e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2));
}
static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1874,7 +1887,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { trig.AddLast(new Trigger(tok, true, es, null));
}
- } else Error(124);
+ } else Error(125);
Expect(26);
}
@@ -1888,15 +1901,15 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { } else if (StartOf(5)) {
Expression(out e);
o = e;
- } else Error(125);
+ } else Error(126);
}
static void QSep() {
- if (t.kind == 83) {
+ if (t.kind == 84) {
Get();
- } else if (t.kind == 84) {
+ } else if (t.kind == 85) {
Get();
- } else Error(126);
+ } else Error(127);
}
@@ -1995,53 +2008,54 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { case 77: s = "false expected"; break;
case 78: s = "true expected"; break;
case 79: s = "old expected"; break;
- case 80: s = "\\u2200 expected"; break;
- case 81: s = "exists expected"; break;
- case 82: s = "\\u2203 expected"; break;
- case 83: s = ":: expected"; break;
- case 84: s = "\\u2022 expected"; break;
- case 85: s = "??? expected"; break;
- case 86: s = "invalid Function"; break;
+ case 80: s = "then expected"; break;
+ case 81: s = "\\u2200 expected"; break;
+ case 82: s = "exists expected"; break;
+ case 83: s = "\\u2203 expected"; break;
+ case 84: s = ":: expected"; break;
+ case 85: s = "\\u2022 expected"; break;
+ case 86: s = "??? expected"; break;
case 87: s = "invalid Function"; break;
- case 88: s = "invalid Procedure"; break;
- case 89: s = "invalid Type"; break;
- case 90: s = "invalid TypeAtom"; break;
- case 91: s = "invalid TypeArgs"; break;
- case 92: s = "invalid Spec"; break;
- case 93: s = "invalid SpecPrePost"; break;
+ case 88: s = "invalid Function"; break;
+ case 89: s = "invalid Procedure"; break;
+ case 90: s = "invalid Type"; break;
+ case 91: s = "invalid TypeAtom"; break;
+ case 92: s = "invalid TypeArgs"; break;
+ case 93: s = "invalid Spec"; break;
case 94: s = "invalid SpecPrePost"; break;
case 95: s = "invalid SpecPrePost"; break;
- case 96: s = "invalid SpecBlock"; break;
- case 97: s = "invalid LabelOrCmd"; break;
- case 98: s = "invalid StructuredCmd"; break;
- case 99: s = "invalid TransferCmd"; break;
- case 100: s = "invalid IfCmd"; break;
- case 101: s = "invalid Guard"; break;
- case 102: s = "invalid LabelOrAssign"; break;
- case 103: s = "invalid CallCmd"; break;
+ case 96: s = "invalid SpecPrePost"; break;
+ case 97: s = "invalid SpecBlock"; break;
+ case 98: s = "invalid LabelOrCmd"; break;
+ case 99: s = "invalid StructuredCmd"; break;
+ case 100: s = "invalid TransferCmd"; break;
+ case 101: s = "invalid IfCmd"; break;
+ case 102: s = "invalid Guard"; break;
+ case 103: s = "invalid LabelOrAssign"; break;
case 104: s = "invalid CallCmd"; break;
- case 105: s = "invalid CallForallArg"; break;
- case 106: s = "invalid CallOutIdent"; break;
- case 107: s = "invalid EquivOp"; break;
- case 108: s = "invalid ImpliesOp"; break;
- case 109: s = "invalid ExpliesOp"; break;
- case 110: s = "invalid AndOp"; break;
- case 111: s = "invalid OrOp"; break;
- case 112: s = "invalid RelOp"; break;
- case 113: s = "invalid AddOp"; break;
- case 114: s = "invalid UnaryExpression"; break;
- case 115: s = "invalid MulOp"; break;
- case 116: s = "invalid NegOp"; break;
- case 117: s = "invalid CoercionExpression"; break;
- case 118: s = "invalid AtomExpression"; break;
+ case 105: s = "invalid CallCmd"; break;
+ case 106: s = "invalid CallForallArg"; break;
+ case 107: s = "invalid CallOutIdent"; break;
+ case 108: s = "invalid EquivOp"; break;
+ case 109: s = "invalid ImpliesOp"; break;
+ case 110: s = "invalid ExpliesOp"; break;
+ case 111: s = "invalid AndOp"; break;
+ case 112: s = "invalid OrOp"; break;
+ case 113: s = "invalid RelOp"; break;
+ case 114: s = "invalid AddOp"; break;
+ case 115: s = "invalid UnaryExpression"; break;
+ case 116: s = "invalid MulOp"; break;
+ case 117: s = "invalid NegOp"; break;
+ case 118: s = "invalid CoercionExpression"; break;
case 119: s = "invalid AtomExpression"; break;
case 120: s = "invalid AtomExpression"; break;
- case 121: s = "invalid Forall"; break;
- case 122: s = "invalid QuantifierBody"; break;
- case 123: s = "invalid Exists"; break;
- case 124: s = "invalid AttributeOrTrigger"; break;
- case 125: s = "invalid AttributeParameter"; break;
- case 126: s = "invalid QSep"; break;
+ case 121: s = "invalid AtomExpression"; break;
+ case 122: s = "invalid Forall"; break;
+ case 123: s = "invalid QuantifierBody"; break;
+ case 124: s = "invalid Exists"; break;
+ case 125: s = "invalid AttributeOrTrigger"; break;
+ case 126: s = "invalid AttributeParameter"; break;
+ case 127: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -2049,21 +2063,21 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
static bool[,]! set = {
- {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,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,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,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, 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,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,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,x,x, x,x,x,x, x,x,x,x, 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, 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, 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,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,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,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,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, T,x,x,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,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,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,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,T,T, T,T,T,T, T,T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, 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,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, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x},
- {x,T,T,T, 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, x,x,x,x, x,x,x,x, x,x,x,x, 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, 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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, x,x,x,T, x,x,x,T, T,x,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,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, 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,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,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,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, 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, 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,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,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,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,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, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,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,T,T, 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,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,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,T,T,T, 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,x,x, T,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, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},
+ {x,T,T,T, 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, 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, x,x,x,x, x,x,x,x}
};
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index 745f8dc4..d8e18754 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -1,8 +1,3 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- using System;
using System.IO;
using System.Collections;
@@ -350,7 +345,7 @@ public class Scanner { start[8804] = 45;
start[8805] = 46;
}
- const int noSym = 85;
+ const int noSym = 86;
static short[] start = new short[16385];
@@ -524,7 +519,8 @@ public class Scanner { case "false": t.kind = 77; break;
case "true": t.kind = 78; break;
case "old": t.kind = 79; break;
- case "exists": t.kind = 81; break;
+ case "then": t.kind = 80; break;
+ case "exists": t.kind = 82; break;
default: break;
}
@@ -672,13 +668,13 @@ public class Scanner { case 52:
{t.kind = 76; goto done;}
case 53:
- {t.kind = 80; goto done;}
+ {t.kind = 81; goto done;}
case 54:
- {t.kind = 82; goto done;}
- case 55:
{t.kind = 83; goto done;}
- case 56:
+ case 55:
{t.kind = 84; goto done;}
+ case 56:
+ {t.kind = 85; goto done;}
case 57: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Provers/Isabelle/Prover.ssc b/Source/Provers/Isabelle/Prover.ssc index 9b91cd63..33764112 100644 --- a/Source/Provers/Isabelle/Prover.ssc +++ b/Source/Provers/Isabelle/Prover.ssc @@ -756,6 +756,12 @@ namespace Microsoft.Boogie.Isabelle b2i.Write(child2);
return true;
}
+
+ public bool VisitIfThenElseOp(VCExprNAry! node, B2I! b2i)
+ {
+ throw new System.NotImplementedException(); // TODO
+ }
+
public bool VisitHeapSuccessionOp(VCExprNAry! node, B2I! b2i)
{
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.ssc b/Source/Provers/SMTLib/SMTLibLineariser.ssc index cbf69107..7efa109f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.ssc +++ b/Source/Provers/SMTLib/SMTLibLineariser.ssc @@ -140,6 +140,7 @@ namespace Microsoft.Boogie.SMTLib internal const string! orName = "or"; // disjunction
internal const string! notName = "not"; // negation
internal const string! impliesName = "implies"; // implication
+ internal const string! iteName = "ite"; // if-then-else
internal const string! iffName = "iff"; // logical equivalence
internal const string! eqName = "="; // equality
internal const string! lessName = "<";
@@ -160,6 +161,7 @@ namespace Microsoft.Boogie.SMTLib internal const string! boolNotName = "boolNot";
internal const string! boolIffName = "boolIff";
internal const string! boolImpliesName = "boolImplies";
+ internal const string! boolIteName = "ite";
internal const string! termUEqual = "UEqual";
internal const string! termTEqual = "TEqual";
internal const string! termIntEqual = "IntEqual";
@@ -519,6 +521,11 @@ namespace Microsoft.Boogie.SMTLib return true;
}
+ public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(boolIteName, iteName, node, options);
+ return true;
+ }
+
public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {
ExprLineariser.AssertAsFormula(distinctName, options);
diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc index f6393679..4698f541 100644 --- a/Source/VCExpr/Boogie2VCExpr.ssc +++ b/Source/VCExpr/Boogie2VCExpr.ssc @@ -738,6 +738,10 @@ namespace Microsoft.Boogie.VCExprAST return this.args[0];
}
+ public VCExpr! Visit(IfThenElse! ite) {
+ return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);
+ }
+
///////////////////////////////////////////////////////////////////////////////
private VCExpr! TranslateBinaryOperator(BinaryOperator! app, List<VCExpr!>! args) {
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index 52681162..7085bffe 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -701,6 +701,19 @@ namespace Microsoft.Boogie.VCExprAST return true;
}
+ public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) {
+
+ wr.Write("(ITE ");
+ ExprLineariser.Linearise(node[0], options.SetAsTerm(false));
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[2], options);
+ wr.Write(")");
+
+ return true;
+ }
+
public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) {
if (CommandLineOptions.Clo.ReflectAdd) {
WriteTermApplication(intAddNameReflect, node, options);
diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc index 604be456..d41cb887 100644 --- a/Source/VCExpr/TypeErasure.ssc +++ b/Source/VCExpr/TypeErasure.ssc @@ -1016,6 +1016,17 @@ namespace Microsoft.Boogie.TypeErasure // (at least for Simplify ... should this be ensured at a later point?)
return CastArguments(node, Type.Bool, bindings, Eraser.Polarity);
}
+ public override VCExpr! VisitIfThenElseOp (VCExprNAry! node, VariableBindings! bindings) {
+ List<VCExpr!>! newArgs = MutateSeq(node, bindings, 0);
+ newArgs[0] = AxBuilder.Cast(newArgs[0], Type.Bool);
+ Type t = node.Type;
+ if (!AxBuilder.UnchangedType(t)) {
+ t = AxBuilder.U;
+ }
+ newArgs[1] = AxBuilder.Cast(newArgs[1], t);
+ newArgs[2] = AxBuilder.Cast(newArgs[2], t);
+ return Gen.Function(node.Op, newArgs);
+ }
public override VCExpr! VisitAddOp (VCExprNAry! node, VariableBindings! bindings) {
return CastArguments(node, Type.Int, bindings, 0);
}
diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc index 5a9063cc..e08e6138 100644 --- a/Source/VCExpr/VCExprAST.ssc +++ b/Source/VCExpr/VCExprAST.ssc @@ -221,6 +221,7 @@ namespace Microsoft.Boogie // ternary version of the subtype operator, the first argument of which gives
// the type of the compared terms
public static readonly VCExprOp! Subtype3Op = new VCExprNAryOp (3, Type.Bool);
+ public static readonly VCExprOp! IfThenElseOp = new VCExprIfThenElseOp();
public VCExprOp! BoogieFunctionOp(Function! func) {
return new VCExprBoogieFunctionOp(func);
@@ -990,6 +991,34 @@ namespace Microsoft.Boogie.VCExprAST }
}
+ public class VCExprIfThenElseOp : VCExprOp {
+ public override int Arity { get { return 3; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return args[1].Type;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprIfThenElseOp)
+ return true;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return 1;
+ }
+
+ internal VCExprIfThenElseOp() {
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitIfThenElseOp(expr, arg);
+ }
+ }
+
/////////////////////////////////////////////////////////////////////////////////
// Bitvector operators
diff --git a/Source/VCExpr/VCExprASTPrinter.ssc b/Source/VCExpr/VCExprASTPrinter.ssc index 1c143516..ca8ec11a 100644 --- a/Source/VCExpr/VCExprASTPrinter.ssc +++ b/Source/VCExpr/VCExprASTPrinter.ssc @@ -193,6 +193,9 @@ namespace Microsoft.Boogie.VCExprAST public bool VisitBvConcatOp (VCExprNAry! node, TextWriter! wr) {
return PrintNAry("BvConcat", node, wr);
}
+ public bool VisitIfThenElseOp(VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("if-then-else", node, wr);
+ }
public bool VisitAddOp (VCExprNAry! node, TextWriter! wr) {
if (CommandLineOptions.Clo.ReflectAdd) {
return PrintNAry("Reflect$Add", node, wr);
@@ -237,4 +240,4 @@ namespace Microsoft.Boogie.VCExprAST }
-}
\ No newline at end of file +}
diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc index 2808f6bb..1ae71b26 100644 --- a/Source/VCExpr/VCExprASTVisitors.ssc +++ b/Source/VCExpr/VCExprASTVisitors.ssc @@ -51,6 +51,7 @@ namespace Microsoft.Boogie.VCExprAST Result VisitSubtypeOp (VCExprNAry! node, Arg arg);
Result VisitSubtype3Op (VCExprNAry! node, Arg arg);
Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg);
+ Result VisitIfThenElseOp (VCExprNAry! node, Arg arg);
}
//////////////////////////////////////////////////////////////////////////////
@@ -955,6 +956,9 @@ namespace Microsoft.Boogie.VCExprAST public virtual Result VisitBvConcatOp (VCExprNAry! node, Arg arg) {
return StandardResult(node, arg);
}
+ public virtual Result VisitIfThenElseOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
public virtual Result VisitAddOp (VCExprNAry! node, Arg arg) {
return StandardResult(node, arg);
}
diff --git a/Test/test1/Answer b/Test/test1/Answer index b0f4aac3..10ad5494 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -135,3 +135,7 @@ FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int) FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)
FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)
3 type checking errors detected in FunBody.bpl
+IfThenElse0.bpl(5,7): Error: the first argument to if-then-else should be bool, not int
+IfThenElse0.bpl(6,7): Error: branches of if-then-else have incompatible types bool and int
+IfThenElse0.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to bool)
+3 type checking errors detected in IfThenElse0.bpl
diff --git a/Test/test1/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl new file mode 100644 index 00000000..c26461b1 --- /dev/null +++ b/Test/test1/IfThenElse0.bpl @@ -0,0 +1,8 @@ +procedure foo() +{ + var b:bool, i:int; + + b := if i then b else b; + b := if b then b else i; + b := if b then i else i; +} diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index c6881263..dda3a0af 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -17,3 +17,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify Orderings.bpl
%BGEXE% %* /noVerify EmptyCallArgs.bpl
%BGEXE% %* /noVerify FunBody.bpl
+%BGEXE% %* /noVerify IfThenElse0.bpl
diff --git a/Test/test2/Answer b/Test/test2/Answer index 1e5a0d5f..230a8861 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -323,6 +323,16 @@ Execution trace: Implies.bpl(11,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
+
+-------------------- IfThenElse1.bpl --------------------
+IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ IfThenElse1.bpl(26,3): anon0
+IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ IfThenElse1.bpl(33,3): anon0
+
+Boogie program verifier finished with 2 verified, 2 errors
-------------------- sk_hack.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl new file mode 100644 index 00000000..8a867f50 --- /dev/null +++ b/Test/test2/IfThenElse1.bpl @@ -0,0 +1,34 @@ +type t1; + +procedure ok() +{ + var b:bool, x:int, y:int; + + assert x == if b then x else x; + assert x == if true then x else y; +} + +procedure ok2() +{ + var x:int, y:int; + var a:t1, b:t1, c:t1; + + c := if x > y then a else b; + assert c == a || c == b; + assume x > y; + assert c == a; +} + +procedure fail1() +{ + var b:bool, x:int, y:int; + + assert x == if b then x else y; +} + +procedure fail2() +{ + var b:bool, x:int, y:int; + + assert x == if false then x else y; +} diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat index 5f48a799..ab9ec103 100644 --- a/Test/test2/runtest.bat +++ b/Test/test2/runtest.bat @@ -10,7 +10,8 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl CutBackEdge.bpl False.bpl LoopInvAssume.bpl
strings-no-where.bpl strings-where.bpl
Structured.bpl Where.bpl UpdateExpr.bpl
- NeverPattern.bpl NullaryMaps.bpl Implies.bpl) do (
+ NeverPattern.bpl NullaryMaps.bpl Implies.bpl
+ IfThenElse1.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /noinfer %%f
|