diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index f1d97551a..cbc7f6511 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.0.11 + 3.0.12 net6.0 false Boogie diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index faf89dc7b..ff4755836 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -1257,6 +1257,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.GetIntArgument(x => normalizeDeclarationOrder = x); return true; + case "prune": + ps.GetIntArgument(x => Prune = x); + return true; + default: bool optionValue = false; if (ps.CheckBooleanFlag("printUnstructured", x => optionValue = x)) @@ -1318,7 +1322,6 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("trustSequentialization", x => trustSequentialization = x) || ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) || ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) || - ps.CheckBooleanFlag("prune", x => Prune = x) || ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) ) { @@ -1889,12 +1892,14 @@ Boogie automatically detects monomorphic programs and enables the SMT theory of arrays. This option allows the use of axioms instead. /reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined to be +, instead of +. - /prune - Turn on pruning. Pruning will remove any top-level Boogie declarations - that are not accessible by the implementation that is about to be verified. - Without pruning, due to the unstable nature of SMT solvers, - a change to any part of a Boogie program has the potential - to affect the verification of any other part of the program. + /prune: + 0 - Turn off pruning. + 1 - Turn on pruning (default). Pruning will remove any top-level + Boogie declarations that are not accessible by the implementation + that is about to be verified. Without pruning, due to the unstable + nature of SMT solvers, a change to any part of a Boogie program + has the potential to affect the verification of any other part of + the program. Only use this if your program contains uses clauses where required, otherwise pruning will break your program. diff --git a/Test/commandline/noprune.bpl b/Test/commandline/noprune.bpl new file mode 100644 index 000000000..cf6e4ba4f --- /dev/null +++ b/Test/commandline/noprune.bpl @@ -0,0 +1,12 @@ +// RUN: %parallel-boogie -quiet -prune:0 -normalizeNames:0 -proverLog:"%t.noprune.smt2" "%s" +// RUN: %OutputCheck --file-to-check "%t.noprune.smt2" "%s" +// CHECK: ThisIsAFunction + +function ThisIsAFunction(): int uses { + axiom ThisIsAFunction() == 2; +} + +procedure P() +{ + assert 1 == 1; +} diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index 850c6b833..8fbc5a243 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -91,13 +91,13 @@ // CHECK: xy_sum // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage" // RUN: %diff "%s.expect" "%t.coverage" -// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a" +// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune:1 "%s" > "%t.coverage-a" // RUN: %diff "%s.expect" "%t.coverage-a" -// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune "%s" > "%t.coverage-p" +// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune:1 "%s" > "%t.coverage-p" // RUN: %diff "%s.expect" "%t.coverage-p" -// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d" +// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune:1 "%s" > "%t.coverage-d" // RUN: %diff "%s.expect" "%t.coverage-d" -// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n" +// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune:1 "%s" > "%t.coverage-n" // RUN: %diff "%s.expect" "%t.coverage-n" procedure testRequiresAssign(n: int) diff --git a/Test/dafny/dafny-issue-4804.bpl b/Test/dafny/dafny-issue-4804.bpl index 747c9b313..2aa0b4b46 100644 --- a/Test/dafny/dafny-issue-4804.bpl +++ b/Test/dafny/dafny-issue-4804.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 /prune "%s" > "%t" +// RUN: %parallel-boogie /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 /prune:1 "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t" // CHECK: Boogie program verifier finished with 3 verified, 0 errors, 1 out of resource // dafny 4.3.0.0 diff --git a/Test/pruning/IncludeDep.bpl b/Test/pruning/IncludeDep.bpl index 69f33e240..f800b6528 100644 --- a/Test/pruning/IncludeDep.bpl +++ b/Test/pruning/IncludeDep.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" function f1 (x: int) : int; diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 956498d8c..56a21f196 100644 --- a/Test/pruning/MonomorphicSplit.bpl +++ b/Test/pruning/MonomorphicSplit.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /errorTrace:0 /printPruned:"%t" "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /errorTrace:0 /printPruned:"%t" "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t-after-monomorphicSplit.bpl" // The following checks are a bit simplistic, but this is diff --git a/Test/pruning/NonmonomorphicSplit.bpl b/Test/pruning/NonmonomorphicSplit.bpl index 17fbb7df6..0e61a7065 100644 --- a/Test/pruning/NonmonomorphicSplit.bpl +++ b/Test/pruning/NonmonomorphicSplit.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /trace /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /trace /errorTrace:0 "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t" // Related PR #767. diff --git a/Test/pruning/Triggers.bpl b/Test/pruning/Triggers.bpl index 966b28cb2..e1116afe7 100644 --- a/Test/pruning/Triggers.bpl +++ b/Test/pruning/Triggers.bpl @@ -1,4 +1,4 @@ - // RUN: %parallel-boogie /prune /errorTrace:0 "%s" > "%t" + // RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" function f1 (x: int) : bool; @@ -32,4 +32,4 @@ axiom (forall x: int :: {f5(f4(x)), f4(x)} f4(x)); procedure twoTriggers(x : int) ensures f4(x); { -} \ No newline at end of file +} diff --git a/Test/pruning/UsesClauses.bpl b/Test/pruning/UsesClauses.bpl index 0ec5f06c5..0ebe6cfe8 100644 --- a/Test/pruning/UsesClauses.bpl +++ b/Test/pruning/UsesClauses.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /printPruned:"%tpruned" /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /printPruned:"%tpruned" /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // UNSUPPORTED: batch_mode diff --git a/Test/test15/CommonVariablesPruning.bpl b/Test/test15/CommonVariablesPruning.bpl index 513c4c6c5..0cec41d8b 100644 --- a/Test/test15/CommonVariablesPruning.bpl +++ b/Test/test15/CommonVariablesPruning.bpl @@ -1,6 +1,6 @@ // VcsCores:1 means we only use a single solver for both procedures in this Boogie program. // Prune triggers a full reset after using the solver on one problem -// RUN: %boogie "%s" -typeEncoding:p -vcsCores:1 -normalizeNames:1 -prune -mv:- > "%t" +// RUN: %boogie "%s" -typeEncoding:p -vcsCores:1 -normalizeNames:1 -prune:1 -mv:- > "%t" // RUN: %diff "%s.expect" "%t" --ignore-matching-lines='else ->' // Part of the MultiDimArray test from Dafny: https://github.com/dafny-lang/dafny/blob/cc913d9159ded2ad131c048135f817e49f500e50/Test/dafny0/MultiDimArray.dfy