Merge

22 files changed, 522 insertions, 194 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 8e5170b2..47c68419 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -33,6 +33,27 @@ namespace BytecodeTranslator
 

     private bool contractContext;

 

+    private Bpl.Expr FindOrCreateTypeReferenceInCodeContext(ITypeReference typeReference) {

+      return this.sink.FindOrCreateTypeReference(typeReference, true);

+

+      IGenericTypeParameter gtp = typeReference as IGenericTypeParameter;

+      if (gtp != null) {

+        var selectorName = gtp.Name.Value;

+        selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);

+        var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);

+        typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

+        var funcName = String.Format("{0}#{1}", selectorName, typeName);

+        Bpl.IToken tok = Bpl.Token.NoToken;

+        var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.sink.Heap.TypeType)));

+        var funcCall = new Bpl.FunctionCall(identExpr);

+        var thisArg = new Bpl.IdentifierExpr(tok, this.sink.ThisVariable);

+        var dynType = this.sink.Heap.DynamicType(thisArg);

+        var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));

+        return nary;

+      }

+      return this.sink.FindOrCreateTypeReference(typeReference);

+    }

+

     #region Constructors

 

     ///// <summary>

@@ -473,7 +494,7 @@ namespace BytecodeTranslator
           new Bpl.AssumeCmd(tok,

             Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

             this.sink.Heap.DynamicType(locExpr),

-            this.sink.FindOrCreateTypeReference(typ)

+            this.FindOrCreateTypeReferenceInCodeContext(typ)

             )

             )

           );

@@ -637,7 +658,7 @@ namespace BytecodeTranslator
           new Bpl.AssumeCmd(methodCallToken,

             Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

             this.sink.Heap.DynamicType(thisExpr),

-            this.sink.FindOrCreateTypeReference(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)

+            this.FindOrCreateTypeReferenceInCodeContext(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)

             )

             )

           );

@@ -701,13 +722,13 @@ namespace BytecodeTranslator
         List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();

         Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, methodToCall.ContainingType);

         foreach (ITypeReference typeReference in consolidatedTypeArguments) {

-          inexpr.Add(sink.FindOrCreateTypeReference(typeReference));

+          inexpr.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));

         }

       }

       IGenericMethodInstanceReference methodInstanceReference = methodToCall as IGenericMethodInstanceReference;

       if (methodInstanceReference != null) {

         foreach (ITypeReference typeReference in methodInstanceReference.GenericArguments) {

-          inexpr.Add(sink.FindOrCreateTypeReference(typeReference));

+          inexpr.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));

         }

       }

 

@@ -945,7 +966,7 @@ namespace BytecodeTranslator
             new Bpl.AssumeCmd(token,

               Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

               this.sink.Heap.DynamicType(Bpl.Expr.Ident(a)),

-              this.sink.FindOrCreateTypeReference(createObjectInstance.Type)

+              this.FindOrCreateTypeReferenceInCodeContext(createObjectInstance.Type)

               )

               )

             );

@@ -953,6 +974,7 @@ namespace BytecodeTranslator
       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

 

+

     public override void TraverseChildren(ICreateArray createArrayInstance)

     {

       Bpl.IToken cloc = createArrayInstance.Token();

@@ -1002,13 +1024,13 @@ namespace BytecodeTranslator
         List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();

         Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, methodToCall.ContainingType);

         foreach (ITypeReference typeReference in consolidatedTypeArguments) {

-          typeParameterExprs.Add(sink.FindOrCreateTypeReference(typeReference));

+          typeParameterExprs.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));

         }

       }

       IGenericMethodInstanceReference methodInstanceReference = methodToCall as IGenericMethodInstanceReference;

       if (methodInstanceReference != null) {

         foreach (ITypeReference typeReference in methodInstanceReference.GenericArguments) {

-          typeParameterExprs.Add(sink.FindOrCreateTypeReference(typeReference));

+          typeParameterExprs.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));

         }

       }

       Bpl.Expr typeParameterExpr =

