diff options
| author |  akashlal <unknown> | 2013-04-18 17:50:18 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-04-18 17:50:18 +0530 |
| commit | a2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 (patch) | |
| tree | 48d4d5b6d86968a058ffbbe9661518ec763b9204 /Source/BoogieDriver | |
| parent | 308a4d37f063384cb8de166b248d9377c904e77c (diff) | |
Nice clean re-implementation of AbstractHoudini. And tests
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 38 |
1 files changed, 34 insertions, 4 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9d1038f5..9b31c31e 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -639,15 +639,45 @@ namespace Microsoft.Boogie { {
if (CommandLineOptions.Clo.AbstractHoudini != null)
{
- CommandLineOptions.Clo.PrintErrorModel = 1;
+ //CommandLineOptions.Clo.PrintErrorModel = 1;
CommandLineOptions.Clo.UseArrayTheory = true;
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
CommandLineOptions.Clo.ProverCCLimit = 1;
+ CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never;
+
+ // Declare abstract domains
+ var domains = new List<System.Tuple<string, Houdini.IAbstractDomain>>(new System.Tuple<string, Houdini.IAbstractDomain>[] {
+ System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain),
+ System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute<Houdini.ConstantProp>() 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;
}
|