diff options
| author |  allydonaldson <unknown> | 2013-04-30 15:45:47 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-04-30 15:45:47 +0100 |
| commit | 77aeb920de2c3cd22a1296700305539f28f6761c (patch) | |
| tree | cf140a2c6ced506e28d10f3e2d8937815354e652 /Source/BoogieDriver | |
| parent | 89c7d4c339f58dc9ec39b14b0b2a4120f2689322 (diff) | |
| parent | 8d06e693c56205a1d2ba4c25d850c7c6676e19a8 (diff) | |
Merge
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 44 |
1 files changed, 39 insertions, 5 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 4531b9bb..c12ba47d 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -651,15 +651,49 @@ namespace Microsoft.Boogie { {
if (CommandLineOptions.Clo.AbstractHoudini != null)
{
- CommandLineOptions.Clo.PrintErrorModel = 1;
+ //CommandLineOptions.Clo.PrintErrorModel = 1;
+ CommandLineOptions.Clo.UseProverEvaluate = true;
+ CommandLineOptions.Clo.ModelViewFile = "z3model";
CommandLineOptions.Clo.UseArrayTheory = true;
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
- 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("PredicateAbs", new Houdini.PredicateAbsElem() 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)
+ });
+
+ domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2));
+
+ // Find the abstract domain
+ Houdini.IAbstractDomain domain = null;
+ foreach (var tup in domains)
+ {
+ if (tup.Item1 == CommandLineOptions.Clo.AbstractHoudini)
+ {
+ domain = tup.Item2;
+ break;
+ }
+ }
+ if (domain == null)
+ {
+ Console.WriteLine("Domain {0} not found", CommandLineOptions.Clo.AbstractHoudini);
+ Console.WriteLine("Supported domains are:");
+ domains.Iter(tup => Console.WriteLine(" {0}", tup.Item1));
+ throw new Houdini.AbsHoudiniInternalError("Domain not found");
+ }
// Run Abstract Houdini
- Houdini.PredicateAbs.Initialize(program);
- var abs = new Houdini.AbstractHoudini(program);
- abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
+ var abs = new Houdini.AbsHoudini(program, domain);
+ abs.ComputeSummaries();
+
+ //Houdini.PredicateAbs.Initialize(program);
+ //var abs = new Houdini.AbstractHoudini(program);
+ //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
return PipelineOutcome.Done;
}
|