Added support for stub methods. If a method definition is marked with a custom attribute [Stub], then no procedure declaration is created for it. The user must make sure to provide Boogie with a file containing the procedure declaration.

In addition, if the attribute has a string argument, [Stub("f")], then "f" is used as the nsame of the corresponding procedure instead of the encoded name computed from the method.

2 files changed, 30 insertions, 4 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 7f236ebb..bb73547a 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -549,11 +549,10 @@ namespace BytecodeTranslator
         }

         else

         {

-          string methodName = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);

           if (attrib != null)

-            call = new Bpl.CallCmd(cloc, methodName, inexpr, outvars, attrib);

+            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

           else

-            call = new Bpl.CallCmd(cloc, methodName, inexpr, outvars);

+            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

           this.StmtTraverser.StmtBuilder.Add(call);

         }

       }

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 4e51c3ec..74e095dc 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -352,13 +352,40 @@ namespace BytecodeTranslator {
             boogiePostcondition);

 

 

-        this.TranslatedProgram.TopLevelDeclarations.Add(proc);

+        string newName = null;

+        if (IsStubMethod(method, out newName)) {

+          if (newName != null) {

+            proc.Name = newName;

+          }

+        } else {

+          this.TranslatedProgram.TopLevelDeclarations.Add(proc);

+        }

         procAndFormalMap = new ProcedureInfo(proc, formalMap, this.RetVariable);

         this.declaredMethods.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Procedure;

     }

 

+    // TODO: check method's containing type in case the entire type is a stub type.

+    // TODO: do a type test, not a string test for the attribute

+    private bool IsStubMethod(IMethodReference method, out string newName) {

+      newName = null;

+      var methodDefinition = method.ResolvedMethod;

+      foreach (var a in methodDefinition.Attributes) {

+        if (TypeHelper.GetTypeName(a.Type).EndsWith("StubAttribute")) {

+          foreach (var c in a.Arguments) {

+            var mdc = c as IMetadataConstant;

+            if (mdc != null && mdc.Type.TypeCode == PrimitiveTypeCode.String) {

+              newName = (string) (mdc.Value);

+              break;

+            }

+          }

+          return true;

+        }

+      }

+      return false;

+    }

+

     public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method, bool isStatic) {

       this.FindOrCreateProcedure(method, isStatic);

       return this.declaredMethods[method];