@@ -1448,7 +1470,7 @@ namespace BytecodeTranslator
     public override void TraverseChildren(ICastIfPossible castIfPossible) {

       base.Traverse(castIfPossible.ValueToCast);

       var exp = TranslatedExpressions.Pop();

-      var e = this.sink.FindOrCreateTypeReference(castIfPossible.TargetType);

+      var e = this.FindOrCreateTypeReferenceInCodeContext(castIfPossible.TargetType);

       var callAs = new Bpl.NAryExpr(

         castIfPossible.Token(),

         new Bpl.FunctionCall(this.sink.Heap.AsFunction),

@@ -1458,7 +1480,7 @@ namespace BytecodeTranslator
       return;

     }

     public override void TraverseChildren(ICheckIfInstance checkIfInstance) {

-      var e = this.sink.FindOrCreateTypeReference(checkIfInstance.TypeToCheck);

+      var e = this.FindOrCreateTypeReferenceInCodeContext(checkIfInstance.TypeToCheck);

       //var callTypeOf = new Bpl.NAryExpr(

       //  checkIfInstance.Token(),

       //  new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),

@@ -1644,7 +1666,7 @@ namespace BytecodeTranslator
     }

 

     public override void TraverseChildren(ITypeOf typeOf) {

-      var e = this.sink.FindOrCreateTypeReference(typeOf.TypeToGet);

+      var e = this.FindOrCreateTypeReferenceInCodeContext(typeOf.TypeToGet);

       var callTypeOf = new Bpl.NAryExpr(

         typeOf.Token(),

         new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 4f0e3667..f6dc7ecf 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -125,7 +125,7 @@ namespace BytecodeTranslator {
       if (typeDefinition.IsClass) {

         bool savedSawCctor = this.sawCctor;

         this.sawCctor = false;

-        sink.FindOrCreateTypeReference(typeDefinition);

+        sink.FindOrDefineType(typeDefinition);

         base.TraverseChildren(typeDefinition);

         if (!this.sawCctor) {

           CreateStaticConstructor(typeDefinition);

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4af8c9ec..4702d5a0 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -211,7 +211,7 @@ namespace BytecodeTranslator {
         }

         module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

         // The decompiler does not turn calls to Assert/Assume into Code Model nodes

-        module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(module);

+        module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);

 

         host.RegisterAsLatest(module);

         modules.Add(module);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 50051b0c..957b8c38 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -867,14 +867,14 @@ namespace BytecodeTranslator {
     /// <paramref name="type"/> in the Bpl program. I.e., its

     /// value represents the expression "typeof(type)".

     /// </summary>

-    public Bpl.Expr FindOrCreateTypeReference(ITypeReference type) {

+    public Bpl.Expr FindOrCreateTypeReference(ITypeReference type, bool codeContext = false) {

 

       var gtir = type as IGenericTypeInstanceReference;

       if (gtir != null) {

-        var genericType = FindOrDefineType(gtir.GenericType);

+        var genericType = FindOrDefineType(gtir.GenericType.ResolvedType);

         var gArgs = new Bpl.ExprSeq();

         foreach (var a in gtir.GenericArguments) {

-          var a_prime = FindOrCreateTypeReference(a);

+          var a_prime = FindOrCreateTypeReference(a, codeContext);

           gArgs.Add(a_prime);

         }

         var typeExpression = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(genericType), gArgs);

@@ -882,18 +882,24 @@ namespace BytecodeTranslator {
 

       IGenericTypeParameter gtp = type as IGenericTypeParameter;

       if (gtp != null) {

-        var selectorName = gtp.Name.Value;

-        selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);

-        var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);

-        typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

-        var funcName = String.Format("{0}#{1}", selectorName, typeName);

-        Bpl.IToken tok = Bpl.Token.NoToken;

-        var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.Heap.TypeType)));

-        var funcCall = new Bpl.FunctionCall(identExpr);

-        var thisArg = new Bpl.IdentifierExpr(tok, this.ThisVariable);

-        var dynType = this.Heap.DynamicType(thisArg);

-        var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));

-        return nary;

+        if (codeContext) {

+          var selectorName = gtp.Name.Value;

+          selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);

+          var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);

+          typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

+          var funcName = String.Format("{0}#{1}", selectorName, typeName);

+          Bpl.IToken tok = Bpl.Token.NoToken;

+          var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.Heap.TypeType)));

+          var funcCall = new Bpl.FunctionCall(identExpr);

+          var thisArg = new Bpl.IdentifierExpr(tok, this.ThisVariable);

+          var dynType = this.Heap.DynamicType(thisArg);

+          var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));

+          return nary;

+

+        } else {

+          var formal = FindOrDefineTypeParameter(gtp);

+          return Bpl.Expr.Ident(formal);

+        }

       }

 

       IGenericMethodParameter gmp = type as IGenericMethodParameter;

@@ -903,6 +909,15 @@ namespace BytecodeTranslator {
       }

 

       ITypeReference uninstantiatedGenericType = GetUninstantiatedGenericType(type);

+

+      // Corner case: type might be a reference to the uninstantiated generic type.

+      // This happens, e.g., with "typeof(Dictionary<,>)".

+      // In that case, need to create a constant for it (because Boogie doesn't allow

+      // overloading by arity on functions

+      if (type.ResolvedType.IsGeneric && type == uninstantiatedGenericType) {

+        return FindOrDefineTypeConstant(type);

+      }

+

       List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();

       GetConsolidatedTypeArguments(consolidatedTypeArguments, type);

 

@@ -912,24 +927,58 @@ namespace BytecodeTranslator {
         var f2 = this.declaredTypeFunctions[k];

         Bpl.ExprSeq args = new Bpl.ExprSeq();

         foreach (ITypeReference p in consolidatedTypeArguments) {

-          args.Add(FindOrCreateTypeReference(p));

+          args.Add(FindOrCreateTypeReference(p, codeContext));

         }

         Bpl.Expr naryExpr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f2), args);

         return naryExpr;

       }

 

-      var  f = FindOrDefineType(type);

-      // BUGBUG: Generics!

+      var  f = FindOrDefineType(type.ResolvedType);

       var fCall = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), new Bpl.ExprSeq());

       return fCall;

     }

 

+    /// <summary>

+    /// Constants of type "Type" that represent the uninstantiated type of a generic type.

+    /// E.g. "Dictionary&lt;,&gt;".

+    /// </summary>

+    private Dictionary<uint, Bpl.Constant> declaredTypeConstants = new Dictionary<uint, Bpl.Constant>();

