11 files changed, 85 insertions, 24 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 13cb3552..74e52cfc 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -375,7 +375,10 @@ namespace BytecodeTranslator
       }
       else if (constant.Value is string)
       {
-        throw new NotImplementedException("Strings are not translated");
+        var c = this.sink.FindOrCreateConstant((string)(constant.Value));
+        TranslatedExpressions.Push(Bpl.Expr.Ident(c));
+
+        //throw new NotImplementedException("Strings are not translated");
       } else {
         // TODO: (mschaef) hack
         var lit = Bpl.Expr.Literal((int)constant.Value);
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 4bd086c0..8f21d59a 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -497,6 +497,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
     public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
       Bpl.Variable v;
       string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+      fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
       Bpl.IToken tok = field.Token();
 
       if (field.IsStatic) {
@@ -584,9 +585,11 @@ procedure {:inline 1} Alloc() returns (x: ref)
       else {
         // wrap it in the right conversion function
         Bpl.Function conversion;
-        if (value.Type == Bpl.Type.Bool)
+        var originalType = this.underlyingTypes[f.Decl];
+        var boogieType = TranslationHelper.CciTypeToBoogie(originalType);
+        if (boogieType == Bpl.Type.Bool)
           conversion = this.Bool2Box;
-        else if (value.Type == Bpl.Type.Int)
+        else if (boogieType == Bpl.Type.Int)
           conversion = this.Int2Box;
         else
           throw new InvalidOperationException("Unknown Boogie type");
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index e0c4124f..78be9b53 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -84,6 +84,7 @@ namespace BytecodeTranslator {
     {
         Bpl.Variable v;
         string typename = TypeHelper.GetTypeName(type);
+        typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
         Bpl.IToken tok = type.Token();
         Bpl.Type t = this.TypeType;
         Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, t);
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 9fc2f4ee..ce5bff5b 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -186,6 +186,8 @@ namespace BytecodeTranslator {
         base.Visit(typeDefinition);
       } else if (typeDefinition.IsEnum) {
         return; // enums just are translated as ints
+      } else if (typeDefinition.IsStruct) {
+        Console.WriteLine("Skipping definition of '" + TypeHelper.GetTypeName(typeDefinition) + "' because it is a struct!");
       } else {
         Console.WriteLine("Unknown kind of type definition '{0}' was found",
           TypeHelper.GetTypeName(typeDefinition));
@@ -196,8 +198,9 @@ namespace BytecodeTranslator {
     private bool sawCctor = false;
 
     private void CreateStaticConstructor(ITypeDefinition typeDefinition) {
-      var proc = new Bpl.Procedure(Bpl.Token.NoToken,
-          TypeHelper.GetTypeName(typeDefinition) + ".#cctor",
+      var typename = TypeHelper.GetTypeName(typeDefinition);
+      typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
+      var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#cctor",
           new Bpl.TypeVariableSeq(),
           new Bpl.VariableSeq(), // in
           new Bpl.VariableSeq(), // out
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index e08c1b7b..5a2b27d0 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -173,6 +173,21 @@ namespace BytecodeTranslator {
       return null;
     }
 
+    public Bpl.Constant FindOrCreateConstant(string str) {
+      Bpl.Constant c;
+      if (!this.declaredStringConstants.TryGetValue(str, out c)) {
+        var tok = Bpl.Token.NoToken;
+        var t = Bpl.Type.Int;
+        var name = "$string_literal_" + TranslationHelper.TurnStringIntoValidIdentifier(str);
+        var tident = new Bpl.TypedIdent(tok, name, t);
+        c = new Bpl.Constant(tok, tident, true);
+        this.declaredStringConstants.Add(str, c);
+        this.TranslatedProgram.TopLevelDeclarations.Add(c);
+      }
+      return c;
+    }
+    private Dictionary<string, Bpl.Constant> declaredStringConstants = new Dictionary<string, Bpl.Constant>();
+
     private Dictionary<IPropertyDefinition, Bpl.Variable> declaredProperties = new Dictionary<IPropertyDefinition, Bpl.Variable>();
 
     public struct ProcedureInfo {
@@ -268,7 +283,8 @@ namespace BytecodeTranslator {
         Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();
         Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();
 
-        IMethodContract contract = ContractProvider.GetMethodContractFor(method);
+        var possiblyUnspecializedMethod = Unspecialize(method);
+        IMethodContract contract = ContractProvider.GetMethodContractFor(possiblyUnspecializedMethod);
 
         if (contract != null) {
           try {
@@ -338,6 +354,24 @@ namespace BytecodeTranslator {
       this.FindOrCreateProcedure(method, isStatic);
       return this.declaredMethods[method];
     }
+    private static IMethodReference Unspecialize(IMethodReference method) {
+      IMethodReference result = method;
+      var gmir = result as IGenericMethodInstanceReference;
+      if (gmir != null) {
+        result = gmir.GenericMethod;
+      }
+      var smr = result as ISpecializedMethodReference;
+      if (smr != null) {
+        result = smr.UnspecializedVersion;
+      }
+      // Temporary hack until ISpecializedMethodDefinition implements ISpecializedMethodReference
+      var smd = result as ISpecializedMethodDefinition;
+      if (smd != null) {
+        result = smd.UnspecializedVersion;
+      }
+      return result;
+    }
+
 
 
     /// <summary>
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index be104448..bff181c5 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -113,7 +113,7 @@ namespace BytecodeTranslator
       StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);
       StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);
 
-      ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, null);
+      ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this);
       condTraverser.Visit(conditionalStatement.Condition);
       thenTraverser.Visit(conditionalStatement.TrueBranch);
       elseTraverser.Visit(conditionalStatement.FalseBranch);
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 04b95b37..30e90f8a 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -104,13 +104,30 @@ namespace BytecodeTranslator {
       }
       var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);
       s = s.Substring(2);
+      s = s.TrimEnd(')');
+      s = TurnStringIntoValidIdentifier(s);
+      return s;
+    }
+
+    public static string TurnStringIntoValidIdentifier(string s) {
       s = s.Replace('(', '$');
+      s = s.Replace(')', '$');
       s = s.Replace(',', '$');
-      s = s.TrimEnd(')');
       s = s.Replace("[]", "array");
       s = s.Replace('<', '$');
       s = s.Replace('>', '$');
       s = s.Replace(':', '$');
+      s = s.Replace(' ', '$');
+      s = s.Replace('{', '$');
+      s = s.Replace('}', '$');
+      s = s.Replace('-', '$');
+      s = s.Replace(' ', '$');
+      s = s.Replace('\t', '$');
+      s = s.Replace('\n', '$');
+      s = s.Replace('/', '$');
+      s = s.Replace('\\', '$');
+      s = s.Replace('=', '$');
+      s = s.Replace('@', '$');
       return s;
     }
 
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index a9ca1990..8f070d61 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -639,11 +639,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 
 
 
-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
@@ -658,11 +658,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 
 
 
-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 176360d8..c9ddf0dd 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -617,11 +617,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 
 
 
-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
@@ -636,11 +636,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 
 
 
-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
index cde891c4..555b1c5b 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
@@ -625,11 +625,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 
 
 
-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
@@ -644,11 +644,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 
 
 
-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
index 9f63170c..7091a8ea 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -615,11 +615,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 
 
 
-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
 {
   var local_0: int;
 
@@ -634,11 +634,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 
 
 
-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);
 
 
 
-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)
 {
   var local_0: int;