cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Adjust ModelCheckerSettings in tools tests

Browse Source
This commit is contained in:
Leo Alt 2021-10-06 11:52:44 +02:00
parent a104443ac1
commit 2cbd496576
2 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/solc/CommandLineParser.cpp
View File

@ -149,6 +149,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
"--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-contracts=contract1.yul:A,contract2.yul:B",
"--model-checker-div-mod-no-slacks", "--model-checker-div-mod-no-slacks",
"--model-checker-engine=bmc", "--model-checker-engine=bmc",
"--model-checker-invariants=contract,reentrancy",
"--model-checker-show-unproved", "--model-checker-show-unproved",
"--model-checker-solvers=z3,smtlib2", "--model-checker-solvers=z3,smtlib2",
"--model-checker-targets=underflow,divByZero", "--model-checker-targets=underflow,divByZero",
@ -212,6 +213,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
{{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}},
true, true,
{true, false}, {true, false},
{{InvariantType::Contract, InvariantType::Reentrancy}},
true, true,
{false, true, true}, {false, true, true},
{{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}},
@ -285,6 +287,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options)
"contract2.yul:B", "contract2.yul:B",
"--model-checker-div-mod-no-slacks", // Ignored in assembly mode "--model-checker-div-mod-no-slacks", // Ignored in assembly mode
"--model-checker-engine=bmc", // Ignored in assembly mode "--model-checker-engine=bmc", // Ignored in assembly mode
"--model-checker-invariants=contract,reentrancy", // Ignored in assembly mode
"--model-checker-show-unproved", // Ignored in assembly mode "--model-checker-show-unproved", // Ignored in assembly mode
"--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode "--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode
"--model-checker-targets=" // Ignored in assembly mode "--model-checker-targets=" // Ignored in assembly mode
@ -375,6 +378,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options)
"contract2.yul:B", "contract2.yul:B",
"--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode "--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode
"--model-checker-engine=bmc", // Ignored in Standard JSON mode "--model-checker-engine=bmc", // Ignored in Standard JSON mode
"--model-checker-invariants=contract,reentrancy", // Ignored in Standard JSON mode
"--model-checker-show-unproved", // 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-solvers=z3,smtlib2", // Ignored in Standard JSON mode
"--model-checker-targets=" // Ignored in Standard JSON mode "--model-checker-targets=" // Ignored in Standard JSON mode

1
test/tools/fuzzer_common.cpp
View File

@ -106,6 +106,7 @@ void FuzzerUtil::testCompiler(
frontend::ModelCheckerContracts::Default(), frontend::ModelCheckerContracts::Default(),
/*divModWithSlacks*/true, /*divModWithSlacks*/true,
frontend::ModelCheckerEngine::All(), frontend::ModelCheckerEngine::All(),
frontend::ModelCheckerInvariants::All(),
/*showUnproved=*/false, /*showUnproved=*/false,
smtutil::SMTSolverChoice::All(), smtutil::SMTSolverChoice::All(),
frontend::ModelCheckerTargets::Default(), frontend::ModelCheckerTargets::Default(),