Closed
Description
See #2356 for the context
A couple of initial suggestions to fix this:
- Use an explicit dummy target to be passed to make_goto()
- very simple
- helps avoiding wrongly incomplete initialisations
- allows checking that a converted goto program does not have incompletely initialised instructions
- Refactor goto_convert to perform single-step initialisation of goto instructions
- quite some work
- Keep NO_INSTRUCTION_TYPE and move if-then-else optimisation into a goto pass
- doable, but doesn't feel right
- makes invalid instructions explicit and the absence of incompletely initialised instructions can be easily checked
- ?
In any case also https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/goto_program.h#L495 should be removed.
Metadata
Metadata
Assignees
Labels
No labels