fix array->f typechecking

This commit is contained in:
Daniel Kroening 2018-04-24 12:36:58 +01:00
parent 714ccff121
commit a0ca0bab57
3 changed files with 36 additions and 12 deletions

View File

@ -0,0 +1,10 @@
struct some_struct
{
int some_field;
} array[10];
int main()
{
array[0].some_field=1;
array->some_field=1;
}

View File

@ -0,0 +1,8 @@
CORE
main.c
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$

View File

@ -1431,25 +1431,31 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)
const typet &final_op0_type=follow(expr.op0().type());
if(final_op0_type.id()!=ID_pointer &&
final_op0_type.id()!=ID_array)
if(final_op0_type.id()==ID_array)
{
// a->f is the same as a[0].f
exprt zero=from_integer(0, index_type());
index_exprt index_expr(expr.op0(), zero, final_op0_type.subtype());
index_expr.set(ID_C_lvalue, true);
expr.op0().swap(index_expr);
}
else if(final_op0_type.id()==ID_pointer)
{
// turn x->y into (*x).y
dereference_exprt deref_expr(expr.op0());
deref_expr.add_source_location()=expr.source_location();
typecheck_expr_dereference(deref_expr);
expr.op0().swap(deref_expr);
}
else
{
err_location(expr);
error() << "ptrmember operator requires pointer type "
error() << "ptrmember operator requires pointer or array type "
"on left hand side, but got `"
<< to_string(expr.op0().type()) << "'" << eom;
throw 0;
}
// turn x->y into (*x).y
dereference_exprt deref(expr.op0());
deref.add_source_location()=expr.source_location();
typecheck_expr_dereference(deref);
expr.op0().swap(deref);
expr.id(ID_member);
typecheck_expr_member(expr);
}