@@ -817,7 +817,7 @@ void code_contractst::apply_function_contract(
817817 }
818818 }
819819
820- const auto &mode = symbol_table. lookup_ref (target_function) .mode ;
820+ const auto &mode = function_symbol .mode ;
821821
822822 is_fresh_replacet is_fresh (*this , log, target_function);
823823 is_fresh.create_declarations ();
@@ -830,10 +830,7 @@ void code_contractst::apply_function_contract(
830830 replace (requires );
831831
832832 goto_programt assertion;
833- converter.goto_convert (
834- code_assertt (requires ),
835- assertion,
836- symbol_table.lookup_ref (target_function).mode );
833+ converter.goto_convert (code_assertt (requires ), assertion, mode);
837834 assertion.instructions .back ().source_location_nonconst () =
838835 requires .source_location ();
839836 assertion.instructions .back ().source_location_nonconst ().set_comment (
@@ -854,10 +851,8 @@ void code_contractst::apply_function_contract(
854851 replace (ensures);
855852
856853 auto assumption = code_assumet (ensures);
857- ensures_pair = create_ensures_instruction (
858- assumption,
859- ensures.source_location (),
860- symbol_table.lookup_ref (target_function).mode );
854+ ensures_pair =
855+ create_ensures_instruction (assumption, ensures.source_location (), mode);
861856
862857 // add all the history variable initialization instructions
863858 // to the goto program
0 commit comments