diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 23 | ||||
| -rw-r--r-- | Source/Dafny/DafnyPipeline.csproj | 45 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 14 |
5 files changed, 68 insertions, 26 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 218f95e5..0a553036 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -752,7 +752,7 @@ namespace Microsoft.Dafny { Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(ctors));
- Contract.Invariant(1 <= ctors.Count);
+ Contract.Requires(1 <= ctors.Count);
Ctors = ctors;
}
}
@@ -871,8 +871,8 @@ namespace Microsoft.Dafny { void ObjectInvariant() {
Contract.Invariant(Expr != null);
Contract.Invariant(cce.NonNullElements(Toks));
- Contract.Invariant(cce.NonNullElements(Formals));
- Contract.Invariant(cce.NonNullElements(Refined));
+ Contract.Invariant(Formals == null || cce.NonNullElements(Formals));
+ Contract.Invariant(Refined == null || cce.NonNullElements(Refined));
}
@@ -1298,12 +1298,13 @@ namespace Microsoft.Dafny { public Statement TargetStmt; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(TargetLabel == null || 1 <= BreakCount);
+ Contract.Invariant(TargetLabel != null || 1 <= BreakCount);
}
public BreakStmt(IToken tok, string targetLabel)
: base(tok) {
Contract.Requires(tok != null);
+ Contract.Requires(targetLabel != null);
this.TargetLabel = targetLabel;
}
public BreakStmt(IToken tok, int breakCount)
@@ -1639,13 +1640,11 @@ namespace Microsoft.Dafny { public IfStmt(IToken tok, Expression guard, Statement thn, Statement els)
: base(tok) {
Contract.Requires(tok != null);
- Contract.Requires(guard != null);
Contract.Requires(thn != null);
Contract.Requires(els == null || els is BlockStmt || els is IfStmt);
this.Guard = guard;
this.Thn = thn;
this.Els = els;
-
}
}
@@ -1875,9 +1874,15 @@ namespace Microsoft.Dafny { Contract.Invariant(tok != null);
}
+ [Pure]
+ public bool WasResolved()
+ {
+ return Type != null;
+ }
+
public Expression Resolved {
get {
- Contract.Requires(type != null); // should be called only on resolved expressions; this approximates that precondition
+ Contract.Requires(WasResolved()); // should be called only on resolved expressions; this approximates that precondition
Expression r = this;
while (true) {
var rr = r as ConcreteSyntaxExpression;
@@ -1899,7 +1904,7 @@ namespace Microsoft.Dafny { [NoDefaultContract] // no particular validity of 'this' is required, except that it not be committed
set {
Contract.Requires(cce.IsValid(this));
- Contract.Requires(Type == null); // set it only once
+ Contract.Requires(!WasResolved()); // set it only once
Contract.Requires(value != null);
//modifies type;
type = value.Normalize();
@@ -2907,7 +2912,7 @@ namespace Microsoft.Dafny { Contract.Requires(operands != null);
Contract.Requires(operators != null);
Contract.Requires(desugaring != null);
- Contract.Requires(operators.Count == operators.Count + 1);
+ Contract.Requires(operands.Count == operators.Count + 1);
Operands = operands;
Operators = operators;
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index 6a15b1f7..40a8cacc 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -75,6 +75,10 @@ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
@@ -85,6 +89,43 @@ <WarningLevel>4</WarningLevel>
<CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
</PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Checked\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
<ItemGroup>
<Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
@@ -154,4 +195,4 @@ <Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project>
\ No newline at end of file diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 34fcb740..97324ef9 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -723,7 +723,7 @@ namespace Microsoft.Dafny { }
wr.Write(")");
}
- bool parensNeeded = !isLastCase && mc.Body.Resolved is MatchExpr;
+ bool parensNeeded = !isLastCase && mc.Body.WasResolved() && mc.Body.Resolved is MatchExpr;
if (parensNeeded) {
wr.WriteLine(" => (");
} else {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5e2bc911..b9f5e7e6 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -935,9 +935,9 @@ namespace Microsoft.Dafny { Contract.Requires(proxy != null);
Contract.Requires(t != null);
Contract.Requires(proxy.T == null);
- Contract.Requires((t is TypeProxy)|| ((TypeProxy)t).T == null);
+ Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);
//modifies proxy.T, ((TypeProxy)t).T; // might also change t.T if t is a proxy
- Contract.Ensures(Contract.Result<bool>() || proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null));
+ Contract.Ensures(Contract.Result<bool>() == (proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null)));
if (proxy == t) {
// they are already in the same equivalence class
return true;
@@ -1845,7 +1845,7 @@ namespace Microsoft.Dafny { Contract.Assume(lhs.Type != null); // a sanity check that LHSs have already been resolved
}
// resolve arguments
- if (!s.IsGhost) {
+ if (!s.IsGhost && s.Receiver.WasResolved()) {
CheckIsNonGhost(s.Receiver);
}
int j = 0;
@@ -2791,7 +2791,7 @@ namespace Microsoft.Dafny { void CheckIsNonGhost(Expression expr) {
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
- Contract.Requires(expr.Type != null); // this check approximates the requirement that "expr" be resolved
+ Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved
if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
@@ -3505,7 +3505,7 @@ namespace Microsoft.Dafny { Contract.Requires(currentClass != null);
Contract.Ensures(expr.Type != null);
- if (expr is ThisExpr) {
+ if (expr is ThisExpr && !expr.WasResolved()) {
// Allow 'this' here, regardless of scope.AllowInstance. The caller is responsible for
// making sure 'this' does not really get used when it's not available.
expr.Type = GetThisType(expr.tok, currentClass);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 17df4e06..3ec3c291 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2751,10 +2751,9 @@ namespace Microsoft.Dafny { public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)
{
- Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);
- if (subst.ContainsKey(node.Name))
+ if (node != null && subst.ContainsKey(node.Name))
return subst[node.Name];
else
return base.VisitIdentifierExpr(node);
@@ -3582,7 +3581,7 @@ namespace Microsoft.Dafny { void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,
Bpl.StmtListBuilder builder, VariableSeq locals, ExpressionTranslator etran) {
Contract.Requires(alternatives != null);
- Contract.Requires((elseCase0 == null) == (elseCase1 == null)); // ugly way of doing a type union
+ Contract.Requires((elseCase0 != null) == (elseCase1 == null)); // ugly way of doing a type union
Contract.Requires(builder != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
@@ -3665,7 +3664,7 @@ namespace Microsoft.Dafny { Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
Contract.Requires(tok != null);
- Contract.Requires((dafnyReceiver == null) != (bReceiver == null));
+ Contract.Requires((dafnyReceiver != null) || (bReceiver != null));
Contract.Requires(method != null);
Contract.Requires(cce.NonNullElements(Args));
Contract.Requires(cce.NonNullElements(Lhss));
@@ -4515,7 +4514,7 @@ namespace Microsoft.Dafny { public readonly string This;
public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.
readonly Function applyLimited_CurrentFunction;
- readonly int layerOffset = 0;
+ public readonly int layerOffset = 0;
public int Statistics_FunctionCount = 0;
[ContractInvariantMethod]
void ObjectInvariant()
@@ -4564,7 +4563,6 @@ namespace Microsoft.Dafny { Contract.Requires(translator != null);
Contract.Requires(predef != null);
Contract.Requires(heap != null);
- Contract.Requires(applyLimited_CurrentFunction != null);
this.translator = translator;
this.predef = predef;
this.HeapExpr = heap;
@@ -6271,7 +6269,6 @@ namespace Microsoft.Dafny { static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
- Contract.Requires(receiverReplacement != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
@@ -6436,8 +6433,7 @@ namespace Microsoft.Dafny { static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullElements(elist));
- Contract.Requires((receiverReplacement == null) == (substMap == null));
- Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
List<Expression> newElist = null; // initialized lazily
|