replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

assignment to union 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3360 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-01-06 23:07:23 +00:00
parent 6ab29dd1ee
commit cd35e8a110
1 changed files with 29 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
src/path-symex/path_symex.cpp
View File

@ -150,6 +150,10 @@ bool path_symext::propagate(const exprt &src)
{ {
return propagate(to_array_of_expr(src).what()); return propagate(to_array_of_expr(src).what());
} }
else if(src.id()==ID_union)
{
return propagate(to_union_expr(src).op());
}
else else
{ {
return false; return false;
@ -496,16 +500,34 @@ void path_symext::assign_rec(
#endif #endif
const member_exprt &lhs_member_expr=to_member_expr(lhs); const member_exprt &lhs_member_expr=to_member_expr(lhs);
// add component name to the suffix
const std::string new_suffix=
"."+id2string(lhs_member_expr.get_component_name())+suffix;
const exprt &struct_op=lhs_member_expr.struct_op(); const exprt &struct_op=lhs_member_expr.struct_op();
//typet lhs_type=state.var_map.ns.follow(lhs_suffix_type); const typet &compound_type=
state.var_map.ns.follow(struct_op.type());
if(compound_type.id()==ID_struct)
{
// add component name to the suffix
const std::string new_suffix=
"."+id2string(lhs_member_expr.get_component_name())+suffix;
assign_rec(state, guard, struct_op, rhs, new_suffix, full_lhs); //typet lhs_type=state.var_map.ns.follow(lhs_suffix_type);
assign_rec(state, guard, struct_op, rhs, new_suffix, full_lhs);
}
else if(compound_type.id()==ID_union)
{
// adjust rhs
union_exprt new_rhs;
new_rhs.type()=struct_op.type();
new_rhs.set_component_name(lhs_member_expr.get_component_name());
new_rhs.op()=rhs;
assign_rec(state, guard, struct_op, new_rhs, suffix, full_lhs);
}
else
throw "assign_rec: member expects struct or union type";
} }
else if(lhs.id()==ID_index) else if(lhs.id()==ID_index)
{ {