diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-08-06 10:27:17 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-08-06 10:27:17 -0700 |
| commit | b95f6aa1be913fe996848a64ad53e63b4f49d4ab (patch) | |
| tree | 2b12b51feca9af1b299225a864c014af784d5baa /BCT/BytecodeTranslator/Program.cs | |
| parent | 87946bf9c24a394c93dc3ffbae7c544640e8c120 (diff) | |
Added option "getMeHere" so that calls to GetMeHere.Assert(e) become "assert e"
(which really could be done just by defining it that way in an assembly either
via a contract or else by inlining it). But more importantly the option causes
all assertions to be translated as assumptions. Still to do: postconditions
should be translated as "free ensures".
Diffstat (limited to 'BCT/BytecodeTranslator/Program.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 7a56db76..abb9a2c2 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -34,6 +34,9 @@ namespace BytecodeTranslator { [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]
public bool captureState = false;
+ [OptionDescription("Translation should be done for Get Me Here functionality, (default: false)", ShortForm = "gmh")]
+ public bool getMeHere = false;
+
[OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
|