From 8ce878621a254a20816e09f1172142ff308b9766 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 11 Aug 2021 10:54:03 +0200 Subject: [PATCH] Make show unproved CLI a flag --- docs/smtchecker.rst | 2 +- solc/CommandLineParser.cpp | 8 ++------ .../args | 1 - .../err | 3 --- .../input.sol | 12 ------------ .../model_checker_show_unproved_false_bmc/args | 1 - .../model_checker_show_unproved_false_bmc/err | 1 - .../model_checker_show_unproved_false_bmc/input.sol | 12 ------------ .../model_checker_show_unproved_false_chc/args | 1 - .../model_checker_show_unproved_false_chc/err | 1 - .../model_checker_show_unproved_false_chc/input.sol | 12 ------------ .../args | 2 +- .../model_checker_show_unproved_true_bmc/args | 2 +- .../model_checker_show_unproved_true_chc/args | 2 +- .../args | 1 - .../err | 1 - .../exit | 1 - .../input.sol | 12 ------------ test/solc/CommandLineParser.cpp | 6 +++--- 19 files changed, 9 insertions(+), 72 deletions(-) delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_all_engines/args delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_all_engines/err delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_bmc/args delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_bmc/err delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_chc/args delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_chc/err delete mode 100644 test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol delete mode 100644 test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args delete mode 100644 test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err delete mode 100644 test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit delete mode 100644 test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 65b21a10e..d1e8f6c81 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -488,7 +488,7 @@ Unproved Targets If there are any unproved targets, the SMTChecker issues one warning stating how many unproved targets there are. If the user wishes to see all the specific -unproved targets, the CLI option ``--model-checker-show-unproved true`` and +unproved targets, the CLI option ``--model-checker-show-unproved`` and the JSON option ``settings.modelChecker.showUnproved = true`` can be used. Verified Contracts diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index f23865c2f..e8d8b8a6e 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -733,8 +733,7 @@ General Information)").c_str(), ) ( g_strModelCheckerShowUnproved.c_str(), - po::value()->value_name("false,true")->default_value(false), - "Select whether to show all unproved targets." + "Show all unproved targets separately." ) ( g_strModelCheckerSolvers.c_str(), @@ -1114,10 +1113,7 @@ General Information)").c_str(), } if (m_args.count(g_strModelCheckerShowUnproved)) - { - bool showUnproved = m_args[g_strModelCheckerShowUnproved].as(); - m_options.modelChecker.settings.showUnproved = showUnproved; - } + m_options.modelChecker.settings.showUnproved = true; if (m_args.count(g_strModelCheckerSolvers)) { diff --git a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/args deleted file mode 100644 index 5f6883c76..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine all --model-checker-show-unproved false diff --git a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/err b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/err deleted file mode 100644 index 45c38ef35..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/err +++ /dev/null @@ -1,3 +0,0 @@ -Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. diff --git a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol deleted file mode 100644 index 567c9cd2b..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol +++ /dev/null @@ -1,12 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C { - struct S { - uint x; - } - S s; - function f(bool b) public { - s.x |= b ? 1 : 2; - assert(s.x > 0); - } -} diff --git a/test/cmdlineTests/model_checker_show_unproved_false_bmc/args b/test/cmdlineTests/model_checker_show_unproved_false_bmc/args deleted file mode 100644 index 40fcde62b..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_bmc/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine bmc --model-checker-show-unproved false diff --git a/test/cmdlineTests/model_checker_show_unproved_false_bmc/err b/test/cmdlineTests/model_checker_show_unproved_false_bmc/err deleted file mode 100644 index f8d0af2f4..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_bmc/err +++ /dev/null @@ -1 +0,0 @@ -Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. diff --git a/test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol b/test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol deleted file mode 100644 index 567c9cd2b..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol +++ /dev/null @@ -1,12 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C { - struct S { - uint x; - } - S s; - function f(bool b) public { - s.x |= b ? 1 : 2; - assert(s.x > 0); - } -} diff --git a/test/cmdlineTests/model_checker_show_unproved_false_chc/args b/test/cmdlineTests/model_checker_show_unproved_false_chc/args deleted file mode 100644 index c14333f44..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_chc/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine chc --model-checker-show-unproved false diff --git a/test/cmdlineTests/model_checker_show_unproved_false_chc/err b/test/cmdlineTests/model_checker_show_unproved_false_chc/err deleted file mode 100644 index 77083185f..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_chc/err +++ /dev/null @@ -1 +0,0 @@ -Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. diff --git a/test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol b/test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol deleted file mode 100644 index 567c9cd2b..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol +++ /dev/null @@ -1,12 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C { - struct S { - uint x; - } - S s; - function f(bool b) public { - s.x |= b ? 1 : 2; - assert(s.x > 0); - } -} diff --git a/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args index 4ccfd2e96..fbc67f1ee 100644 --- a/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args +++ b/test/cmdlineTests/model_checker_show_unproved_true_all_engines/args @@ -1 +1 @@ ---model-checker-engine all --model-checker-show-unproved true +--model-checker-engine all --model-checker-show-unproved diff --git a/test/cmdlineTests/model_checker_show_unproved_true_bmc/args b/test/cmdlineTests/model_checker_show_unproved_true_bmc/args index 79cae9260..319afff3f 100644 --- a/test/cmdlineTests/model_checker_show_unproved_true_bmc/args +++ b/test/cmdlineTests/model_checker_show_unproved_true_bmc/args @@ -1 +1 @@ ---model-checker-engine bmc --model-checker-show-unproved true +--model-checker-engine bmc --model-checker-show-unproved diff --git a/test/cmdlineTests/model_checker_show_unproved_true_chc/args b/test/cmdlineTests/model_checker_show_unproved_true_chc/args index f992f4d0c..cf2a73372 100644 --- a/test/cmdlineTests/model_checker_show_unproved_true_chc/args +++ b/test/cmdlineTests/model_checker_show_unproved_true_chc/args @@ -1 +1 @@ ---model-checker-engine chc --model-checker-show-unproved true +--model-checker-engine chc --model-checker-show-unproved diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args deleted file mode 100644 index b20188349..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine all --model-checker-show-unproved aaa diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err deleted file mode 100644 index 9ece92874..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err +++ /dev/null @@ -1 +0,0 @@ -the argument ('aaa') for option '--model-checker-show-unproved' is invalid. Valid choices are 'on|off', 'yes|no', '1|0' and 'true|false' diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit deleted file mode 100644 index d00491fd7..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit +++ /dev/null @@ -1 +0,0 @@ -1 diff --git a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol deleted file mode 100644 index 567c9cd2b..000000000 --- a/test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol +++ /dev/null @@ -1,12 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C { - struct S { - uint x; - } - S s; - function f(bool b) public { - s.x |= b ? 1 : 2; - assert(s.x > 0); - } -} diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index f97636a94..d13c8a27b 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -146,7 +146,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-div-mod-no-slacks", "--model-checker-engine=bmc", - "--model-checker-show-unproved=true", + "--model-checker-show-unproved", "--model-checker-solvers=z3,smtlib2", "--model-checker-targets=underflow,divByZero", "--model-checker-timeout=5", @@ -278,7 +278,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options) "contract2.yul:B", "--model-checker-div-mod-no-slacks", // Ignored in assembly mode "--model-checker-engine=bmc", // Ignored in assembly mode - "--model-checker-show-unproved=true", // Ignored in assembly mode + "--model-checker-show-unproved", // Ignored in assembly mode "--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode "--model-checker-targets=" // Ignored in assembly mode "underflow," @@ -378,7 +378,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options) "contract2.yul:B", "--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode "--model-checker-engine=bmc", // Ignored in Standard JSON mode - "--model-checker-show-unproved=true", // Ignored in Standard JSON mode + "--model-checker-show-unproved", // Ignored in Standard JSON mode "--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode "--model-checker-targets=" // Ignored in Standard JSON mode "underflow,"