summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.hgignore2
-rw-r--r--BCT/BytecodeTranslator/Program.cs5
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs17
-rw-r--r--Source/Dafny/Printer.cs6
-rw-r--r--Test/dafny0/Answer220
-rw-r--r--Test/dafny0/SmallTests.dfy17
-rw-r--r--Test/dafny0/runtest.bat7
7 files changed, 270 insertions, 4 deletions
diff --git a/.hgignore b/.hgignore
index 1028a0fc..06649311 100644
--- a/.hgignore
+++ b/.hgignore
@@ -11,7 +11,7 @@ syntax: regexp
^Chalice/tests/(examples|permission-model|refinements|general-tests|regressions)/.*\.bpl
Test/([^/]*)/Output
Test/([^/]*)/([^/]*)\.sx
-Test/(dafny0|dafny1|dafny2|VSI-Benchmarks|vacid0|VSComp2010|vstte2012)/(out\.cs|.*\.dll|.*\.pdb|.*\.exe|.*\.tmp)
+Test/(dafny0|dafny1|dafny2|VSI-Benchmarks|vacid0|VSComp2010|vstte2012)/(out\.cs|.*\.dll|.*\.pdb|.*\.exe|.*\.tmp.*)
Test/desktop/
^.*~$
syntax: glob
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 9a48f1f0..eaef7e40 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -66,6 +66,9 @@ namespace BytecodeTranslator {
[OptionDescription("File containing white/black list (optionally end file name with + for white list, - for black list, default is white list", ShortForm = "exempt")]
public string exemptionFile = "";
+ [OptionDescription("Instrument branches with unique counter values", ShortForm = "ib")]
+ public bool instrumentBranches = false;
+
}
public class BCT {
@@ -248,7 +251,7 @@ namespace BytecodeTranslator {
}
var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;
// The decompiler does not turn calls to Assert/Assume into Code Model nodes
- m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);
+ m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);
decompiledModules.Add(m2);
host.RegisterAsLatest(m2);
contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 424064ff..43441642 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -198,6 +198,17 @@ namespace BytecodeTranslator
StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
+
+ if (this.sink.Options.instrumentBranches) {
+ var tok = conditionalStatement.Token();
+ thenTraverser.StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))
+ );
+ elseTraverser.StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))
+ );
+ }
+
condTraverser.Traverse(conditionalStatement.Condition);
thenTraverser.Traverse(conditionalStatement.TrueBranch);
elseTraverser.Traverse(conditionalStatement.FalseBranch);
@@ -225,6 +236,12 @@ namespace BytecodeTranslator
}
+ private static int counter = 0;
+ internal int NextUniqueNumber() {
+ return counter++;
+ }
+
+
/// <summary>
///
/// </summary>
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index cf8be27e..4290953b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -976,9 +976,13 @@ namespace Microsoft.Dafny {
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
+ bool containsNestedNot = e.E is ParensExpression &&
+ ((ParensExpression)e.E).E is UnaryExpr &&
+ ((UnaryExpr)((ParensExpression)e.E).E).Op == UnaryExpr.Opcode.Not;
+
if (parensNeeded) { wr.Write("("); }
wr.Write(op);
- PrintExpr(e.E, opBindingStrength, false, parensNeeded || isRightmost, -1);
+ PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, -1);
if (parensNeeded) { wr.Write(")"); }
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5e1428c2..da1055c8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -247,7 +247,7 @@ SmallTests.dfy(411,41): Error: possible violation of function postcondition
Execution trace:
(0,0): anon6_Else
-Dafny program verifier finished with 56 verified, 21 errors
+Dafny program verifier finished with 58 verified, 21 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -1342,3 +1342,221 @@ Execution trace:
(0,0): anon11_Then
Dafny program verifier finished with 13 verified, 2 errors
+
+-------------------- SmallTests.dfy --------------------
+SmallTests.dfy(30,11): Error: index out of range
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(61,36): Error: possible division by zero
+Execution trace:
+ (0,0): anon12_Then
+SmallTests.dfy(62,51): Error: possible division by zero
+Execution trace:
+ (0,0): anon12_Else
+ (0,0): anon3
+ (0,0): anon13_Else
+SmallTests.dfy(63,22): Error: target object may be null
+Execution trace:
+ (0,0): anon12_Then
+ (0,0): anon3
+ (0,0): anon13_Then
+ (0,0): anon6
+SmallTests.dfy(82,24): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(81,5): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ (0,0): anon10_Then
+SmallTests.dfy(116,5): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+ (0,0): anon3
+SmallTests.dfy(129,9): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+SmallTests.dfy(131,9): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+SmallTests.dfy(171,9): Error: assignment may update an object field not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon22_Else
+ (0,0): anon5
+ (0,0): anon24_Else
+ (0,0): anon11
+ (0,0): anon26_Else
+ (0,0): anon16
+ (0,0): anon28_Then
+ (0,0): anon29_Then
+ (0,0): anon19
+SmallTests.dfy(199,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Then
+SmallTests.dfy(206,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Else
+ (0,0): anon3
+ (0,0): anon13_Then
+SmallTests.dfy(226,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Else
+ (0,0): anon3
+ (0,0): anon13_Else
+ (0,0): anon6
+ (0,0): anon14_Then
+ (0,0): anon11
+SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.
+SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(266,19): anon3_Else
+ (0,0): anon2
+SmallTests.dfy(376,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(386,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
+SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Else
+ (0,0): anon11
+ (0,0): anon23_Then
+ (0,0): anon24_Then
+ (0,0): anon15
+ (0,0): anon25_Else
+SmallTests.dfy(347,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon7
+SmallTests.dfy(354,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
+SmallTests.dfy(411,41): Error: possible violation of function postcondition
+Execution trace:
+ (0,0): anon6_Else
+
+Dafny program verifier finished with 58 verified, 21 errors
+out.tmp.dfy(33,11): Error: index out of range
+Execution trace:
+ (0,0): anon0
+out.tmp.dfy(69,37): Error: possible division by zero
+Execution trace:
+ (0,0): anon12_Then
+out.tmp.dfy(70,52): Error: possible division by zero
+Execution trace:
+ (0,0): anon12_Else
+ (0,0): anon3
+ (0,0): anon13_Else
+out.tmp.dfy(71,22): Error: target object may be null
+Execution trace:
+ (0,0): anon12_Then
+ (0,0): anon3
+ (0,0): anon13_Then
+ (0,0): anon6
+out.tmp.dfy(88,24): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ out.tmp.dfy(87,5): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ (0,0): anon10_Then
+out.tmp.dfy(122,5): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+ (0,0): anon3
+out.tmp.dfy(135,9): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+out.tmp.dfy(137,9): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+out.tmp.dfy(177,9): Error: assignment may update an object field not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon22_Else
+ (0,0): anon5
+ (0,0): anon24_Else
+ (0,0): anon11
+ (0,0): anon26_Else
+ (0,0): anon16
+ (0,0): anon28_Then
+ (0,0): anon29_Then
+ (0,0): anon19
+out.tmp.dfy(202,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Then
+out.tmp.dfy(208,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Else
+ (0,0): anon3
+ (0,0): anon13_Then
+out.tmp.dfy(229,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Else
+ (0,0): anon3
+ (0,0): anon13_Else
+ (0,0): anon6
+ (0,0): anon14_Then
+ (0,0): anon11
+out.tmp.dfy(266,24): Error BP5002: A precondition for this call might not hold.
+out.tmp.dfy(247,30): Related location: This is the precondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ out.tmp.dfy(263,19): anon3_Else
+ (0,0): anon2
+out.tmp.dfy(286,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+out.tmp.dfy(296,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+out.tmp.dfy(306,6): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
+out.tmp.dfy(422,3): Error BP5003: A postcondition might not hold on this return path.
+out.tmp.dfy(416,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Else
+ (0,0): anon11
+ (0,0): anon23_Then
+ (0,0): anon24_Then
+ (0,0): anon15
+ (0,0): anon25_Else
+out.tmp.dfy(446,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon7
+out.tmp.dfy(451,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+out.tmp.dfy(461,4): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
+out.tmp.dfy(470,41): Error: possible violation of function postcondition
+Execution trace:
+ (0,0): anon6_Else
+
+Dafny program verifier finished with 58 verified, 21 errors
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 5fabe354..914e228e 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -518,3 +518,20 @@ class AttributeTests {
}
}
}
+
+// ----------------------- Pretty printing of !(!expr) --------
+
+static method TestNotNot()
+{
+ assert !(!true); // Shouldn't pretty print as "!!true".
+
+ assert !(true == false);
+
+ assert !(if true then false else false);
+
+ assert !if true then false else false;
+
+ assert !if !(!true) then false else false;
+
+ assert true == !(!true);
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f1fc0828..7761b47d 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -25,3 +25,10 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
)
+
+for %%f in (SmallTests.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
+ %DAFNY_EXE% /compile:0 %* out.tmp.dfy
+)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:08:50 +0000