Following #1469, it looks like a viable solution for supporting alternative backends is to comment the produced Irep to allow for a different interpretation than CBMC.

At the moment, the choice has been made to add a "#comment" named sub to the Irep itself. For example, in the case of Deinit, the assignment statement corresponding to lvalue = Nondet has this name sub. However, comments are usually attached to the location member of the irep.

The reason the comment was attached to the irep itself is simplicity: Stmt::to_irep's job is to call Location::to_irep and StmtBody::to_irep, and then aggregating the results. Therefore, if we want StmtBody::to_irep to produce a comment that is then added to the Location's irep, we need StmtBody::to_irep to return two things, instead of one. That would mean refactoring the function to change every return value, for 1 use case.

This issue aims at discussing the best and cleanest way to handle AST comments in the future.