diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 6 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 29 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 273 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 57 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 36 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/version.cs | 18 | ||||
| -rw-r--r-- | Source/version.ssc | 18 |
9 files changed, 256 insertions, 194 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index af0926fe..95078433 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -19,6 +19,8 @@ </FileUpgradeFlags>
<OldToolsVersion>3.5</OldToolsVersion>
<UpgradeBackupLocation />
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <TargetFrameworkProfile />
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
@@ -31,17 +33,15 @@ <MapFileExtensions>true</MapFileExtensions>
<ApplicationRevision>0</ApplicationRevision>
<ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile />
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DefineConstants>TRACE;DEBUG</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 8f2d0c68..4a9c531b 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -136,6 +136,7 @@ namespace Microsoft.Boogie { public bool NoTypecheck = false;
public bool OverlookBoogieTypeErrors = false;
public bool Verify = true;
+ public bool DisallowSoundnessCheating = false;
public bool TraceVerify = false;
public int /*(0:3)*/ ErrorTrace = 1;
public bool IntraproceduralInfer = true;
@@ -143,6 +144,7 @@ namespace Microsoft.Boogie { public bool UseUncheckedContracts = false;
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
+ public string Z3ExecutablePath = null;
private bool noConsistencyChecks = false;
public bool NoConsistencyChecks {
@@ -159,6 +161,7 @@ namespace Microsoft.Boogie { public string DafnyPrelude = null;
public string DafnyPrintFile = null;
public bool Compile = true;
+ public bool ForceCompile = false;
public enum ProverWarnings {
None,
@@ -712,8 +715,18 @@ namespace Microsoft.Boogie { case "-compile":
case "/compile": {
int compile = 0;
- if (ps.GetNumericArgument(ref compile, 2)) {
- Compile = compile == 1;
+ if (ps.GetNumericArgument(ref compile, 3)) {
+ Compile = compile == 1 || compile == 2;
+ ForceCompile = compile == 2;
+ }
+ break;
+ }
+
+ case "-noCheating":
+ case "/noCheating": {
+ int cheat = 0; // 0 is default, allows cheating
+ if (ps.GetNumericArgument(ref cheat, 2)) {
+ DisallowSoundnessCheating = cheat == 1;
}
break;
}
@@ -1376,6 +1389,13 @@ namespace Microsoft.Boogie { }
break;
+ case "-z3exe":
+ case "/z3exe":
+ if (ps.ConfirmArgumentCount(1)) {
+ Z3ExecutablePath = args[ps.i];
+ }
+ break;
+
default:
Contract.Assume(true);
bool option = false;
@@ -2097,6 +2117,10 @@ namespace Microsoft.Boogie { /compile:<n> : 0 - do not compile Dafny program
1 (default) - upon successful verification of the Dafny
program, compile Dafny program to C# program out.cs
+ 2 - always attempt to compile Dafny program to C# program
+ out.cs, regardless of verification outcome
+ /noCheating:<n> : 0 (default) - allow assume statements and free invariants
+ 1 - treat all assumptions as asserts, and drop free.
---- Boogie options --------------------------------------------------------
@@ -2319,6 +2343,7 @@ namespace Microsoft.Boogie { /z3types : generate multi-sorted VC that make use of Z3 types
/z3lets:<n> : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
3 - (default) any
+ /z3exe:<path> : path to Z3 executable
");
}
}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0b3435e8..4868be10 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1463,7 +1463,7 @@ namespace Microsoft.Dafny { {
public readonly List<Expression> Lhss;
public readonly List<AssignmentRhs> Rhss;
- public bool secretlyReturnStatment;
+ public readonly bool CanMutateKnownState;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Lhss));
@@ -1478,9 +1478,9 @@ namespace Microsoft.Dafny { Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
Lhss = lhss;
Rhss = rhss;
- secretlyReturnStatment = false;
+ CanMutateKnownState = false;
}
- public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool srs)
+ public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)
: base(tok)
{
Contract.Requires(tok != null);
@@ -1489,7 +1489,7 @@ namespace Microsoft.Dafny { Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
Lhss = lhss;
Rhss = rhss;
- secretlyReturnStatment = srs;
+ CanMutateKnownState = mutate;
}
}
@@ -1678,7 +1678,6 @@ namespace Microsoft.Dafny { public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;
public readonly List<Expression/*!*/>/*!*/ Decreases;
public readonly List<FrameExpression/*!*/>/*!*/ Mod;
- public readonly bool explictModifies;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Invariants));
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 24732dac..780e04d9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1232,141 +1232,15 @@ namespace Microsoft.Dafny { i++;
}
s.hiddenUpdate = new UpdateStmt(s.Tok, formals, s.rhss, true);
- ResolveStatement(s.hiddenUpdate, specContextOnly, method);
// resolving the update statement will check for return statement specifics.
+ ResolveStatement(s.hiddenUpdate, specContextOnly, method);
}
}
else {// this is a regular return statement.
s.hiddenUpdate = null;
}
} else if (stmt is UpdateStmt) {
- var s = (UpdateStmt)stmt;
- int prevErrorCount = ErrorCount;
- // First, resolve all LHS's and expression-looking RHS's.
- SeqSelectExpr arrayRangeLhs = null;
- foreach (var lhs in s.Lhss) {
- if (lhs is SeqSelectExpr) {
- var sse = (SeqSelectExpr)lhs;
- ResolveSeqSelectExpr(sse, true, true);
- if (arrayRangeLhs == null && !sse.SelectOne) {
- arrayRangeLhs = sse;
- }
- } else {
- ResolveExpression(lhs, true);
- }
- }
- IToken firstEffectfulRhs = null;
- CallRhs callRhs = null;
- // Resolve RHSs
- foreach (var rhs in s.Rhss) {
- bool isEffectful;
- if (rhs is TypeRhs) {
- var tr = (TypeRhs)rhs;
- ResolveTypeRhs(tr, stmt, specContextOnly, method);
- isEffectful = tr.InitCall != null;
- } else if (rhs is HavocRhs) {
- isEffectful = false;
- } else {
- var er = (ExprRhs)rhs;
- if (er.Expr is IdentifierSequence) {
- var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);
- isEffectful = cRhs != null;
- callRhs = callRhs ?? cRhs;
- } else if (er.Expr is FunctionCallExpr) {
- var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);
- isEffectful = cRhs != null;
- callRhs = callRhs ?? cRhs;
- } else {
- ResolveExpression(er.Expr, true);
- isEffectful = false;
- }
- }
- if (isEffectful && firstEffectfulRhs == null) {
- firstEffectfulRhs = rhs.Tok;
- }
- }
- // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
- var lhsNameSet = new Dictionary<string, object>();
- foreach (var lhs in s.Lhss) {
- var ie = lhs.Resolved as IdentifierExpr;
- if (ie != null) {
- if (lhsNameSet.ContainsKey(ie.Name)) {
- Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");
- } else {
- lhsNameSet.Add(ie.Name, null);
- }
- }
- }
-
- // figure out what kind of UpdateStmt this is
- if (firstEffectfulRhs == null) {
- if (s.Lhss.Count == 0) {
- Contract.Assert(s.Rhss.Count == 1); // guaranteed by the parser
- Error(s, "expected method call, found expression");
- } else if (s.Lhss.Count != s.Rhss.Count) {
- Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
- } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {
- Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");
- } else if (ErrorCount == prevErrorCount) {
- // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)
- for (int i = 0; i < s.Lhss.Count; i++) {
- var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);
- s.ResolvedStatements.Add(a);
- }
- }
- } else {
- if (s.secretlyReturnStatment) {
- if (1 < s.Rhss.Count)
- Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
- else { // it might be ok, if it is a TypeExpr
- Contract.Assert(s.Rhss.Count == 1);
- if (callRhs != null) {
- Error(callRhs.Tok, "cannot have method call in return statement.");
- }
- else {
- // we have a TypeExpr
- Contract.Assert(s.Rhss[0] is TypeRhs);
- var tr = (TypeRhs)s.Rhss[0];
- Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
- if (tr.CanAffectPreviouslyKnownExpressions) {
- Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
- }
- }
- }
- }
- else {
- // if there was an effectful RHS, that must be the only RHS
- if (s.Rhss.Count != 1) {
- Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
- } else if (arrayRangeLhs != null) {
- Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
- } else if (callRhs == null) {
- // must be a single TypeRhs
- if (s.Lhss.Count != 1) {
- Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
- Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
- } else if (ErrorCount == prevErrorCount) {
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);
- s.ResolvedStatements.Add(a);
- }
- } else {
- // a call statement
- if (ErrorCount == prevErrorCount) {
- var resolvedLhss = new List<Expression>();
- foreach (var ll in s.Lhss) {
- resolvedLhss.Add(ll.Resolved);
- }
- var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
- s.ResolvedStatements.Add(a);
- }
- }
- }
- }
-
- foreach (var a in s.ResolvedStatements) {
- ResolveStatement(a, specContextOnly, method);
- }
- // end of UpdateStmt
+ ResolveUpdateStmt((UpdateStmt)stmt, specContextOnly, method);
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
foreach (var vd in s.Lhss) {
@@ -1748,6 +1622,149 @@ namespace Microsoft.Dafny { }
}
+ private void ResolveUpdateStmt(UpdateStmt s, bool specContextOnly, Method method)
+ {
+ int prevErrorCount = ErrorCount;
+ // First, resolve all LHS's and expression-looking RHS's.
+ SeqSelectExpr arrayRangeLhs = null;
+ foreach (var lhs in s.Lhss) {
+ if (lhs is SeqSelectExpr) {
+ var sse = (SeqSelectExpr)lhs;
+ ResolveSeqSelectExpr(sse, true, true);
+ if (arrayRangeLhs == null && !sse.SelectOne) {
+ arrayRangeLhs = sse;
+ }
+ }
+ else {
+ ResolveExpression(lhs, true);
+ }
+ }
+ IToken firstEffectfulRhs = null;
+ CallRhs callRhs = null;
+ // Resolve RHSs
+ foreach (var rhs in s.Rhss) {
+ bool isEffectful;
+ if (rhs is TypeRhs) {
+ var tr = (TypeRhs)rhs;
+ ResolveTypeRhs(tr, s, specContextOnly, method);
+ isEffectful = tr.InitCall != null;
+ }
+ else if (rhs is HavocRhs) {
+ isEffectful = false;
+ }
+ else {
+ var er = (ExprRhs)rhs;
+ if (er.Expr is IdentifierSequence) {
+ var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+ }
+ else if (er.Expr is FunctionCallExpr) {
+ var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+ }
+ else {
+ ResolveExpression(er.Expr, true);
+ isEffectful = false;
+ }
+ }
+ if (isEffectful && firstEffectfulRhs == null) {
+ firstEffectfulRhs = rhs.Tok;
+ }
+ }
+ // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
+ var lhsNameSet = new Dictionary<string, object>();
+ foreach (var lhs in s.Lhss) {
+ var ie = lhs.Resolved as IdentifierExpr;
+ if (ie != null) {
+ if (lhsNameSet.ContainsKey(ie.Name)) {
+ Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");
+ }
+ else {
+ lhsNameSet.Add(ie.Name, null);
+ }
+ }
+ }
+
+ // figure out what kind of UpdateStmt this is
+ if (firstEffectfulRhs == null) {
+ if (s.Lhss.Count == 0) {
+ Contract.Assert(s.Rhss.Count == 1); // guaranteed by the parser
+ Error(s, "expected method call, found expression");
+ }
+ else if (s.Lhss.Count != s.Rhss.Count) {
+ Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
+ }
+ else if (arrayRangeLhs != null && s.Lhss.Count != 1) {
+ Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");
+ }
+ else if (ErrorCount == prevErrorCount) {
+ // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)
+ for (int i = 0; i < s.Lhss.Count; i++) {
+ var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ }
+ else {
+ if (s.CanMutateKnownState) {
+ if (1 < s.Rhss.Count)
+ Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
+ else { // it might be ok, if it is a TypeExpr
+ Contract.Assert(s.Rhss.Count == 1);
+ if (callRhs != null) {
+ Error(callRhs.Tok, "cannot have method call in return statement.");
+ }
+ else {
+ // we have a TypeExpr
+ Contract.Assert(s.Rhss[0] is TypeRhs);
+ var tr = (TypeRhs)s.Rhss[0];
+ Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
+ if (tr.CanAffectPreviouslyKnownExpressions) {
+ Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
+ }
+ }
+ }
+ }
+ else {
+ // if there was an effectful RHS, that must be the only RHS
+ if (s.Rhss.Count != 1) {
+ Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
+ }
+ else if (arrayRangeLhs != null) {
+ Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
+ }
+ else if (callRhs == null) {
+ // must be a single TypeRhs
+ if (s.Lhss.Count != 1) {
+ Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
+ Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
+ }
+ else if (ErrorCount == prevErrorCount) {
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ else {
+ // a call statement
+ if (ErrorCount == prevErrorCount) {
+ var resolvedLhss = new List<Expression>();
+ foreach (var ll in s.Lhss) {
+ resolvedLhss.Add(ll.Resolved);
+ }
+ var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ }
+ }
+
+ foreach (var a in s.ResolvedStatements) {
+ ResolveStatement(a, specContextOnly, method);
+ }
+ }
+
bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {
Contract.Requires(alternatives != null);
Contract.Requires(method != null);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e16470c3..d1c77122 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2517,19 +2517,20 @@ namespace Microsoft.Dafny { if (!wellformednessProc) {
string comment = "user-defined preconditions";
foreach (MaybeFreeExpression p in m.Req) {
- if (p.IsFree) {
+ if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
}
}
comment = null;
}
comment = "user-defined postconditions";
if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) {
- if (p.IsFree) {
+ if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
@@ -3001,27 +3002,31 @@ namespace Microsoft.Dafny { Contract.Requires(locals != null);
Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
- if (stmt is AssertStmt) {
- AddComment(builder, stmt, "assert statement");
- AssertStmt s = (AssertStmt)stmt;
- TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
- bool splitHappened;
- var ss = TrSplitExpr(s.Expr, etran, out splitHappened);
- if (!splitHappened) {
- builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));
- } else {
- foreach (var split in ss) {
- if (!split.IsFree) {
- builder.Add(AssertNS(split.E.tok, split.E, "assertion violation"));
+ if (stmt is PredicateStmt) {
+ if (stmt is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
+ AddComment(builder, stmt, "assert statement");
+ PredicateStmt s = (PredicateStmt)stmt;
+ TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
+ bool splitHappened;
+ var ss = TrSplitExpr(s.Expr, etran, out splitHappened);
+ if (!splitHappened) {
+ builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));
+ }
+ else {
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ builder.Add(AssertNS(split.E.tok, split.E, "assertion violation"));
+ }
}
+ builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
}
+ }
+ else if (stmt is AssumeStmt) {
+ AddComment(builder, stmt, "assume statement");
+ AssumeStmt s = (AssumeStmt)stmt;
+ TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
}
- } else if (stmt is AssumeStmt) {
- AddComment(builder, stmt, "assume statement");
- AssumeStmt s = (AssumeStmt)stmt;
- TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
- builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
} else if (stmt is PrintStmt) {
AddComment(builder, stmt, "print statement");
PrintStmt s = (PrintStmt)stmt;
@@ -3030,7 +3035,7 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);
}
}
-
+
} else if (stmt is BreakStmt) {
AddComment(builder, stmt, "break statement");
var s = (BreakStmt)stmt;
@@ -3100,11 +3105,11 @@ namespace Microsoft.Dafny { Bpl.Expr wh = GetWhereClause(stmt.Tok, new Bpl.IdentifierExpr(stmt.Tok, s.UniqueName, varType), s.Type, etran);
Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.UniqueName, varType, wh));
locals.Add(var);
-
+
} else if (stmt is CallStmt) {
AddComment(builder, stmt, "call statement");
TrCallStmt((CallStmt)stmt, builder, locals, etran, null);
-
+
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
TrStmt(ss, builder, locals, etran);
@@ -3201,7 +3206,7 @@ namespace Microsoft.Dafny { oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));
}
oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
-
+
// range
Bpl.Expr qr = new Bpl.ForallExpr(s.Range.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(s.Range, etran)));
builder.Add(AssertNS(s.Range.tok, qr, "range expression must be well defined"));
@@ -3209,7 +3214,7 @@ namespace Microsoft.Dafny { // sequence of asserts and assumes and uses
foreach (PredicateStmt ps in s.BodyPrefix) {
- if (ps is AssertStmt) {
+ if (ps is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));
builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined")); // totality check
bool splitHappened;
@@ -3249,7 +3254,7 @@ namespace Microsoft.Dafny { Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
}
-
+
// Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
@@ -3407,7 +3412,7 @@ namespace Microsoft.Dafny { invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));
- if (loopInv.IsFree) {
+ if (loopInv.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
} else {
bool splitHappened;
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 91e33ea9..73f7fc71 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -166,24 +166,14 @@ namespace Microsoft.Boogie PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
switch (oc) {
case PipelineOutcome.VerificationCompleted:
- if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) {
- string targetFilename = "out.cs";
- using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
- Dafny.Compiler compiler = new Dafny.Compiler(target);
- compiler.Compile(dafnyProgram);
- WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- if (compiler.ErrorCount == 0) {
- Console.WriteLine("Compiled program written to {0}", targetFilename);
- } else {
- Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
- }
- }
- } else {
- WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- }
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if ((CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) || CommandLineOptions.Clo.ForceCompile)
+ CompileDafnyProgram(dafnyProgram);
break;
case PipelineOutcome.Done:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if (CommandLineOptions.Clo.ForceCompile)
+ CompileDafnyProgram(dafnyProgram);
break;
default:
// error has already been reported to user
@@ -192,7 +182,21 @@ namespace Microsoft.Boogie }
}
}
-
+
+ private static void CompileDafnyProgram(Dafny.Program dafnyProgram)
+ {
+ string targetFilename = "out.cs";
+ using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
+ Dafny.Compiler compiler = new Dafny.Compiler(target);
+ compiler.Compile(dafnyProgram);
+ if (compiler.ErrorCount == 0) {
+ Console.WriteLine("Compiled program written to {0}", targetFilename);
+ }
+ else {
+ Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
+ }
+ }
+ }
static void PrintBplFile (string filename, Program program, bool allowPrintDesugaring)
{
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 95d8950a..497911ab 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -239,6 +239,10 @@ namespace Microsoft.Boogie.Simplify { Contract.Requires(proverExe != null);
Contract.Ensures(_proverPath != null);
+ if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
+ _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
+ }
+
if (_proverPath == null) {
// Initialize '_proverPath'
_proverPath = Path.Combine(CodebaseString(), proverExe);
diff --git a/Source/version.cs b/Source/version.cs index 2804c330..fd211b1c 100644 --- a/Source/version.cs +++ b/Source/version.cs @@ -1,8 +1,12 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+// ==++==
+//
+//
+//
+// ==--==
+// Warning: Automatically generated file. DO NOT EDIT
+// Generated at Dienstag, 5. Juli 2011 11:26:45
+
using System.Reflection;
-[assembly: AssemblyVersion("2.0.0.0")]
-[assembly: AssemblyFileVersion("2.0.0.0")]
+[assembly: AssemblyVersion("2.2.30705.1126")]
+[assembly: AssemblyFileVersion("2.2.30705.1126")]
+
diff --git a/Source/version.ssc b/Source/version.ssc index 2804c330..fd211b1c 100644 --- a/Source/version.ssc +++ b/Source/version.ssc @@ -1,8 +1,12 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+// ==++==
+//
+//
+//
+// ==--==
+// Warning: Automatically generated file. DO NOT EDIT
+// Generated at Dienstag, 5. Juli 2011 11:26:45
+
using System.Reflection;
-[assembly: AssemblyVersion("2.0.0.0")]
-[assembly: AssemblyFileVersion("2.0.0.0")]
+[assembly: AssemblyVersion("2.2.30705.1126")]
+[assembly: AssemblyFileVersion("2.2.30705.1126")]
+
|