diff options
| author |  mikebarnett <unknown> | 2011-01-16 05:38:44 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2011-01-16 05:38:44 +0000 |
| commit | 855c51dc0533b552cadcb513cbca541b53c4b7b3 (patch) | |
| tree | 68ad0bdefcb2702891071f22433560ad397455ae | |
| parent | d95ace9aad0fc7a9fc5dbf43ed713db7f3625b2f (diff) | |
Fix translation of "null" so that it produces a type-correct value.
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 12 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Prelude.cs | 3 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/RegressionTestInput.txt | 3 |
3 files changed, 13 insertions, 5 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index e1d07c14..2c3b1feb 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -398,9 +398,15 @@ namespace BytecodeTranslator {
if (constant.Value == null)
{
- // TODO: (mschaef) hack
- TranslatedExpressions.Push(Bpl.Expr.False);
- }
+ var bplType = TranslationHelper.CciTypeToBoogie(constant.Type);
+ if (bplType == Bpl.Type.Int) {
+ TranslatedExpressions.Push(Bpl.Expr.Literal(0));
+ } else if (bplType == Bpl.Type.Bool) {
+ TranslatedExpressions.Push(Bpl.Expr.False);
+ } else {
+ throw new NotImplementedException("Don't know how to translate type");
+ }
+ }
else if (constant.Value is bool)
{
TranslatedExpressions.Push(((bool)constant.Value) ? Bpl.Expr.True : Bpl.Expr.False);
diff --git a/BCT/BytecodeTranslator/Prelude.cs b/BCT/BytecodeTranslator/Prelude.cs index b0830eec..919fa39a 100644 --- a/BCT/BytecodeTranslator/Prelude.cs +++ b/BCT/BytecodeTranslator/Prelude.cs @@ -19,7 +19,8 @@ var $ArrayLength: [int]int; var $Alloc: [int] bool;
procedure {:inline 1} Alloc() returns (x: int)
-modifies $Alloc;
+ free ensures x != 0;
+ modifies $Alloc;
{
assume $Alloc[x] == false;
$Alloc[x] := true;
diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt index 9a736906..ae41cebd 100644 --- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt +++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt @@ -11,7 +11,8 @@ var $ArrayLength: [int]int; var $Alloc: [int] bool;
procedure {:inline 1} Alloc() returns (x: int)
-modifies $Alloc;
+ free ensures x != 0;
+ modifies $Alloc;
{
assume $Alloc[x] == false;
$Alloc[x] := true;
|