From 5a58dff96dc46fa2960a1c1e7c6b89217ccdce70 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 10 Apr 2022 13:38:01 +0000 Subject: [PATCH] CONTRACTS: apply: use previously computed mode There is no need to do repeated lookups. --- src/goto-instrument/contracts/contracts.cpp | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6793bc025d8..082d4c8f31f 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -817,7 +817,7 @@ void code_contractst::apply_function_contract( } } - const auto &mode = symbol_table.lookup_ref(target_function).mode; + const auto &mode = function_symbol.mode; is_fresh_replacet is_fresh(*this, log, target_function); is_fresh.create_declarations(); @@ -830,10 +830,7 @@ void code_contractst::apply_function_contract( replace(requires); goto_programt assertion; - converter.goto_convert( - code_assertt(requires), - assertion, - symbol_table.lookup_ref(target_function).mode); + converter.goto_convert(code_assertt(requires), assertion, mode); assertion.instructions.back().source_location_nonconst() = requires.source_location(); assertion.instructions.back().source_location_nonconst().set_comment( @@ -854,10 +851,8 @@ void code_contractst::apply_function_contract( replace(ensures); auto assumption = code_assumet(ensures); - ensures_pair = create_ensures_instruction( - assumption, - ensures.source_location(), - symbol_table.lookup_ref(target_function).mode); + ensures_pair = + create_ensures_instruction(assumption, ensures.source_location(), mode); // add all the history variable initialization instructions // to the goto program