Merge pull request #11782 from ethereum/smt_show_unproved_flag

[SMTChecker] Make show unproved CLI a flag

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

solc/CommandLineParser.cpp

@@ -733,8 +733,7 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerShowUnproved.c_str(),
-			po::value<bool>()->value_name("false,true")->default_value(false),
+			"Show all unproved targets separately."
-			"Select whether to show all unproved targets."
 		)
 		(
 			g_strModelCheckerSolvers.c_str(),
@@ -1114,10 +1113,7 @@ General Information)").c_str(),
 	}
 
 	if (m_args.count(g_strModelCheckerShowUnproved))
-	{
+		m_options.modelChecker.settings.showUnproved = true;
-		bool showUnproved = m_args[g_strModelCheckerShowUnproved].as<bool>();
-		m_options.modelChecker.settings.showUnproved = showUnproved;
-	}
 
 	if (m_args.count(g_strModelCheckerSolvers))
 	{

test/cmdlineTests/model_checker_show_unproved_false_all_engines/args

@@ -1 +0,0 @@
---model-checker-engine all --model-checker-show-unproved false

test/cmdlineTests/model_checker_show_unproved_false_all_engines/err

@@ -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.

test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol

@@ -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);
-    }
-}

test/cmdlineTests/model_checker_show_unproved_false_bmc/args

@@ -1 +0,0 @@
---model-checker-engine bmc --model-checker-show-unproved false

test/cmdlineTests/model_checker_show_unproved_false_bmc/err

@@ -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.

test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol

@@ -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);
-    }
-}

test/cmdlineTests/model_checker_show_unproved_false_chc/args

@@ -1 +0,0 @@
---model-checker-engine chc --model-checker-show-unproved false

test/cmdlineTests/model_checker_show_unproved_false_chc/err

@@ -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.

test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol

@@ -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);
-    }
-}

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

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

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

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args

@@ -1 +0,0 @@
---model-checker-engine all --model-checker-show-unproved aaa

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err

@@ -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'

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit

@@ -1 +0,0 @@
-1

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol

@@ -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);
-    }
-}

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,"