+    private Bpl.Expr FindOrDefineTypeConstant(ITypeReference type) {

+      Bpl.Constant c;

+      var k = type.InternedKey;

+      if (!this.declaredTypeConstants.TryGetValue(k, out c)) {

+        var typeName = TypeHelper.GetTypeName(type);

+        var i = typeName.IndexOf('`');

+        // assume there is just one occurrence

+        if (i != -1) {

+          typeName = typeName.Substring(0, i);

+        }

+        typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

+        var typedIdent = new Bpl.TypedIdent(Bpl.Token.NoToken, typeName, this.Heap.TypeType);

+        c = new Bpl.Constant(Bpl.Token.NoToken, typedIdent, true);

+        this.declaredTypeConstants.Add(k, c);

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

+      }

+      return Bpl.Expr.Ident(c);

+    }

+

+    private Dictionary<IGenericParameter, Bpl.Formal> declaredTypeParameters = new Dictionary<IGenericParameter, Bpl.Formal>();

+    public Bpl.Formal FindOrDefineTypeParameter(IGenericParameter genericParameter) {

+      Bpl.Formal formal;

+      if (!this.declaredTypeParameters.TryGetValue(genericParameter, out formal)) {

+        var n = genericParameter.Name.Value;

+        var n2 = TranslationHelper.TurnStringIntoValidIdentifier(n);

+        formal = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, n2, this.Heap.TypeType), true);

+      }

+      return formal;

+    }

   

     /// <summary>

-    /// The Heap has to decide how to represent the type. 

-    /// All the Sink cares about is adding a declaration for it.

+    /// Every type is represented as a function.

+    /// Non-generic types are nullary functions.

+    /// Generic types are n-ary functions, where n is the number of generic parameters.

     /// </summary>

-    public Bpl.Function FindOrDefineType(ITypeReference type) {

+    public Bpl.Function FindOrDefineType(ITypeDefinition type) {

 

       Bpl.Function f;

 

@@ -939,19 +988,30 @@ namespace BytecodeTranslator {
 

       var numParameters = ConsolidatedGenericParameterCount(type);

 

-      f = this.Heap.CreateTypeFunction(type, numParameters);

+      //f = this.Heap.CreateTypeFunction(type, numParameters);

+

+      string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);

+      typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

+      var tok = type.Token();

+      var inputs = new Bpl.VariableSeq();

+      foreach (var t in TranslationHelper.ConsolidatedGenericParameters(type)) {

+        var formal = FindOrDefineTypeParameter(t);

+        inputs.Add(formal);

+      }

+      Bpl.Variable output = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "result", this.Heap.TypeType), false);

+      Bpl.Function func = new Bpl.Function(tok, typename, inputs, output);

+      func.Attributes = new Bpl.QKeyValue(Bpl.Token.NoToken, "constructor", new List<object>(1), null);

+      f = func;

+

       this.declaredTypeFunctions.Add(key, f);

       this.TranslatedProgram.TopLevelDeclarations.Add(f);

-      DeclareParents(type.ResolvedType, f);

+      DeclareParents(type, f);

 

       bool isExtern = this.assemblyBeingTranslated != null &&

                       !TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);

       if (isExtern) {

         var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);

-        if (f.Attributes == null)

-          f.Attributes = attrib;

-        else

-          f.Attributes.AddLast(attrib);

+        f.Attributes.AddLast(attrib);

       }

       return f;

     }

@@ -966,31 +1026,27 @@ namespace BytecodeTranslator {
       return;

     }

     private void DeclareSuperType(Bpl.Function typeDefinitionAsBplFunction, ITypeReference superType) {

-      var superTypeFunction = FindOrDefineType(superType);

+      var superTypeExpr = FindOrCreateTypeReference(superType);

       var numberOfGenericParameters = typeDefinitionAsBplFunction.InParams.Length;

 

       var qvars = new Bpl.VariableSeq();

       var exprs = new Bpl.ExprSeq();

-      var superTypeArgs = new Bpl.ExprSeq();

       for (int i = 0; i < numberOfGenericParameters; i++) {

         var t = typeDefinitionAsBplFunction.InParams[i];

         qvars.Add(t);

         var identForT = Bpl.Expr.Ident(t);

         exprs.Add(identForT);

-        if (i < superTypeFunction.InParams.Length)

-          superTypeArgs.Add(identForT);

       }

 

       // G(t,u)

       var callToG = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs);

-      var callToSuperType = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(superTypeFunction), superTypeArgs);

       // Subtype(G(t,u), super)

-      Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, callToSuperType));

+      Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, superTypeExpr));

       Bpl.Expr disjointSubtree = null;

       var isDisjoint = !superType.ResolvedType.IsInterface;

       if (isDisjoint) {

         // DisjointSubtree(G(t,u), super)

-        disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, callToSuperType));

