@@ -1095,6 +1095,40 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
10951095 const std::string callee_ident = as_string (callee_id);
10961096 const code_typet &fn_type =
10971097 program->get_functions ().function_map .at (callee_id).type ;
1098+ if (database.contains (callee_id))
1099+ {
1100+ std::shared_ptr<taint_summaryt> summary = database.at (callee_id);
1101+
1102+ transition_properties[Iit].push_back (
1103+ {taint_transition_property_typet::APPLICATION_OF_SUMMARY,
1104+ taint_rule_idt{},
1105+ " " });
1106+
1107+ statistics->on_taint_analysis_use_callee_summary (
1108+ summary, callee_ident);
1109+
1110+ numbered_lvalue_to_taint_mapt substituted_summary;
1111+ std::map<taint_variablet, taint_sett> symbols_substitution;
1112+ taint_build_symbols_substitution (
1113+ symbols_substitution,
1114+ a,
1115+ summary,
1116+ fn_call,
1117+ fn_type,
1118+ lvsa,
1119+ Iit,
1120+ caller_ident);
1121+ taint_build_substituted_summary (
1122+ substituted_summary,
1123+ summary->get_output (),
1124+ symbols_substitution,
1125+ caller_ident,
1126+ fn_call,
1127+ fn_type,
1128+ Iit,
1129+ lvsa);
1130+ result = assign (result, substituted_summary);
1131+ }
10981132 std::vector<irep_idt> overridden_functions;
10991133 get_virtual_function_callees (
11001134 callee_expr,
@@ -1292,41 +1326,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
12921326 }
12931327 }
12941328 }
1295- if (!rule_found && database.contains (callee_id))
1296- {
1297- std::shared_ptr<taint_summaryt> summary = database.at (callee_id);
1298-
1299- transition_properties[Iit].push_back (
1300- {taint_transition_property_typet::APPLICATION_OF_SUMMARY,
1301- taint_rule_idt{},
1302- " " });
1303-
1304- statistics->on_taint_analysis_use_callee_summary (
1305- summary, callee_ident);
1306-
1307- numbered_lvalue_to_taint_mapt substituted_summary;
1308- std::map<taint_variablet, taint_sett> symbols_substitution;
1309- taint_build_symbols_substitution (
1310- symbols_substitution,
1311- a,
1312- summary,
1313- fn_call,
1314- fn_type,
1315- lvsa,
1316- Iit,
1317- caller_ident);
1318- taint_build_substituted_summary (
1319- substituted_summary,
1320- summary->get_output (),
1321- symbols_substitution,
1322- caller_ident,
1323- fn_call,
1324- fn_type,
1325- Iit,
1326- lvsa);
1327- result = assign (result, substituted_summary);
1328- }
1329- else if (!rule_found)
1329+ if (!rule_found && !database.contains (callee_id))
13301330 {
13311331 log->debug ()
13321332 << " *** WARNING: Neither matching rule nor summary was found for "
0 commit comments