diff options
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 3 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 3 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 12 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 30 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 30 |
6 files changed, 81 insertions, 3 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index b2d23777..64f4777f 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -687,8 +687,10 @@ namespace BytecodeTranslator this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion));
}
- Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
- this.StmtTraverser.RaiseException(expr);
+ if (this.sink.Options.modelExceptions) {
+ Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
+ this.StmtTraverser.RaiseException(expr);
+ }
} finally {
// TODO move away phone related code from the translation, it would be better to have 2 or more translation phases
if (PhoneCodeHelper.instance().PhonePlugin != null) {
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index e65ef6a9..c95d69e5 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -532,7 +532,8 @@ namespace BytecodeTranslator { foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
vars.Add(v);
}
- vars.Add(procInfo.LocalExcVariable);
+ if (this.sink.Options.modelExceptions)
+ vars.Add(procInfo.LocalExcVariable);
vars.Add(procInfo.LabelVariable);
Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
#endregion
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index ffee13eb..81f630aa 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -38,6 +38,9 @@ namespace BytecodeTranslator { [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]
public bool captureState = false;
+ [OptionDescription("Model exceptional control flow, (default: true)", ShortForm = "e")]
+ public bool modelExceptions = true;
+
[OptionDescription("Translation should be done for Get Me Here functionality, (default: false)", ShortForm = "gmh")]
public bool getMeHere = false;
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 49f932ec..745c2fff 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -518,6 +518,14 @@ namespace BytecodeTranslator }
public override void TraverseChildren(ITryCatchFinallyStatement tryCatchFinallyStatement) {
+
+ if (!this.sink.Options.modelExceptions) {
+ this.Traverse(tryCatchFinallyStatement.TryBody);
+ if (tryCatchFinallyStatement.FinallyBody != null)
+ this.Traverse(tryCatchFinallyStatement.FinallyBody);
+ return;
+ }
+
this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InTry));
this.Traverse(tryCatchFinallyStatement.TryBody);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
@@ -572,6 +580,10 @@ namespace BytecodeTranslator }
public override void TraverseChildren(IThrowStatement throwStatement) {
+ if (!this.sink.Options.modelExceptions) {
+ StmtBuilder.Add(new Bpl.AssumeCmd(throwStatement.Token(), Bpl.Expr.False));
+ return;
+ }
ExpressionTraverser exceptionTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
exceptionTraverser.Traverse(throwStatement.Exception);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), exceptionTraverser.TranslatedExpressions.Pop()));
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 0fe003ae..0a2a515a 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -997,6 +997,36 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
+{
+ var xs: Ref;
+ var $localExc: Ref;
+ var $label: int;
+
+ xs := xs$in;
+ assume {:breadcrumb 13} true;
+ if (xs != null)
+ {
+ }
+ else
+ {
+ }
+
+ if ((if xs != null then $ArrayLength(xs) > 0 else false))
+ {
+ assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assume $this != null;
+ assume xs != null;
+ $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
+ }
+ else
+ {
+ }
+}
+
+
+
procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);
free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 5dfc582e..b552ee36 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -983,6 +983,36 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
+{
+ var xs: Ref;
+ var $localExc: Ref;
+ var $label: int;
+
+ xs := xs$in;
+ assume {:breadcrumb 13} true;
+ if (xs != null)
+ {
+ }
+ else
+ {
+ }
+
+ if ((if xs != null then $ArrayLength(xs) > 0 else false))
+ {
+ assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assume $this != null;
+ assume xs != null;
+ $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
+ }
+ else
+ {
+ }
+}
+
+
+
procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);
free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);
|