Verilog: comments and redundant synth_expr call

[kroening]

This adds comments to the arguments of assignment_rec, which indicate that a redundant call to synth_expr can be removed.

[tautschnig]

Wouldn't it be better to introduce synth_exprt and synth_lhs_exprt (both deriving from exprt) to replace good intentions by a compiler-provided mechanism?

[kroening]

Wouldn't it be better to introduce synth_exprt and synth_lhs_exprt (both deriving from exprt) to replace good intentions by a compiler-provided mechanism?

You'd need predicates on types (you'd want a synthesised symbol_exprt, synthesised index expression etc).

[tautschnig]

You'd need predicates on types (you'd want a synthesised symbol_exprt, synthesised index expression etc).

You could still wrap a symbol expression/index expression/etc. in that predicate? Just like the approach you introduced in the expression simplifier (to track changed/unchanged)?

[tautschnig]

Approving so as not the block all the work building on top of this, but I'd still prefer a solution not based on comments.

[kroening]

Approving so as not the block all the work building on top of this, but I'd still prefer a solution not based on comments.

Agreed; the synthesis part should likely get a redesign.