diff options
| author |  akashlal <unknown> | 2011-02-17 12:19:53 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2011-02-17 12:19:53 +0000 |
| commit | f79fc4e0abd823571d5705106a4192d61b801b84 (patch) | |
| tree | a13a43dff28e8f0b5e648bfd5738438bc76777fe /Source/BoogieDriver | |
| parent | 3baf091750430d9f94cd75ac0334d54748f7a8c0 (diff) | |
Stratified inlining: Added concrete values to error traces. Added an extra flag "inferLeastForUnsat".
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 6b8cf7ca..3929e237 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -497,7 +497,24 @@ namespace Microsoft.Boogie { VCGen.Outcome outcome;
try {
- outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ if (CommandLineOptions.Clo.inferLeastForUnsat != null)
+ {
+ var svcgen = vcgen as VC.StratifiedVCGen;
+ Debug.Assert(svcgen != null);
+ var ss = new HashSet<string>();
+ foreach (var tdecl in program.TopLevelDeclarations)
+ {
+ var c = tdecl as Constant;
+ if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
+ ss.Add(c.Name);
+ }
+ outcome = svcgen.FindLeastToVerify(impl, program, ref ss);
+ errors = new List<Counterexample>();
+ }
+ else
+ {
+ outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ }
} catch (VCGenException e) {
ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true, true);
errors = null;
|