Added option "getMeHere" so that calls to GetMeHere.Assert(e) become "assert e"

(which really could be done just by defining it that way in an assembly either
via a contract or else by inlining it). But more importantly the option causes
all assertions to be translated as assumptions. Still to do: postconditions
should be translated as "free ensures".

4 files changed, 22 insertions, 2 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index ea171b25..f2f0dde5 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -487,6 +487,19 @@ namespace BytecodeTranslator
       }

 

       Bpl.IToken methodCallToken = methodCall.Token();

+

+      if (this.sink.Options.getMeHere) {

+        // TODO: Get a method reference so this isn't a string comparison?

+        var methodName = MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None);

+        if (methodName.Equals("GetMeHere.GetMeHere.Assert")) {

+          // for now, just translate it as "assert e"

+          this.Visit(methodCall.Arguments.First());

+          Bpl.Expr e = this.TranslatedExpressions.Pop();

+          this.StmtTraverser.StmtBuilder.Add(new Bpl.AssertCmd(methodCallToken, e));

+          return;

+        }

+      }

+

       List<Bpl.Expr> inexpr;

       List<Bpl.IdentifierExpr> outvars;

       Bpl.IdentifierExpr thisExpr;

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 7a56db76..abb9a2c2 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -34,6 +34,9 @@ namespace BytecodeTranslator {
     [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]

     public bool captureState = false;

 

+    [OptionDescription("Translation should be done for Get Me Here functionality, (default: false)", ShortForm = "gmh")]

+    public bool getMeHere = false;

+

     [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]

     public List<string> libpaths = new List<string>();

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 1427b836..fc98bb9f 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -431,7 +431,7 @@ namespace BytecodeTranslator {
         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

         // The method can be generic (or have a parameter whose type is a type parameter of the method's

         // containing class) and then there can be name clashes.

-        MethodName += key.ToString();

+        //MethodName += key.ToString();

 

         if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out procInfo)) return procInfo;

 

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 015e57ce..b6fc1dfd 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -158,7 +158,11 @@ namespace BytecodeTranslator
       else {

         System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

       }

-      StmtBuilder.Add(new Bpl.AssertCmd(assertStatement.Token(), conditionExpr));

+      if (this.sink.Options.getMeHere) {

+        StmtBuilder.Add(new Bpl.AssumeCmd(assertStatement.Token(), conditionExpr));

+      } else {

+        StmtBuilder.Add(new Bpl.AssertCmd(assertStatement.Token(), conditionExpr));

+      }

     }

 

     public override void Visit(IAssumeStatement assumeStatement) {