diff options
| author |  akashlal <unknown> | 2013-05-03 11:07:05 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-05-03 11:07:05 +0530 |
| commit | 4428ac1f7e5520a23d256638c98c9570bd943169 (patch) | |
| tree | d798ff4f9cc86cbfc4f7da07f65207a4752726c7 /Source/BoogieDriver | |
| parent | 4024e730fe78f4f210b497041ca083b1464426b5 (diff) | |
Some code refactoring
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 31 |
1 files changed, 1 insertions, 30 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index c12ba47d..52e3c3fc 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -656,36 +656,7 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ModelViewFile = "z3model";
CommandLineOptions.Clo.UseArrayTheory = true;
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
- // 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");
- }
+ var domain = Houdini.AbstractDomainFactory.Initialize(CommandLineOptions.Clo.AbstractHoudini);
// Run Abstract Houdini
var abs = new Houdini.AbsHoudini(program, domain);
|