diff options
| author |  rustanleino <unknown> | 2010-03-13 03:30:09 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-13 03:30:09 +0000 |
| commit | d83d1f3813e2765db4e3855adcb10fc3319a737f (patch) | |
| tree | e6291ebf6ab4993644926825d8e35379ef05a002 /Source/VCGeneration | |
| parent | c48d205507068bcce227645acc7a07add0561820 (diff) | |
Dafny: Added definedness checks for all statements (previously, some were missing)
Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
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)
{
|