Discussion : structural invariants on goto-programs

[martin-cs]

At which points in the system, if any, is it acceptable to have a GOTO instruction whose target is the next instruction? For example:

if CONDITION goto next;
next : ...

I ask because remove_skip recognises (and removes) this case and many of the older abstract domains are written (implicitly) assuming it does not occur. So can/should we always assume that remove_skip has been run after any program transformations / input? Or should I update the domains so they are correct for this kind of program?

[peterschrammel]

domains are written (implicitly) assuming it does not occur

What is the performance optimisation enabled by this assumption?

[martin-cs]

It's not performance, it is correctness :

https://github.com/diffblue/cbmc/blob/develop/src/analyses/interval_domain.cpp#L84

[peterschrammel]

Why wouldn't it take a join at the GOTO target location (next)?

[peterschrammel]

The current implementation is simply unsound. Assumptions on the absence of certain control flow patterns are not a good idea and should be fixed.

[martin-cs]

OK, will fix all instances.