diff options
| author |  allydonaldson <unknown> | 2013-06-07 17:00:07 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-06-07 17:00:07 +0100 |
| commit | 471a652e56da9b8d24a72d77688c360abf613bef (patch) | |
| tree | 6abcca1343dafac57c441454a986ea480503a5dc /Source/Core | |
| parent | 8cd9a8f63d7b13281e76ffcdd255842de977bb23 (diff) | |
| parent | 6547ad9261c353a5c1228a8876b684ac8627533f (diff) | |
Merge
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 35 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 6 |
2 files changed, 40 insertions, 1 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c3a9a164..55b37f13 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2567,6 +2567,41 @@ namespace Microsoft.Boogie { }
}
+ public string Checksum
+ {
+ get
+ {
+ return FindStringAttribute("checksum");
+ }
+ }
+
+ public string Id
+ {
+ get
+ {
+ var id = FindStringAttribute("id");
+ if (id == null)
+ {
+ id = Name + ":0";
+ }
+ return id;
+ }
+ }
+
+ public int Priority
+ {
+ get
+ {
+ int priority = 0;
+ CheckIntAttribute("priority", ref priority);
+ if (priority <= 0)
+ {
+ priority = 1;
+ }
+ return priority;
+ }
+ }
+
public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)
: this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {
Contract.Requires(structuredStmts != null);
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 420e5abd..dc69a3e8 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -363,6 +363,7 @@ namespace Microsoft.Boogie { Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3); // 0 = print only structured, 1 = both structured and unstructured, 2 = only unstructured
}
+ public bool VerifySnapshots;
public string PrintFile = null;
public int PrintUnstructured = 0;
public int DoomStrategy = -1;
@@ -464,6 +465,7 @@ namespace Microsoft.Boogie { public string PrintCFGPrefix = null;
public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
public bool UseArrayTheory = false;
+ public bool WeakArrayTheory = false;
public bool UseLabels = true;
public bool MonomorphicArrays {
get {
@@ -1308,6 +1310,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
+ ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) ||
ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||
ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||
@@ -1317,7 +1320,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
- ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)
+ ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
+ ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots)
) {
// one of the boolean flags matched
return true;
|