+        disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, superTypeExpr));

       }

 

       if (0 < numberOfGenericParameters) {

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 7a9340db..424064ff 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -512,7 +512,7 @@ namespace BytecodeTranslator
       List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();

       this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InCatch));

       foreach (ICatchClause catchClause in tryCatchFinallyStatement.CatchClauses) {

-        typeReferences.Insert(0, this.sink.FindOrCreateTypeReference(catchClause.ExceptionType));

+        typeReferences.Insert(0, this.sink.FindOrCreateTypeReference(catchClause.ExceptionType, true));

         StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

         if (catchClause.ExceptionContainer != Dummy.LocalVariable) {

           Bpl.Variable catchClauseVariable = this.sink.FindOrCreateLocalVariable(catchClause.ExceptionContainer);

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 98610297..2862a520 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -126,14 +126,25 @@ namespace BytecodeTranslator {
       Contract.Requires(typeReference != null);

 

       var typeDefinition = typeReference.ResolvedType;

-      var totalParameters = new List<IGenericTypeParameter>(typeDefinition.GenericParameters);

+      var totalParameters = new List<IGenericTypeParameter>();

+      ConsolidatedGenericParameters(typeDefinition, totalParameters);

+      return totalParameters;

+

+      //var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;

+      //while (nestedTypeDefinition != null) {

+      //  var containingType = nestedTypeDefinition.ContainingType.ResolvedType;

+      //  totalParameters.AddRange(containingType.GenericParameters);

+      //  nestedTypeDefinition = containingType as INestedTypeDefinition;

+      //}

+      //totalParameters.AddRange(typeDefinition.GenericParameters);

+      //return totalParameters;

+    }

+    private static void ConsolidatedGenericParameters(ITypeDefinition typeDefinition, List<IGenericTypeParameter> consolidatedParameters){

       var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;

-      while (nestedTypeDefinition != null) {

-        var containingType = nestedTypeDefinition.ContainingType.ResolvedType;

-        totalParameters.AddRange(containingType.GenericParameters);

-        nestedTypeDefinition = containingType as INestedTypeDefinition;

+      if (nestedTypeDefinition != null){

+        ConsolidatedGenericParameters(nestedTypeDefinition.ContainingTypeDefinition, consolidatedParameters);

       }

-      return totalParameters;

+      consolidatedParameters.AddRange(typeDefinition.GenericParameters);

     }

 

     public static string CreateUniqueMethodName(IMethodReference method) {

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index e1d2d73a..d9366708 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -165,7 +165,7 @@ namespace BytecodeTranslator {
           var m = typeMethodPair.Item2;

 

           // guard: is#T($DynamicType(local_variable))

-          var typeFunction = this.sink.FindOrDefineType(t);

+          var typeFunction = this.sink.FindOrDefineType(t.ResolvedType);

           if (typeFunction == null) {

             // BUGBUG!! This just silently skips the branch that would dispatch to t's implementation of the method!

             continue;

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 5a1f8dc5..83e6009d 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -389,8 +389,8 @@ namespace Microsoft.Boogie {
             inline = true;

           }

         }

-        if (inline && CommandLineOptions.Clo.LazyInlining == 0 &&

-          CommandLineOptions.Clo.StratifiedInlining == 0) {

+        if ((inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) ||

+            CommandLineOptions.Clo.InlineDepth >= 0) {

           foreach (Declaration d in TopLevelDeclarations) {

             Implementation impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ffccdc5..7d3fce84 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -143,6 +143,7 @@ namespace Microsoft.Boogie {
     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

+    public int InlineDepth = -1;

     public bool UseUncheckedContracts = false;

     public bool SimplifyLogFileAppend = false;

     public bool SoundnessSmokeTest = false;

@@ -949,7 +950,10 @@ namespace Microsoft.Boogie {
           case "/contractInfer":

             ContractInfer = true;

             break;

-

+          case "-inlineDepth":

+          case "/inlineDepth":

+            ps.GetNumericArgument(ref InlineDepth);

+            break;

           case "-subsumption":

           case "/subsumption": {

               int s = 0;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index d9c33bd4..adc7e2f0 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -26,6 +26,8 @@ namespace Microsoft.Boogie {
 

     protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap;

 

+    protected int inlineDepth;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(codeCopier != null);

@@ -67,6 +69,7 @@ namespace Microsoft.Boogie {
     protected Inliner(InlineCallback cb) {

       inlinedProcLblMap = new Dictionary<string/*!*/, int>();

       recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();

+      inlineDepth = CommandLineOptions.Clo.InlineDepth;

       codeCopier = new CodeCopier();

       inlineCallback = cb;

     }

@@ -159,6 +162,8 @@ namespace Microsoft.Boogie {
     // otherwise, the procedure is not inlined at the call site

     protected int GetInlineCount(Implementation impl) {

       Contract.Requires(impl != null);

+      Contract.Requires(impl.Proc != null);

+

       string/*!*/ procName = impl.Name;

       Contract.Assert(procName != null);

       int c;

@@ -169,9 +174,7 @@ namespace Microsoft.Boogie {
       c = -1; // TryGetValue above always overwrites c

       impl.CheckIntAttribute("inline", ref c);

       // procedure attribute overrides implementation

-      if (impl.Proc != null) {

-        impl.Proc.CheckIntAttribute("inline", ref c);

-      }

+      impl.Proc.CheckIntAttribute("inline", ref c);

 

       recursiveProcUnrollMap[procName] = c;

       return c;

@@ -194,9 +197,9 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private List<Block/*!*/>/*!*/ DoInlineBlocks(Stack<Procedure/*!*/>/*!*/ callStack, List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,

-                                         VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, ref bool inlinedSomething) {

-      Contract.Requires(cce.NonNullElements(callStack));

+    private List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,

+                                                 VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, 

+                                                 ref bool inlinedSomething) {

       Contract.Requires(cce.NonNullElements(blocks));

       Contract.Requires(program != null);

       Contract.Requires(newLocalVars != null);

@@ -204,7 +207,6 @@ namespace Microsoft.Boogie {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       List<Block/*!*/>/*!*/ newBlocks = new List<Block/*!*/>();

       

-

       foreach (Block block in blocks) {

         TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd);

         CmdSeq cmds = block.Cmds;

@@ -223,14 +225,16 @@ namespace Microsoft.Boogie {
           } else {

             Contract.Assert(callCmd.Proc != null);

             Procedure proc = callCmd.Proc;

-            int inline = -1;

 

             Implementation impl = FindProcImpl(program, proc);

-            if (impl != null) {

-              inline = GetInlineCount(impl);

+            if (impl == null) {

+              newCmds.Add(codeCopier.CopyCmd(cmd));

+              continue;

             }

+          

+            int inline = GetInlineCount(impl);

 

-            if (inline > 0) { // at least one block should exist

+            if (inline > 0 || (inline == -1 && inlineDepth > 0)) { // at least one block should exist

               Contract.Assume(impl != null);

               Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0);

               inlinedSomething = true;

@@ -247,18 +251,24 @@ namespace Microsoft.Boogie {
               // increment the counter for the procedure to be used in constructing the locals and formals

               NextInlinedProcLabel(proc.Name);

 

-              BeginInline(newLocalVars, newModifies, proc, impl);

+              BeginInline(newLocalVars, newModifies, impl);

 

-              List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, proc, impl, nextBlockLabel);

+              List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, impl, nextBlockLabel);

               Contract.Assert(cce.NonNullElements(inlinedBlocks));

 

               EndInline();

 

-              recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;

-              callStack.Push(cce.NonNull(impl.Proc));

-              inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);

-              callStack.Pop();

-              recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;

+              if (inline > 0)

+                recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;

+              else

+                inlineDepth = inlineDepth - 1;

+

+              inlinedBlocks = DoInlineBlocks(inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);

+

+              if (inline > 0)

+                recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;

+              else

+                inlineDepth = inlineDepth + 1;

 

               Block/*!*/ startBlock = inlinedBlocks[0];

               Contract.Assert(startBlock != null);

@@ -271,7 +281,7 @@ namespace Microsoft.Boogie {
 

               lblCount = nextlblCount;

               newCmds = new CmdSeq();

-            } else if (inline == 0) {

+            } else if (inline == 0 || (inline == -1 && inlineDepth == 0)) {

               inlinedSomething = true;

               if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {

                 // add assert

@@ -304,17 +314,20 @@ namespace Microsoft.Boogie {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       inlinedProcLblMap.Clear();

       recursiveProcUnrollMap.Clear();

+      inlineDepth = CommandLineOptions.Clo.InlineDepth;

 

       inlined = false;

-      return DoInlineBlocks(new Stack<Procedure/*!*/>(), blocks, program, newLocalVars, newModifies, ref inlined);

+      return DoInlineBlocks(blocks, program, newLocalVars, newModifies, ref inlined);

     }

 

-    protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Procedure proc, Implementation impl) {

+    protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Implementation impl) {

       Contract.Requires(impl != null);

-      Contract.Requires(proc != null);

+      Contract.Requires(impl.Proc != null);

       Contract.Requires(newModifies != null);

       Contract.Requires(newLocalVars != null);

+      

       Hashtable substMap = new Hashtable();

+      Procedure proc = impl.Proc;

 

       foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {

         Contract.Assert(locVar != null);

@@ -377,18 +390,19 @@ namespace Microsoft.Boogie {
 

 

     // result[0] is the entry block

-    protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Procedure proc, Implementation impl, string nextBlockLabel) {

+    protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {

       Contract.Requires(nextBlockLabel != null);

       Contract.Requires(impl != null);

-      Contract.Requires(proc != null);

+      Contract.Requires(impl.Proc != null);

       Contract.Requires(callCmd != null);

-      Contract.Requires(((codeCopier.Subst != null)));

+      Contract.Requires(codeCopier.Subst != null);

 

-      Contract.Requires((codeCopier.OldSubst != null));

+      Contract.Requires(codeCopier.OldSubst != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       List<Block/*!*/>/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks);

       Contract.Assert(implBlocks.Count > 0);

 

+      Procedure proc = impl.Proc;

       string startLabel = implBlocks[0].Label;

 

       List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>();

@@ -407,7 +421,7 @@ namespace Microsoft.Boogie {
       // inject non-free requires

       for (int i = 0; i < proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

-        if (!req.Free) {

+        if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {

           Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

           reqCopy.Condition = codeCopier.CopyExpr(req.Condition);

           AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);

@@ -472,7 +486,7 @@ namespace Microsoft.Boogie {
       // inject non-free ensures

       for (int i = 0; i < proc.Ensures.Length; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

-        if (!ens.Free) {

+        if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {

           Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());

           ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

           AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);

diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln
index 4fb930ef..a78d449e 100644
--- a/Source/GPUVerify.sln
+++ b/Source/GPUVerify.sln
@@ -53,26 +53,28 @@ Global
 		z3apidebug|x86 = z3apidebug|x86

 	EndGlobalSection

 	GlobalSection(ProjectConfigurationPlatforms) = postSolution

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Checked|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Checked|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.Build.0 = Debug|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.Build.0 = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.Build.0 = Release|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.ActiveCfg = Release|Any CPU

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.Build.0 = Release|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.Build.0 = Checked|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 74bdaa5e..b17ca60f 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -261,7 +261,7 @@ namespace GPUVerify
             verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

         }

 

-        private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)

+        protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)

         {

             Variable ReadOrWriteHasOccurred = ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);

             ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;

@@ -355,22 +355,12 @@ namespace GPUVerify
             AddReadOrWrittenZOffsetIsThreadIdCandidateEnsures(Proc, v, ReadOrWrite, Thread);

         }

 

-        protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));

-        }

-

-        protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));

-        }

-

         private void AddReadOrWrittenXOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)

         {

             Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);

             if (expr != null)

             {

-                Proc.Requires.Add(new Requires(false, expr));

+                verifier.AddCandidateRequires(Proc, expr);

             }

         }

 

@@ -379,7 +369,7 @@ namespace GPUVerify
             Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);

             if (expr != null)

             {

-                Proc.Requires.Add(new Requires(false, expr));

+                verifier.AddCandidateRequires(Proc, expr);

             }

         }

 

@@ -388,7 +378,7 @@ namespace GPUVerify
             Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);

             if (expr != null)

             {

-                Proc.Requires.Add(new Requires(false, expr));

+                verifier.AddCandidateRequires(Proc, expr);

             }

         }

 

@@ -397,7 +387,7 @@ namespace GPUVerify
             Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);

             if (expr != null)

             {

-                Proc.Ensures.Add(new Ensures(false, expr));

+                verifier.AddCandidateEnsures(Proc, expr);

             }

         }

 

@@ -406,7 +396,7 @@ namespace GPUVerify
             Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);

             if (expr != null)

             {

-                Proc.Ensures.Add(new Ensures(false, expr));

+                verifier.AddCandidateEnsures(Proc, expr);

             }

         }

 

@@ -415,7 +405,7 @@ namespace GPUVerify
             Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);

             if (expr != null)

             {

-                Proc.Ensures.Add(new Ensures(false, expr));

+                verifier.AddCandidateEnsures(Proc, expr);

             }

         }

 

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 25974225..36881f88 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -597,7 +597,7 @@ namespace GPUVerify
 

 

 

-        private void AddCandidateRequires(Procedure Proc, Expr e)

+        internal void AddCandidateRequires(Procedure Proc, Expr e)

         {

             Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);

             IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);

@@ -605,7 +605,7 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

         }

 

-        private void AddCandidateEnsures(Procedure Proc, Expr e)

+        internal void AddCandidateEnsures(Procedure Proc, Expr e)

         {

             Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);

             IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 7023a2b3..6956b973 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -61,6 +61,37 @@
     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

+    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>

+  </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'">

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <Optimize>true</Optimize>

+    <DebugType>pdbonly</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 0f5f8278..237c155e 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -81,10 +81,6 @@ namespace GPUVerify
 

         protected abstract void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo);

 

-        protected abstract void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);

-

-        protected abstract void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);

-

         public void AddRaceCheckingCandidateInvariants(WhileCmd wc)

         {

             foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

@@ -154,7 +150,13 @@ namespace GPUVerify
                 failedToFindSecondAccess = false;

             }

 

-            AddRaceCheckCalls(verifier.KernelImplementation);

+            foreach (Declaration d in verifier.Program.TopLevelDeclarations)

+            {

+                if (d is Implementation)

+                {

+                    AddRaceCheckCalls(d as Implementation);

+                }

+            }

 

             if (failedToFindSecondAccess || !addedLogWrite)

                 return false;

@@ -447,5 +449,19 @@ namespace GPUVerify
             }

         }

 

