summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
authorGravatar Ken McMillan <kenmcmil@microsoft.com>2013-05-07 17:40:40 -0700
committerGravatar Ken McMillan <kenmcmil@microsoft.com>2013-05-07 17:40:40 -0700
commit9a9991f2131de8e78035581ea2569ba187318ff0 (patch)
tree5f2c0d4e85c9713f4d6663d26b49f67b5fbb27f0 /Source/VCGeneration
parent77aeb920de2c3cd22a1296700305539f28f6761c (diff)
Adding fixedpoint engine backend
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r--Source/VCGeneration/Check.cs5
-rw-r--r--Source/VCGeneration/VC.cs2
-rw-r--r--Source/VCGeneration/VCGeneration.csproj3
3 files changed, 9 insertions, 1 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index fe4b4b99..607476e7 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -405,6 +405,11 @@ namespace Microsoft.Boogie {
}
}
public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);
+
+ public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler, out RPFP.Node cex)
+ {
+ throw new System.NotImplementedException();
+ }
[NoDefaultContract]
public abstract Outcome CheckOutcome(ErrorHandler handler);
public virtual string[] CalculatePath(int controlFlowConstant) {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bcf0b0e5..3748d7f7 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1356,7 +1356,7 @@ namespace VC {
vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Dag:
- if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {
+ if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags || CommandLineOptions.Clo.FixedPointEngine != null) {
vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), proverContext, out assertionCount);
} else {
vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 0c98a891..f724307b 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -147,7 +147,10 @@
<Compile Include="Check.cs" />
<Compile Include="ConditionGeneration.cs" />
<Compile Include="Context.cs" />
+ <Compile Include="ExprExtensions.cs" />
+ <Compile Include="FixedpointVC.cs" />
<Compile Include="OrderingAxioms.cs" />
+ <Compile Include="RPFP.cs" />
<Compile Include="StratifiedVC.cs" />
<Compile Include="VC.cs" />
<Compile Include="..\version.cs" />