@@ -1262,9 +1262,10 @@ void statement_list_typecheckt::typecheck_called_function(
12621262 symbolt &tia_element)
12631263{
12641264 const symbol_exprt call_operand{to_symbol_expr (op_code.op0 ())};
1265- const symbolt &called_function {
1265+ const symbolt &called_function_sym {
12661266 symbol_table.lookup_ref (call_operand.get_identifier ())};
1267- const code_typet &called_type{to_code_type (called_function.type )};
1267+ const symbol_exprt called_function_expr{called_function_sym.symbol_expr ()};
1268+ const code_typet &called_type{to_code_type (called_function_sym.type )};
12681269
12691270 // Check if function name is followed by data block.
12701271 if (!can_cast_expr<equal_exprt>(op_code.op1 ()))
@@ -1288,11 +1289,22 @@ void statement_list_typecheckt::typecheck_called_function(
12881289
12891290 for (const code_typet::parametert ¶m : params)
12901291 {
1291- const exprt &arg{typecheck_function_call_arguments (assignments, param)};
1292+ const exprt &arg{
1293+ typecheck_function_call_arguments (assignments, param, tia_element)};
12921294 args.push_back (arg);
12931295 }
1294- const code_function_callt call{call_operand, args};
1295- tia_element.value .add_to_operands (call);
1296+
1297+ // Check the return value if present.
1298+ if (called_type.return_type ().is_nil ())
1299+ tia_element.value .add_to_operands (
1300+ code_function_callt{called_function_expr, args});
1301+ else
1302+ {
1303+ const exprt lhs{typecheck_return_value_assignment (
1304+ assignments, called_type.return_type (), tia_element)};
1305+ tia_element.value .add_to_operands (
1306+ code_function_callt{lhs, called_function_expr, args});
1307+ }
12961308}
12971309
12981310void statement_list_typecheckt::typecheck_called_function_block (
@@ -1309,23 +1321,60 @@ void statement_list_typecheckt::typecheck_called_function_block(
13091321
13101322exprt statement_list_typecheckt::typecheck_function_call_arguments (
13111323 const std::vector<equal_exprt> &assignments,
1312- const code_typet::parametert ¶m)
1324+ const code_typet::parametert ¶m,
1325+ const symbolt &tia_element)
1326+ {
1327+ const irep_idt ¶m_name = param.get_base_name ();
1328+ const typet ¶m_type = param.type ();
1329+ for (const equal_exprt &assignment : assignments)
1330+ {
1331+ const symbol_exprt &lhs{to_symbol_expr (assignment.lhs ())};
1332+ if (param_name == lhs.get_identifier ())
1333+ {
1334+ const symbol_exprt &rhs{to_symbol_expr (assignment.rhs ())};
1335+ const exprt assigned_variable{
1336+ typecheck_identifier (tia_element, rhs.get_identifier ())};
1337+ if (param_type == assigned_variable.type ())
1338+ return assigned_variable;
1339+ else
1340+ {
1341+ error () << " Types of parameter assignment do not match: "
1342+ << param.type ().id () << " != " << assigned_variable.type ().id ()
1343+ << eom;
1344+ throw TYPECHECK_ERROR;
1345+ }
1346+ }
1347+ }
1348+ error () << " No assignment found for function parameter "
1349+ << param.get_identifier () << eom;
1350+ throw TYPECHECK_ERROR;
1351+ }
1352+
1353+ exprt statement_list_typecheckt::typecheck_return_value_assignment (
1354+ const std::vector<equal_exprt> &assignments,
1355+ const typet &return_type,
1356+ const symbolt &tia_element)
13131357{
13141358 for (const equal_exprt &assignment : assignments)
13151359 {
13161360 const symbol_exprt &lhs{to_symbol_expr (assignment.lhs ())};
1317- if (param. get_identifier () == lhs.get_identifier ())
1361+ if (ID_statement_list_return_value_id == lhs.get_identifier ())
13181362 {
1319- if (param.type () == assignment.rhs ().type ())
1320- return assignment.rhs ();
1363+ const symbol_exprt &rhs{to_symbol_expr (assignment.rhs ())};
1364+ const exprt assigned_variable{
1365+ typecheck_identifier (tia_element, rhs.get_identifier ())};
1366+ if (return_type == assigned_variable.type ())
1367+ return assigned_variable;
13211368 else
13221369 {
1323- error () << " Types of parameter assignment do not match" << eom;
1370+ error () << " Types of return value assignment do not match: "
1371+ << return_type.id () << " != " << assigned_variable.type ().id ()
1372+ << eom;
13241373 throw TYPECHECK_ERROR;
13251374 }
13261375 }
13271376 }
1328- error () << " No assignment found for function parameter " << eom;
1377+ error () << " No assignment found for function return value " << eom;
13291378 throw TYPECHECK_ERROR;
13301379}
13311380
0 commit comments