diff options
Diffstat (limited to 'Source/VCExpr/TypeErasureArguments.ssc')
| -rw-r--r-- | Source/VCExpr/TypeErasureArguments.ssc | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/Source/VCExpr/TypeErasureArguments.ssc b/Source/VCExpr/TypeErasureArguments.ssc index 98baf874..4fe37a4e 100644 --- a/Source/VCExpr/TypeErasureArguments.ssc +++ b/Source/VCExpr/TypeErasureArguments.ssc @@ -148,6 +148,7 @@ namespace Microsoft.Boogie.TypeErasure string! baseName = synonym.Name;
int typeParamNum = abstractedType.FreeVariables.Length +
abstractedType.TypeParameters.Length;
+
int arity = typeParamNum + abstractedType.Arguments.Length;
Type![]! selectTypes = new Type! [arity + 2];
@@ -160,8 +161,13 @@ namespace Microsoft.Boogie.TypeErasure storeTypes[i] = AxBuilder.T;
}
// Fill in the map type
- selectTypes[i] = AxBuilder.U;
- storeTypes[i] = AxBuilder.U;
+ if (CommandLineOptions.Clo.UseArrayTheory) {
+ selectTypes[i] = abstractedType;
+ storeTypes[i] = abstractedType;
+ } else {
+ selectTypes[i] = AxBuilder.U;
+ storeTypes[i] = AxBuilder.U;
+ }
i++;
// Fill in the index types
foreach (Type! type in abstractedType.Arguments)
@@ -186,17 +192,25 @@ namespace Microsoft.Boogie.TypeErasure }
i++;
// Fill in the map type which is the output of the store function
- storeTypes[i] = AxBuilder.U;
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ storeTypes[i] = abstractedType;
+ else
+ storeTypes[i] = AxBuilder.U;
NonNullType.AssertInitialized(selectTypes);
NonNullType.AssertInitialized(storeTypes);
- select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
+ select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);
-
- AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
+
+ if (CommandLineOptions.Clo.UseArrayTheory) {
+ select.AddAttribute("builtin", "select");
+ store.AddAttribute("builtin", "store");
+ } else {
+ AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));
- AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,
+ AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,
abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));
+ }
}
///////////////////////////////////////////////////////////////////////////
|