diff options
| author |  mikebarnett <unknown> | 2011-01-22 00:29:37 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2011-01-22 00:29:37 +0000 |
| commit | 6b20aec17ac8543e94b2a59dc6cef03988f8c4be (patch) | |
| tree | f3c175f231ac66acc435f60096d3531c28dc1386 /BCT/BytecodeTranslator | |
| parent | c5e0eb26a14adaab86c8adba7da828d7680a1bc4 (diff) | |
Make the general heap representation the default.
Make the pre- and post-conditions *not* be free contracts.
Diffstat (limited to 'BCT/BytecodeTranslator')
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index fb709d1e..05fe0f82 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -173,7 +173,7 @@ namespace BytecodeTranslator { Bpl.Requires req
= new Bpl.Requires(pre.Token(),
- true, exptravers.TranslatedExpressions.Pop(), "");
+ false, exptravers.TranslatedExpressions.Pop(), "");
boogiePrecondition.Add(req);
}
@@ -185,7 +185,7 @@ namespace BytecodeTranslator { Bpl.Ensures ens =
new Bpl.Ensures(post.Token(),
- true, exptravers.TranslatedExpressions.Pop(), "");
+ false, exptravers.TranslatedExpressions.Pop(), "");
boogiePostcondition.Add(ens);
}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 99528902..0e26be2a 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -27,7 +27,7 @@ namespace BytecodeTranslator { public enum HeapRepresentation { splitFields, twoDInt, twoDBox, general }
[OptionDescription("Heap representation to use", ShortForm = "heap")]
- public HeapRepresentation heapRepresentation = HeapRepresentation.twoDInt;
+ public HeapRepresentation heapRepresentation = HeapRepresentation.general;
}
|