summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/AbsyExpr.cs5
-rw-r--r--Source/Core/CommandLineOptions.cs46
-rw-r--r--Source/Provers/Isabelle/Prover.cs2
-rw-r--r--Source/VCGeneration/Check.cs14
-rw-r--r--Test/bitvectors/Answer8
-rw-r--r--Test/bitvectors/runtest.bat9
-rw-r--r--Test/extractloops/Answer4
-rw-r--r--Test/stratifiedinline/Answer66
-rw-r--r--Test/test15/Answer286
-rw-r--r--Test/test2/runtest.bat2
10 files changed, 178 insertions, 264 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 630f6f14..9a0fe64e 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -494,8 +494,6 @@ namespace Microsoft.Boogie {
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
- if (Val is BvConst && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None)
- tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");
this.Type = ShallowType;
}
@@ -2241,9 +2239,6 @@ namespace Microsoft.Boogie {
TypeParameters == null) {
TypeParamInstantiation tpInsts;
Type = Fun.Typecheck(ref Args, out tpInsts, tc);
- if (Type != null && Type.IsBv && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) {
- tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");
- }
TypeParameters = tpInsts;
}
IOverloadedAppliable oa = Fun as IOverloadedAppliable;
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ebad5cc..8647e79e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -241,7 +241,6 @@ namespace Microsoft.Boogie {
Z3Native,
ToInt
}
- public BvHandling Bitvectors = BvHandling.Z3Native;
public bool UseArrayTheory = false;
public bool MonomorphicArrays {
get {
@@ -945,31 +944,6 @@ namespace Microsoft.Boogie {
ForceBplErrors = true;
break;
- case "-bv":
- case "/bv":
- if (ps.ConfirmArgumentCount(1)) {
- if (TheProverFactory == null) {
- TheProverFactory = ProverFactory.Load("Z3");
- ProverName = "Z3".ToUpper();
- }
-
- switch (args[ps.i]) {
- case "n":
- Bitvectors = BvHandling.None;
- break;
- case "z":
- Bitvectors = BvHandling.Z3Native;
- break;
- case "i":
- Bitvectors = BvHandling.ToInt;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
- }
- break;
-
case "-contractInfer":
case "/contractInfer":
ContractInfer = true;
@@ -1918,15 +1892,6 @@ namespace Microsoft.Boogie {
{:verify false}
Skip verification of an implementation.
- {:forceBvZ3Native true}
- Verify the given implementation with the native Z3 bitvector
- handling. Only works if /bv:i (or /bv:z, but then it does not do
- anything) is given on the command line.
-
- {:forceBvInt true}
- Use int translation for the given implementation. Only work with
- /bv:z (or /bv:i).
-
{:vcs_max_cost N}
{:vcs_max_splits N}
{:vcs_max_keep_going_splits N}
@@ -1942,12 +1907,9 @@ namespace Microsoft.Boogie {
---- On functions ----------------------------------------------------------
+ {:builtin ""spec""}
{:bvbuiltin ""spec""}
- Z3 specific, used only with /bv:z.
-
- {:bvint ""fn""}
- With /bv:i rewrite the function to function symbol 'fn', except if
- the 'fn' is 'id', in which case just strip the function altogether.
+ Rewrite the function to built-in prover function symbol 'fn'.
{:never_pattern true}
Terms starting with this function symbol will never be
@@ -2177,10 +2139,6 @@ namespace Microsoft.Boogie {
statement in that position) is ignored in checking contexts
(like other free things); this option includes these free
loop invariants as assumes in both contexts
- /bv:<bv> : bitvector handling
- n = none
- z = native Z3 bitvectors (default)
- i = unsoundly translate bitvectors to integers
/inline:<i> : use inlining strategy <i> for procedures with the :inline
attribute, see /attrHelp for details:
none
diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 60a8de22..8bf6bbf0 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie.Isabelle {
public readonly bool AllTypes;
public IsabelleContext(string outputFilename, bool allTypes)
- : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/>(new string/*!*/[] { "bvInt", "bvDefSem", "bvint", "bvz", "external" }))) {
+ : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/> { "bvInt", "bvDefSem", "bvint", "bvz", "external" })) {
Contract.Requires(outputFilename != null);
this.OutputFilename = outputFilename;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 134cff4c..24e083d0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -49,19 +49,7 @@ namespace Microsoft.Boogie {
public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {
- if (impl == null)
- return CommandLineOptions.Clo.Bitvectors;
- bool force_int = false;
- bool force_native = false;
- cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);
- impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
- impl.CheckBooleanAttribute("forceBvInt", ref force_int);
- impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
- if (force_native)
- return CommandLineOptions.BvHandling.Z3Native;
- if (force_int)
- return CommandLineOptions.BvHandling.ToInt;
- return CommandLineOptions.Clo.Bitvectors;
+ return CommandLineOptions.BvHandling.Z3Native;
}
public bool WillingToHandle(Implementation impl, int timeout) {
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
index f0f65b04..e20474d9 100644
--- a/Test/bitvectors/Answer
+++ b/Test/bitvectors/Answer
@@ -28,12 +28,6 @@ Boogie program verifier finished with 1 verified, 0 errors
bv7.bpl(4,14): error: arguments of extract need to be integer literals
bv7.bpl(5,15): error: parentheses around bitvector bounds are not allowed
2 parse errors detected in bv7.bpl
--------------------- bv4.bpl - /bv:n --------------------
-bv4.bpl(3,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-bv4.bpl(3,13): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-bv4.bpl(5,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-4 type checking errors detected in bv4.bpl
-------------------- bv5.bpl --------------------
bv5.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -52,6 +46,6 @@ Boogie program verifier finished with 2 verified, 0 errors
-------------------- bv10.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
+-------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
index a0480645..2a140368 100644
--- a/Test/bitvectors/runtest.bat
+++ b/Test/bitvectors/runtest.bat
@@ -5,16 +5,13 @@ set BGEXE=..\..\Binaries\Boogie.exe
for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% /proverWarnings:1 /bv:z %* /logPrefix:-0 %%f
+ %BGEXE% /proverWarnings:1 %* %%f
)
-echo -------------------- bv4.bpl - /bv:n --------------------
-%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl
-
for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
-echo -------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
-%BGEXE% /bv:z /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl
+echo -------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------
+%BGEXE% /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index 9a6c95a3..954ea799 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -64,6 +64,10 @@ Boogie program verifier finished with 1 verified, 0 errors
t3.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
t3.bpl(19,3): anon0
+ t3.bpl(23,3): anon3_LoopHead
+ Inlined call to procedure foo begins
+ t3.bpl(11,5): anon0
+ Inlined call to procedure foo ends
t3.bpl(27,3): anon3_LoopBody
t3.bpl(23,3): anon3_LoopHead
Inlined call to procedure foo begins
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 290059d6..aee2722e 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -2,31 +2,31 @@
bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
- bar1.bpl(24,3): anon0
- Inlined call to procedure foo begins
- bar1.bpl(13,5): anon0
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
+ bar1.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar1.bpl(13,5): anon0
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar2.bpl
bar2.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- bar2.bpl(19,3): anon0
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(6,7): anon3_Then
- Inlined call to procedure foo ends
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(9,7): anon3_Else
- Inlined call to procedure foo ends
+ bar2.bpl(19,3): anon0
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(9,7): anon3_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(6,7): anon3_Then
+ Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error
bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
- bar3.bpl(38,3): anon0
- Inlined call to procedure foo begins
- bar3.bpl(18,3): anon0
- bar3.bpl(19,7): anon3_Then
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
+ bar3.bpl(38,3): anon0
+ Inlined call to procedure foo begins
+ bar3.bpl(18,3): anon0
+ bar3.bpl(19,7): anon3_Then
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(8,7): anon3_Then
+ Inlined call to procedure bar ends
Inlined call to procedure bar begins
bar3.bpl(7,3): anon0
- bar3.bpl(10,7): anon3_Else
+ bar3.bpl(8,7): anon3_Then
Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
Boogie program verifier finished with 0 verified, 1 error
-----
diff --git a/Test/test15/Answer b/Test/test15/Answer
index 11f0e658..4e3886aa 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -2,56 +2,49 @@
-------------------- NullInModel --------------------
Z3 error model:
partitions:
-*0 -> true
-*1 -> false
-*2 {@true} -> 3:int
-*3 {@false} -> 4:int
+*0 {%lbl%+24 %lbl%+37} -> true
+*1 {%lbl%@47} -> false
+*2 {s null}
+*3 {refType}
*4 {intType}
*5 {boolType}
-*6 {refType}
-*7 {s null}
-*8 -> 0:int
-*9 -> 1:int
-*10 -> 2:int
-*11
+*6 -> 0:int
+*7 -> 1:int
+*8 -> 2:int
+*9
function interpretations:
-$pow2 -> {
- *8 -> *9
- else -> #unspecified
-}
tickleBool -> {
- *1 -> *0
*0 -> *0
+ *1 -> *0
else -> #unspecified
}
-Ctor -> {
- *4 -> *8
- *5 -> *9
- *6 -> *10
+type -> {
+ *2 -> *3
else -> #unspecified
}
-type -> {
- *7 -> *6
+Ctor -> {
+ *4 -> *6
+ *5 -> *7
+ *3 -> *8
else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
-@true : *2
-@false : *3
+%lbl%+24 : *0
+%lbl%+37 : *0
+%lbl%@47 : *1
+s : *2
+null : *2
+refType : *3
intType : *4
boolType : *5
-refType : *6
-s : *7
-null : *7
valueToPartition:
True : *0
False : *1
-3 : *2
-4 : *3
-0 : *8
-1 : *9
-2 : *10
+0 : *6
+1 : *7
+2 : *8
End of model.
NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -62,45 +55,38 @@ Boogie program verifier finished with 0 verified, 1 error
-------------------- IntInModel --------------------
Z3 error model:
partitions:
-*0 -> true
-*1 -> false
-*2 {@true} -> 2:int
-*3 {@false} -> 3:int
-*4 {intType}
-*5 {boolType}
-*6 {i} -> 0:int
-*7 -> 1:int
-*8
+*0 {%lbl%+29 %lbl%+23} -> true
+*1 {%lbl%@39} -> false
+*2 {intType}
+*3 {boolType}
+*4 {i} -> 0:int
+*5 -> 1:int
+*6
function interpretations:
-$pow2 -> {
- *6 -> *7
- else -> #unspecified
-}
tickleBool -> {
- *1 -> *0
*0 -> *0
+ *1 -> *0
else -> #unspecified
}
Ctor -> {
- *4 -> *6
- *5 -> *7
+ *2 -> *4
+ *3 -> *5
else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
-@true : *2
-@false : *3
-intType : *4
-boolType : *5
-i : *6
+%lbl%+29 : *0
+%lbl%+23 : *0
+%lbl%@39 : *1
+intType : *2
+boolType : *3
+i : *4
valueToPartition:
True : *0
False : *1
-2 : *2
-3 : *3
-0 : *6
-1 : *7
+0 : *4
+1 : *5
End of model.
IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -111,66 +97,59 @@ Boogie program verifier finished with 0 verified, 1 error
-------------------- ModelTest --------------------
Z3 error model:
partitions:
-*0 -> true
-*1 -> false
-*2 {@true} -> 5:int
-*3 {@false} -> 6:int
-*4 {intType}
-*5 {boolType}
+*0 {%lbl%+64 %lbl%+119} -> true
+*1 {%lbl%@182} -> false
+*2 {s}
+*3 {j@2} -> 4:int
+*4 {boolType}
+*5 {intType}
*6 {refType}
-*7 {s}
-*8 {r}
-*9 {i@0} -> 1:int
-*10 {j@0} -> 2:int
-*11 {j@1} -> 3:int
-*12 {j@2} -> 4:int
-*13 -> 0:int
-*14
+*7 {i@0} -> 1:int
+*8 {j@0} -> 2:int
+*9 {j@1} -> 3:int
+*10 {r}
+*11 -> 0:int
+*12
function interpretations:
-$pow2 -> {
- *13 -> *9
- else -> #unspecified
-}
tickleBool -> {
- *1 -> *0
*0 -> *0
+ *1 -> *0
else -> #unspecified
}
-Ctor -> {
- *4 -> *13
- *5 -> *9
- *6 -> *10
+type -> {
+ *2 -> *6
+ *10 -> *6
else -> #unspecified
}
-type -> {
- *7 -> *6
- *8 -> *6
+Ctor -> {
+ *5 -> *11
+ *4 -> *7
+ *6 -> *8
else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
-@true : *2
-@false : *3
-intType : *4
-boolType : *5
+%lbl%+64 : *0
+%lbl%+119 : *0
+%lbl%@182 : *1
+s : *2
+j@2 : *3
+boolType : *4
+intType : *5
refType : *6
-s : *7
-r : *8
-i@0 : *9
-j@0 : *10
-j@1 : *11
-j@2 : *12
+i@0 : *7
+j@0 : *8
+j@1 : *9
+r : *10
valueToPartition:
True : *0
False : *1
-5 : *2
-6 : *3
-1 : *9
-2 : *10
-3 : *11
-4 : *12
-0 : *13
+4 : *3
+1 : *7
+2 : *8
+3 : *9
+0 : *11
End of model.
ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -199,86 +178,85 @@ Execution trace:
CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
*** MODEL
-@true -> 6
-@false -> 7
+%lbl%+112 -> true
+%lbl%+116 -> true
+%lbl%+110 -> true
+%lbl%+189 -> true
+%lbl%@334 -> false
+m@3 -> -1
+m@2 -> -1
+this -> *3
intType -> *4
-boolType -> *5
-RefType -> *6
-FieldNameType -> *7
-Heap -> *8
-this -> *9
-F -> *10
-@MV_state_const -> 8
+Heap -> *5
+FieldNameType -> *6
m@0 -> -2
r@0 -> -2
+boolType -> *8
+RefType -> *9
+F -> *10
+@MV_state_const -> 6
x@@4 -> 797
-m@2 -> -1
-m@3 -> -1
y@@1 -> **y@@1
r -> **r
m -> **m
-$pow2 -> {
- 0 -> 1
- else -> *23
-}
tickleBool -> {
- false -> true
true -> true
- else -> *23
-}
-Ctor -> {
- *4 -> 0
- *5 -> 1
- *6 -> 3
- *7 -> 4
- *19 -> 2
- else -> *23
+ false -> true
+ else -> true
}
type -> {
- *8 -> *19
- *9 -> *6
- *10 -> *7
+ *5 -> *13
+ *3 -> *9
+ *10 -> *6
-2 -> *4
- else -> *23
+ else -> *13
}
-MapType0Type -> {
- *6 *7 *4 -> *19
- else -> *23
-}
-MapType0TypeInv2 -> {
- *19 -> *4
- else -> *23
-}
-MapType0TypeInv1 -> {
- *19 -> *7
- else -> *23
-}
-MapType0TypeInv0 -> {
- *19 -> *6
- else -> *23
+Ctor -> {
+ *4 -> 0
+ *8 -> 1
+ *9 -> 3
+ *6 -> 4
+ *13 -> 2
+ else -> 0
}
@MV_state -> {
- 8 0 -> true
- 8 3 -> true
- 8 4 -> true
- 8 5 -> true
- else -> *23
+ 6 0 -> true
+ 6 3 -> true
+ 6 4 -> true
+ 6 5 -> true
+ else -> true
}
[3] -> {
- *8 *9 *10 -> -2
- else -> *23
+ *5 *3 *10 -> -2
+ else -> -2
}
U_2_int -> {
-2 -> -2
- else -> *23
+ else -> -2
+}
+MapType0TypeInv1 -> {
+ *13 -> *6
+ else -> *6
+}
+MapType0Type -> {
+ *9 *6 *4 -> *13
+ else -> *13
+}
+MapType0TypeInv2 -> {
+ *13 -> *4
+ else -> *4
+}
+MapType0TypeInv0 -> {
+ *13 -> *9
+ else -> *9
}
int_2_U -> {
-2 -> -2
- else -> *23
+ else -> -2
}
*** STATE <initial>
- Heap -> *8
- this -> *9
+ Heap -> *5
+ this -> *3
x -> 797
y -> **y@@1
r -> **r
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 3dc7d0c3..8ce2f66e 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -24,7 +24,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
)
echo -------------------- sk_hack.bpl --------------------
-%BGEXE% %* /noinfer /bv:z sk_hack.bpl
+%BGEXE% %* /noinfer sk_hack.bpl
for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
echo.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 13:40:33 +0000