Made it unnecessary to set the types on the Boogie ASTs as we create them.

Added support for string literals.
Translating structs no longer crashes the translator, but on the other hand, they are just skipped and not translated...
Added a helper method to make sure that generated identifiers are Boogie-legal.

1 files changed, 4 insertions, 4 deletions

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;