Add a method to the Sink that is responsible for creating a Boogie expression

representing the default value for a type. All clients that need to create
a default value should use this.

4 files changed, 20 insertions, 38 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index d30202da..bcd9e785 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -405,20 +405,7 @@ namespace BytecodeTranslator
     }

 

     public override void Visit(IDefaultValue defaultValue) {

-      var bplType = sink.CciTypeToBoogie(defaultValue.Type);

-      if (bplType == Bpl.Type.Int) {

-        var lit = Bpl.Expr.Literal(0);

-        lit.Type = Bpl.Type.Int;

-        TranslatedExpressions.Push(lit);

-      } else if (bplType == Bpl.Type.Bool) {

-        var lit = Bpl.Expr.False;

-        lit.Type = Bpl.Type.Bool;

-        TranslatedExpressions.Push(lit);

-      } else if (defaultValue.Type.ResolvedType.IsStruct){

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.Heap.DefaultStruct));

-      } else {

-        throw new NotImplementedException("Don't know how to translate type");

-      }

+      TranslatedExpressions.Push(this.sink.DefaultValue(defaultValue.Type));

     }

 

     #endregion

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index ba35121d..4510db46 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -90,18 +90,7 @@ namespace BytecodeTranslator {
       var stmtBuilder = new Bpl.StmtListBuilder();

 

       foreach (var f in typeDefinition.Fields) {

-        Bpl.Expr e;

-        var bplType = this.sink.CciTypeToBoogie(f.Type);

-        if (bplType == Bpl.Type.Int) {

-          e = Bpl.Expr.Literal(0);

-          e.Type = Bpl.Type.Int;

-        } else if (bplType == Bpl.Type.Bool) {

-          e = Bpl.Expr.False;

-          e.Type = Bpl.Type.Bool;

-        } else {

-          throw new NotImplementedException("Don't know how to translate type");

-        }

-

+        var e = this.sink.DefaultValue(f.Type);

         var fExp = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f));

         var o = Bpl.Expr.Ident(proc.OutParams[0]);

         var c = this.sink.Heap.WriteHeap(Bpl.Token.NoToken, o, fExp, e, true);

@@ -145,18 +134,7 @@ namespace BytecodeTranslator {
       foreach (var f in typeDefinition.Fields) {

         if (f.IsStatic) {

 

-          Bpl.Expr e;

-          var bplType = this.sink.CciTypeToBoogie(f.Type);

-          if (bplType == Bpl.Type.Int) {

-            e = Bpl.Expr.Literal(0);

-            e.Type = Bpl.Type.Int;

-          } else if (bplType == Bpl.Type.Bool) {

-            e = Bpl.Expr.False;

-            e.Type = Bpl.Type.Bool;

-          } else {

-            throw new NotImplementedException("Don't know how to translate type");

-          }

-

+          var e = this.sink.DefaultValue(f.Type);

           stmtBuilder.Add(

             TranslationHelper.BuildAssignCmd(

             Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f)), 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 6e3909ab..c8b365ba 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -97,6 +97,23 @@ namespace BytecodeTranslator {
     

     public readonly Bpl.Program TranslatedProgram;

 

+    public Bpl.Expr DefaultValue(ITypeReference type) {

+      var bplType = CciTypeToBoogie(type);

+      if (bplType == Bpl.Type.Int) {

+        var lit = Bpl.Expr.Literal(0);

+        lit.Type = Bpl.Type.Int;

+        return lit;

+      } else if (bplType == Bpl.Type.Bool) {

+        var lit = Bpl.Expr.False;

+        lit.Type = Bpl.Type.Bool;

+        return lit;

+      } else if (type.ResolvedType.IsStruct) {

+        return Bpl.Expr.Ident(this.Heap.DefaultStruct);

+      } else {

+        throw new NotImplementedException("Don't know how to translate type");

+      }

+    }

+

     public Bpl.Type CciTypeToBoogie(ITypeReference type) {

       if (TypeHelper.TypesAreEquivalent(type, type.PlatformType.SystemBoolean))

         return Bpl.Type.Bool;

diff --git a/BCT/Samples/CodeCounter/codecounter.suo b/BCT/Samples/CodeCounter/codecounter.suo
index ef01e0e8..74d31951 100644
--- a/BCT/Samples/CodeCounter/codecounter.suo
+++ b/BCT/Samples/CodeCounter/codecounter.suo