Adjust tests/tools

This commit is contained in:
Leo Alt 2021-10-12 11:32:25 +02:00
parent 397bd7da4f
commit 4b1cfcd54e
2 changed files with 5 additions and 0 deletions

View File

@ -145,6 +145,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-ext-calls=trusted",
"--model-checker-invariants=contract,reentrancy",
"--model-checker-show-unproved",
"--model-checker-solvers=z3,smtlib2",
@ -211,6 +212,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
{{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}},
true,
{true, false},
{ModelCheckerExtCalls::Mode::TRUSTED},
{{InvariantType::Contract, InvariantType::Reentrancy}},
true,
{false, true, true},
@ -288,6 +290,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-ext-calls=trusted", // Ignored in assembly mode
"--model-checker-invariants=contract,reentrancy", // Ignored in assembly mode
"--model-checker-show-unproved", // Ignored in assembly mode
"--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode
@ -385,6 +388,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-ext-calls=trusted", // 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-solvers=z3,smtlib2", // Ignored in Standard JSON mode

View File

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