Skip to content

Commit bb80cdc

Browse files
committed
Transparent unions require argument conversion, do this for all union types
Also improves the readabilit of error output when argument conversion is denied
1 parent e35f6b7 commit bb80cdc

File tree

1 file changed

+16
-8
lines changed

1 file changed

+16
-8
lines changed

src/goto-symex/symex_function_call.cpp

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include <iostream>
10+
#include <sstream>
1011
#include <cassert>
1112

1213
#include <util/expr_util.h>
@@ -121,23 +122,30 @@ void goto_symext::parameter_assignments(
121122
f_parameter_type.id()==ID_unsignedbv ||
122123
f_parameter_type.id()==ID_c_enum_tag ||
123124
f_parameter_type.id()==ID_bool ||
124-
f_parameter_type.id()==ID_pointer) &&
125+
f_parameter_type.id()==ID_pointer ||
126+
f_parameter_type.id()==ID_union) &&
125127
(f_rhs_type.id()==ID_signedbv ||
126128
f_rhs_type.id()==ID_unsignedbv ||
127129
f_rhs_type.id()==ID_c_bit_field ||
128130
f_rhs_type.id()==ID_c_enum_tag ||
129131
f_rhs_type.id()==ID_bool ||
130-
f_rhs_type.id()==ID_pointer))
132+
f_rhs_type.id()==ID_pointer ||
133+
f_rhs_type.id()==ID_union))
131134
{
132-
rhs.make_typecast(parameter_type);
135+
rhs=
136+
byte_extract_exprt(
137+
byte_extract_id(),
138+
rhs,
139+
gen_zero(index_type()),
140+
parameter_type);
133141
}
134142
else
135143
{
136-
std::string error="function call: parameter \""+
137-
id2string(identifier)+"\" type mismatch: got "+
138-
rhs.type().to_string()+", expected "+
139-
parameter_type.to_string();
140-
throw error;
144+
std::ostringstream error;
145+
error << "function call: parameter \"" << identifier
146+
<< "\" type mismatch: got " << rhs.type().pretty()
147+
<< ", expected " << parameter_type.pretty();
148+
throw error.str();
141149
}
142150
}
143151

0 commit comments

Comments
 (0)