@@ -817,7 +817,7 @@ void code_contractst::apply_function_contract(
817
817
}
818
818
}
819
819
820
- const auto &mode = symbol_table. lookup_ref (target_function) .mode ;
820
+ const auto &mode = function_symbol .mode ;
821
821
822
822
is_fresh_replacet is_fresh (*this , log , target_function);
823
823
is_fresh.create_declarations ();
@@ -830,10 +830,7 @@ void code_contractst::apply_function_contract(
830
830
replace (requires);
831
831
832
832
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);
837
834
assertion.instructions .back ().source_location_nonconst () =
838
835
requires.source_location ();
839
836
assertion.instructions .back ().source_location_nonconst ().set_comment (
@@ -854,10 +851,8 @@ void code_contractst::apply_function_contract(
854
851
replace (ensures);
855
852
856
853
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);
861
856
862
857
// add all the history variable initialization instructions
863
858
// to the goto program
0 commit comments