+        private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

+        {

+            verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

+        }

+

+        private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

+        {

+            verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

+        }

+

+        protected abstract Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo);

+

+

+

     }

 }

diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
index 3b1f877e..b3104609 100644
--- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
@@ -567,7 +567,7 @@ namespace GPUVerify
             verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

         }

 

-        private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)

+        protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)

         {

             int OneOrTwo = Int32.Parse(OneOrTwoString);

             Expr expr = null;

@@ -756,7 +756,7 @@ namespace GPUVerify
 

             if (expr != null)

             {

-                Proc.Requires.Add(new Requires(false, expr));

+                verifier.AddCandidateRequires(Proc, expr);

             }

         }

 

@@ -766,19 +766,9 @@ namespace GPUVerify
 

             if (expr != null)

             {

-                Proc.Ensures.Add(new Ensures(false, expr));

+                verifier.AddCandidateEnsures(Proc, expr);

             }

         }

 

-        protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));

-        }

-

-        protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));

-        }

-

     }

 }

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index c725c96a..310a25af 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -680,8 +680,6 @@ namespace Microsoft.Boogie
       internal System.IO.TextReader rd;

       string lastLine = "";

       int lineNo;

-      bool v1model = false;

-      Dictionary<string, Element> partitionMapping = new Dictionary<string, Element>(); // only used when v1model is true

       internal List<Model> resModels = new List<Model>();

       Model currModel;

 

