@@ -1095,6 +1095,40 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
1095
1095
const std::string callee_ident = as_string (callee_id);
1096
1096
const code_typet &fn_type =
1097
1097
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
+ }
1098
1132
std::vector<irep_idt> overridden_functions;
1099
1133
get_virtual_function_callees (
1100
1134
callee_expr,
@@ -1292,41 +1326,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
1292
1326
}
1293
1327
}
1294
1328
}
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))
1330
1330
{
1331
1331
log ->debug ()
1332
1332
<< " *** WARNING: Neither matching rule nor summary was found for "
0 commit comments