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.

1 files changed, 2 insertions, 3 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);

         }

       }