@@ -55,22 +55,29 @@ void cpp_typecheckt::typecheck_code(codet &code)
5555 // as an extension, we support indexed access into signed/unsigned
5656 // bitvectors, typically used with __CPROVER::(un)signedbv<N>
5757 exprt &expr = code.op0 ();
58- if (
59- expr.operands ().size () == 2 && expr.op0 ().id () == ID_index &&
60- expr.op0 ().operands ().size () == 2 )
58+
59+ if (expr.operands ().size () == 2 )
6160 {
62- exprt array = expr.op0 ().op0 ();
63- typecheck_expr (array);
61+ auto &binary_expr = to_binary_expr (expr);
6462
65- if (array. type ().id () == ID_signedbv || array. type (). id () == ID_unsignedbv )
63+ if (binary_expr. op0 ().id () == ID_index )
6664 {
67- shl_exprt shl{from_integer (1 , array.type ()), expr.op0 ().op1 ()};
68- exprt rhs =
69- if_exprt{equal_exprt{expr.op1 (), from_integer (0 , array.type ())},
70- bitand_exprt{array, bitnot_exprt{shl}},
71- bitor_exprt{array, shl}};
72- expr.op0 () = expr.op0 ().op0 ();
73- expr.op1 () = rhs;
65+ exprt array = to_index_expr (binary_expr.op0 ()).array ();
66+ typecheck_expr (array);
67+
68+ if (
69+ array.type ().id () == ID_signedbv ||
70+ array.type ().id () == ID_unsignedbv)
71+ {
72+ shl_exprt shl{from_integer (1 , array.type ()),
73+ to_index_expr (binary_expr.op0 ()).index ()};
74+ exprt rhs = if_exprt{
75+ equal_exprt{binary_expr.op1 (), from_integer (0 , array.type ())},
76+ bitand_exprt{array, bitnot_exprt{shl}},
77+ bitor_exprt{array, shl}};
78+ binary_expr.op0 () = to_index_expr (binary_expr.op0 ()).array ();
79+ binary_expr.op1 () = rhs;
80+ }
7481 }
7582 }
7683
@@ -191,8 +198,7 @@ void cpp_typecheckt::typecheck_switch(codet &code)
191198 assert (decl.operands ().size ()==1 );
192199
193200 // replace declaration by its symbol
194- assert (decl.op0 ().op0 ().id ()==ID_symbol);
195- value = decl.op0 ().op0 ();
201+ value = to_code_decl (to_code (to_unary_expr (decl).op ())).symbol ();
196202
197203 c_typecheck_baset::typecheck_switch (code);
198204
@@ -287,11 +293,11 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
287293 // a reference member
288294 if (
289295 symbol_expr.id () == ID_dereference &&
290- symbol_expr. op0 ().id () == ID_member &&
296+ to_dereference_expr ( symbol_expr). pointer ().id () == ID_member &&
291297 symbol_expr.get_bool (ID_C_implicit))
292298 {
293299 // treat references as normal pointers
294- exprt tmp = symbol_expr. op0 ();
300+ exprt tmp = to_dereference_expr ( symbol_expr). pointer ();
295301 symbol_expr.swap (tmp);
296302 }
297303
@@ -316,18 +322,20 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
316322
317323 if (
318324 symbol_expr.id () == ID_dereference &&
319- symbol_expr. op0 ().id () == ID_member &&
325+ to_dereference_expr ( symbol_expr). pointer ().id () == ID_member &&
320326 symbol_expr.get_bool (ID_C_implicit))
321327 {
322328 // treat references as normal pointers
323- exprt tmp = symbol_expr. op0 ();
329+ exprt tmp = to_dereference_expr ( symbol_expr). pointer ();
324330 symbol_expr.swap (tmp);
325331 }
326332 }
327333
328- if (symbol_expr.id () == ID_member &&
329- symbol_expr.op0 ().id () == ID_dereference &&
330- symbol_expr.op0 ().op0 () == cpp_scopes.current_scope ().this_expr )
334+ if (
335+ symbol_expr.id () == ID_member &&
336+ to_member_expr (symbol_expr).op ().id () == ID_dereference &&
337+ to_dereference_expr (to_member_expr (symbol_expr).op ()).pointer () ==
338+ cpp_scopes.current_scope ().this_expr )
331339 {
332340 if (is_reference (symbol_expr.type ()))
333341 {
0 commit comments