@@ -704,8 +702,7 @@ namespace Microsoft.Boogie
         return f;

       }

 

-      List<object> GetFunctionTuple() {

-        string newLine = ReadLine();

+      List<object> GetFunctionTuple(string newLine) {

         if (newLine == null)

           return null;

         string line = newLine;

@@ -782,26 +779,15 @@ namespace Microsoft.Boogie
         return new DatatypeValue(currModel, (string)os[0], args);

       }

 

-      Element GetElt(string name)

-      {

-        Element ret;

-

-        if (v1model) {

-          if (!partitionMapping.TryGetValue(name, out ret))

-            BadModel("undefined partition " + name);

-        } else {

-          ret = currModel.TryMkElement(name);

-          if (ret == null)

-            BadModel("invalid element name " + name);

-        }

-

+      Element GetElt(string name) {

+        Element ret = currModel.TryMkElement(name);

+        if (ret == null)

+          BadModel("invalid element name " + name);

         return ret;

       }

 

       void NewModel()

       {

-        v1model = false;

-        partitionMapping.Clear();

         lastLine = "";

         currModel = new Model();

         resModels.Add(currModel);

@@ -822,14 +808,10 @@ namespace Microsoft.Boogie
             continue;

           if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")

             continue;

-          if (line == "partitions:" || line == "function interpretations:") {

-            v1model = true;

-            continue;

-          }

 

-          var words = GetWords(line);

-          if (words.Length == 0) continue;

-          var lastWord = words[words.Length - 1];

+          var words = GetFunctionTuple(line);

+          if (words.Count == 0) continue;

+          var lastWord = words[words.Count - 1];

 

           if (currModel == null)

             BadModel("model begin marker not found");

@@ -853,35 +835,13 @@ namespace Microsoft.Boogie
             continue;

           }

 

-          if (v1model && words[0][0] == '*') {

-            var partName = words[0];

-            var len = words.Length;

-            Element elt;

-            if (len >= 3 && words[len - 2] == "->") {

-              elt = currModel.TryMkElement(lastWord);

-              if (elt == null) BadModel("bad parition value " + lastWord);

-              len -= 2;

-            } else {

-              elt = currModel.MkElement(words[0]);

-            }

-            partitionMapping.Add(partName, elt);

-            for (int i = 1; i < len; ++i) {

-              var name = words[i];

-              if (i == 1 && name[0] == '{')

-                name = name.Substring(1);

-              if (i == len - 1 && name.EndsWith("}"))

-                name = name.Substring(0, name.Length - 1);

-              var cnst = currModel.MkFunc(name, 0);

-              cnst.SetConstant(elt);

-            }

-

-          } else if (words.Length == 3 && words[1] == "->") {

+          if (words.Count == 3 && words[1] is string && ((string) words[1]) == "->") {

             Func fn = null;

-            var funName = words[0];

+            var funName = (string) words[0];

 

-            if (lastWord == "{") {

+            if (lastWord is string && ((string) lastWord) == "{") {

               for ( ; ; ) {

-                var tuple = GetFunctionTuple();

+                var tuple = GetFunctionTuple(ReadLine());

                 if (tuple == null) BadModel("EOF in function table");

                 if (tuple.Count == 0) continue;

                 string tuple0 = tuple[0] as string;

diff --git a/Test/inline/Answer b/Test/inline/Answer
index ae632f79..2c29ab0b 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1439,6 +1439,197 @@ implementation bar()
 

 

 Boogie program verifier finished with 5 verified, 0 errors

+-------------------- test7.bpl --------------------

+

+var g: int;

+

+procedure main();

+  modifies g;

+

+

+

+implementation main()

+{

+

+  anon0:

+    g := 0;

+    call foo();

+    assert g == 1;

+    return;

+}

+

+

+

+procedure foo();

+  modifies g;

+

+

+

+implementation foo()

+{

+

+  anon0:

+    g := g + 1;

+    return;

+}

+

+

+after inlining procedure calls

+procedure main();

+  modifies g;

+

+

+implementation main()

+{

+  var inline$foo$0$g: int;

+

+  anon0:

+    g := 0;

+    goto inline$foo$0$Entry;

+

+  inline$foo$0$Entry:

+    inline$foo$0$g := g;

+    goto inline$foo$0$anon0;

+

+  inline$foo$0$anon0:

+    g := g + 1;

+    goto inline$foo$0$Return;

+

+  inline$foo$0$Return:

+    goto anon0$1;

+

+  anon0$1:

+    assert g == 1;

+    return;

+}

+

+

+

+Boogie program verifier finished with 2 verified, 0 errors

+-------------------- test8.bpl --------------------

+

+var g: int;

+

+procedure main();

+  modifies g;

+

+

+

+implementation main()

+{

+

+  anon0:

+    g := 0;

+    call foo();

+    assert g == 1;

+    return;

+}

+

+

+

+procedure {:inline 1} foo();

+  modifies g;

+

+

+

+implementation foo()

+{

+

+  anon0:

+    call bar();

+    return;

+}

+

+

+

+procedure bar();

+  modifies g;

+

+

+

+implementation bar()

+{

+

+  anon0:

+    g := g + 1;

+    return;

+}

+

+

+after inlining procedure calls

+procedure main();

+  modifies g;

+

+

+implementation main()

+{

+  var inline$foo$0$g: int;

+  var inline$bar$0$g: int;

+

+  anon0:

+    g := 0;

+    goto inline$foo$0$Entry;

+

+  inline$foo$0$Entry:

+    inline$foo$0$g := g;

+    goto inline$foo$0$anon0;

+

+  inline$foo$0$anon0:

+    goto inline$bar$0$Entry;

+

+  inline$bar$0$Entry:

+    inline$bar$0$g := g;

+    goto inline$bar$0$anon0;

+

+  inline$bar$0$anon0:

+    g := g + 1;

+    goto inline$bar$0$Return;

+

+  inline$bar$0$Return:

+    goto inline$foo$0$anon0$1;

+

+  inline$foo$0$anon0$1:

+    goto inline$foo$0$Return;

+

+  inline$foo$0$Return:

+    goto anon0$1;

+

+  anon0$1:

+    assert g == 1;

+    return;

+}

+

+

+after inlining procedure calls

+procedure {:inline 1} foo();

+  modifies g;

+

+

+implementation foo()

+{

+  var inline$bar$0$g: int;

+

+  anon0:

+    goto inline$bar$0$Entry;

+

+  inline$bar$0$Entry:

+    inline$bar$0$g := g;

+    goto inline$bar$0$anon0;

+

+  inline$bar$0$anon0:

+    g := g + 1;

+    goto inline$bar$0$Return;

+

+  inline$bar$0$Return:

+    goto anon0$1;

+

+  anon0$1:

+    return;

+}

+

+

+

+Boogie program verifier finished with 3 verified, 0 errors

 -------------------- test5.bpl --------------------

 test5.bpl(37,3): Error BP5001: This assertion might not hold.

 Execution trace:

diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index f56d55a0..3a8b0a9d 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -13,6 +13,11 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do (
   %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f

 )

 

+for %%f in (test7.bpl test8.bpl) do (

+  echo -------------------- %%f --------------------

+  %BGEXE% %* /inline:spec /inlineDepth:1 /print:- /env:0 /printInlined /noinfer %%f

+)

+

 for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (

   echo -------------------- %%f --------------------

   %BGEXE% %* %%f

diff --git a/Test/inline/test7.bpl b/Test/inline/test7.bpl
new file mode 100644
index 00000000..b5c6a4c6
--- /dev/null
+++ b/Test/inline/test7.bpl
@@ -0,0 +1,15 @@
+var g: int;

+

+procedure main() 

+modifies g;

+{

+  g := 0;

+  call foo();

+  assert g == 1;

+}

+

+procedure foo() 

+modifies g;

+{

+  g := g + 1;

+}
\ No newline at end of file
diff --git a/Test/inline/test8.bpl b/Test/inline/test8.bpl
new file mode 100644
index 00000000..12eab481
--- /dev/null
+++ b/Test/inline/test8.bpl
@@ -0,0 +1,21 @@
+var g: int;

+

+procedure main() 

+modifies g;

+{

+  g := 0;

+  call foo();

+  assert g == 1;

+}

+

+procedure {:inline 1} foo() 

+modifies g;

+{

+  call bar();

+}

+

+procedure bar()

+modifies g;

+{

+  g := g + 1;

+}
\ No newline at end of file
diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index e1ff7176..3ecae08a 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,21 +1,21 @@
-# Aste started: 2011-11-01 07:00:10

+# Aste started: 2011-11-12 07:00:04

 # Host id: Boogiebox

 # Configuration: boogie.cfg

 # Task: aste.tasks.boogie.FullBuild

-# [2011-11-01 07:03:36] SpecSharp revision: 979f82b8db6c

-# [2011-11-01 07:03:36] SscBoogie revision: 979f82b8db6c

-# [2011-11-01 07:05:13] Boogie revision: f402d8e0fc1b

-[2011-11-01 07:06:40] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

+# [2011-11-12 07:03:24] SpecSharp revision: 31c83dcaabce

+# [2011-11-12 07:03:24] SscBoogie revision: 31c83dcaabce

+# [2011-11-12 07:05:06] Boogie revision: c4b860ad3af4

+[2011-11-12 07:06:26] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

 

     1>corflags : warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


     warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


-[2011-11-01 07:08:09] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+[2011-11-12 07:07:59] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


-    D:\Temp\aste\Boogie\Source\Core\Absy.cs(710,9): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\Core\Absy.cs(749,9): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\Core\Absy.cs(679,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.


+    D:\Temp\aste\Boogie\Source\Core\Absy.cs(718,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.


     EXEC : warning CC1079: Type Microsoft.Boogie.Variable implements Microsoft.AbstractInterpretationFramework.IVariable.get_Name by inheriting Microsoft.Boogie.NamedDeclaration.get_Name causing the interface contract to not be checked at runtime. Consider adding a wrapper method.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(111,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(116,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.


@@ -41,5 +41,5 @@
     warning CS0162: Unreachable code detected


     warning CS0219: The variable 'expand' is assigned but its value is never used


     warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


-[2011-11-01 08:02:30] 0 out of 31 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2011-11-01 08:02:53] Released nightly of Boogie

+[2011-11-12 08:05:27] 0 out of 31 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2011-11-12 08:06:33] Released nightly of Boogie