Better error handling.

Defined a new Boogie type, Real, that will be used to represent floating point
numbers.

1 files changed, 22 insertions, 0 deletions

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 7607f30c..9e1fa296 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -73,6 +73,8 @@ namespace BytecodeTranslator {
 

     public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);

 

+    #region Boogie Types

+

     [RepresentationFor("Field", "type Field;")]

     public Bpl.TypeCtorDecl FieldTypeDecl = null;

     public Bpl.CtorType FieldType;

@@ -106,6 +108,15 @@ namespace BytecodeTranslator {
     [RepresentationFor("$DefaultStruct", "const unique $DefaultStruct : Struct;")]

     public Bpl.Constant DefaultStruct;

 

+    [RepresentationFor("Real", "type Real;")]

+    protected Bpl.TypeCtorDecl RealTypeDecl = null;

+    public Bpl.CtorType RealType;

+

+    #endregion

+

+    #region Conversions

+

+    #region Heap values

 

     [RepresentationFor("Box2Int", "function Box2Int(Box): int;")]

     public Bpl.Function Box2Int = null;

@@ -174,6 +185,8 @@ namespace BytecodeTranslator {
       return callExpr;

     }

 

+    #endregion

+

     #region "Boxing" as done in the CLR

     /// <summary>

     /// Used to represent "boxing" as it is done in the CLR.

@@ -186,6 +199,15 @@ namespace BytecodeTranslator {
     public Bpl.Function Bool2Ref = null;

     #endregion

 

+    #region Real number conversions

+    [RepresentationFor("Int2Real", "function Int2Real(int, Type, Type): Real;")]

+    public Bpl.Function Int2Real = null;

+    [RepresentationFor("Real2Int", "function Real2Int(Real, Type, Type): Real;")]

+    public Bpl.Function Real2Int = null;

+    #endregion

+

+    #endregion

+

     /// <summary>

     /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

     /// on its type based on the heap representation. I.e., the value of this