diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:03:09 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:03:09 -0400 |
commit | 618f037a466cd4392be6e1f4b20e248d58447456 (patch) | |
tree | 3c0b51de79e3537d3e94c8f1cca46f32d9a4b974 /Source/Core/CommandLineOptions.cs | |
parent | 636108e4c302a24ed658b5f09812010b30e36e95 (diff) | |
parent | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (diff) |
Merge branch 'dfsg_free'
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 28 |
1 files changed, 22 insertions, 6 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2be1cdf7..e9aa3ceb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -11,6 +11,7 @@ using System.IO; using System.Linq; using System.Diagnostics; using System.Diagnostics.Contracts; +using System.Text.RegularExpressions; namespace Microsoft.Boogie { public class CommandLineOptionEngine @@ -478,6 +479,8 @@ namespace Microsoft.Boogie { public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; + // TODO(wuestholz): Add documentation for this flag. + public bool PrintNecessaryAssumes = false; public int InlineDepth = -1; public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values public bool UseUncheckedContracts = false; @@ -588,7 +591,7 @@ namespace Microsoft.Boogie { } } - public string OwickiGriesDesugaredOutputFile = null; + public string CivlDesugaredFile = null; public bool TrustAtomicityTypes = false; public bool TrustNonInterference = false; public int TrustLayersUpto = -1; @@ -915,9 +918,9 @@ namespace Microsoft.Boogie { } return true; - case "OwickiGries": + case "CivlDesugaredFile": if (ps.ConfirmArgumentCount(1)) { - OwickiGriesDesugaredOutputFile = args[ps.i]; + CivlDesugaredFile = args[ps.i]; } return true; @@ -1502,7 +1505,7 @@ namespace Microsoft.Boogie { return true; case "verifySnapshots": - ps.GetNumericArgument(ref VerifySnapshots, 3); + ps.GetNumericArgument(ref VerifySnapshots, 4); return true; case "traceCaching": @@ -1618,6 +1621,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) || ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) || ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) || @@ -1700,7 +1704,7 @@ namespace Microsoft.Boogie { // no preference return true; } - return ProcsToCheck.Contains(methodFullname); + return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$")); } public virtual StringCollection ParseNamedArgumentList(string argList) { @@ -1857,7 +1861,15 @@ namespace Microsoft.Boogie { Multiple .bpl files supplied on the command line are concatenated into one Boogie program. - /proc:<p> : limits which procedures to check + /proc:<p> : Only check procedures matched by pattern <p>. This option + may be specified multiple times to match multiple patterns. + The pattern <p> matches the whole procedure name (i.e. + pattern ""foo"" will only match a procedure called foo and + not fooBar). The pattern <p> may contain * wildcards which + match any character zero or more times. For example the + pattern ""ab*d"" would match abd, abcd and abccd but not + Aabd nor abdD. The pattern ""*ab*d*"" would match abd, + abcd, abccd, Abd and abdD. /noResolve : parse only /noTypecheck : parse and resolve only @@ -1961,6 +1973,10 @@ namespace Microsoft.Boogie { 0 - do not use any verification result caching (default) 1 - use the basic verification result caching 2 - use the more advanced verification result caching + 3 - use the more advanced caching and report errors according + to the new source locations for errors and their + related locations (but not /errorTrace and CaptureState + locations) /verifySeparately verify each input program separately /removeEmptyBlocks:<c> |