diff options
author | akashlal <unknown> | 2013-04-25 13:51:18 +0530 |
---|---|---|
committer | akashlal <unknown> | 2013-04-25 13:51:18 +0530 |
commit | 410f9a6ade1e16402e283e39bb68e21bb9a8c10b (patch) | |
tree | 326d4d6c9ef8ce259200a40851c6027c2c0cb3c4 /Source/BoogieDriver | |
parent | 1737682c92f641f42efd47318321e03d955040a7 (diff) |
AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,
few bug fixes, hack to support missing prover declarations.
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 0ffa5619..f3194256 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -649,8 +649,10 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ProverCCLimit = 1;
// Declare abstract domains
var domains = new List<System.Tuple<string, Houdini.IAbstractDomain>>(new System.Tuple<string, Houdini.IAbstractDomain>[] {
+ System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain),
System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain),
System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain),
+ System.Tuple.Create("IA[HoudiniConst]", new Houdini.IndependentAttribute<Houdini.HoudiniConst>() as Houdini.IAbstractDomain),
System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute<Houdini.ConstantProp>() as Houdini.IAbstractDomain),
System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute<Houdini.Intervals>() as Houdini.IAbstractDomain)
});
|