diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-15 18:48:02 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-15 18:48:02 -0800 |
| commit | 73b9d30f3b18425e52ef80453977d8608a1db09b (patch) | |
| tree | b2b98d7ba6846bee0a6c8f4a22e67eb620d493d8 /Source/VCGeneration | |
| parent | 78160fbd9492cf88e620a859a405fe9a49a09c54 (diff) | |
Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLineOptions to separate the options that belong to these 3 tools.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 001b3f2d..0a59555e 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2964,10 +2964,11 @@ namespace VC { if (!(kvp.Key is LiteralExpr) && kvp.Key.ToString() != o.ToString()) {
string boogieExpr;
// check whether we are handling BPL or SSC input
- if (CommandLineOptions.Clo.RunningBoogieOnSsc) {
- boogieExpr = Helpers.PrettyPrintBplExpr(kvp.Key);
- } else {
+ bool runningOnBpl = CommandLineOptions.Clo.Files.Exists(fn => Path.GetExtension(fn).ToLower() == "bpl");
+ if (runningOnBpl) {
boogieExpr = kvp.Key.ToString();
+ } else {
+ boogieExpr = Helpers.PrettyPrintBplExpr(kvp.Key);
}
relatedInformation.Add("(internal state dump): " + string.Format("{0} == {1}", boogieExpr, o));
}
|