diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.ssc | 14 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 7 |
2 files changed, 19 insertions, 2 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index fc706e2c..00142344 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -429,6 +429,20 @@ namespace Microsoft.Boogie return true;
}
+ public void AddAttribute(string! name, object! val)
+ {
+ QKeyValue kv;
+ for (kv = this.Attributes; kv != null; kv = kv.Next) {
+ if (kv.Key == name) {
+ kv.Params.Add(val);
+ break;
+ }
+ }
+ if (kv == null) {
+ Attributes = new QKeyValue(tok, name, new List<object!>(new object![] { val }), Attributes);
+ }
+ }
+
public abstract void Emit(TokenTextWriter! stream, int level);
public abstract void Register(ResolutionContext! rc);
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index d3eb2eba..5912220d 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -151,6 +151,8 @@ namespace Microsoft.Boogie public enum BvHandling { None, Z3Native, ToInt }
public BvHandling Bitvectors = BvHandling.Z3Native;
+ public bool UseArrayTheory = false;
+
public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
invariant 0 <= StepsBeforeWidening && StepsBeforeWidening <= 9;
@@ -788,7 +790,7 @@ namespace Microsoft.Boogie }
}
break;
-
+
case "-contractInfer":
case "/contractInfer":
ContractInfer = true;
@@ -1132,7 +1134,8 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||
ps.CheckBooleanFlag("z3types", ref Z3types) ||
ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
- ps.CheckBooleanFlag("monomorphize", ref Monomorphize)
+ ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
+ ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory)
)
{
// one of the boolean flags matched
|