diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.ssc | 12 |
2 files changed, 12 insertions, 2 deletions
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index 5c844953..ee5d3d10 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -40,7 +40,7 @@ namespace VC {
Expr! expr = assrt.Expr;
- switch (CommandLineOptions.Clo.UseSubsumption) {
+ switch (Wlp.Subsumption(assrt)) {
case CommandLineOptions.SubsumptionOption.Never:
expr = Expr.True;
break;
diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc index 003352d7..e70b332f 100644 --- a/Source/VCGeneration/Wlp.ssc +++ b/Source/VCGeneration/Wlp.ssc @@ -59,7 +59,7 @@ namespace VC { } else {
int id = ac.UniqueId;
ctxt.Label2absy[id] = ac;
- switch (CommandLineOptions.Clo.UseSubsumption) {
+ switch (Subsumption(ac)) {
case CommandLineOptions.SubsumptionOption.Never:
break;
case CommandLineOptions.SubsumptionOption.Always:
@@ -89,6 +89,16 @@ namespace VC { assert false; // unexpected command
}
}
+
+ public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd! ac) {
+ int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1);
+ switch (n) {
+ case 0: return CommandLineOptions.SubsumptionOption.Never;
+ case 1: return CommandLineOptions.SubsumptionOption.NotForQuantifiers;
+ case 2: return CommandLineOptions.SubsumptionOption.Always;
+ default: return CommandLineOptions.Clo.UseSubsumption;
+ }
+ }
public static VCExpr! RegExpr(RE! r, VCExpr! N, VCContext! ctxt)
{
|