From 4b1cfcd54e20935fb6e55f2e6ddc27599fa191ea Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 12 Oct 2021 11:32:25 +0200 Subject: [PATCH] Adjust tests/tools --- test/solc/CommandLineParser.cpp | 4 ++++ test/tools/fuzzer_common.cpp | 1 + 2 files changed, 5 insertions(+) diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 22b3bd835..78f973f40 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -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 diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 094a84554..22c55f0d2 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -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(),