Action items for compatibility-breaking release

[tautschnig]

We should consider dropping some cruft; doing so will break compatibility and thus must happen in one major release (and only one). Requires an increment of the goto binary format version.

• Drop symbol_typet and ns.follow (and use tag types instead)
• Restrict gotos to a single target
• Add a width to pointers (and remove all config references from solvers)
• Clean up the interface between cbmc and others (e.g., hw-cbmc, 2ls, ebmc, cegis)
• Replace owning raw pointers #835

[reuk]

#905?

[thk123]

The variable sensitivity domain stuff would be potentially good to get in. The main problem I see is the current interface is crude (binary on/off switches for the different modes) but with a more sophisticated system planned. I had therefore hoped to use a major version release to change this so we could get in what we have so far without feeling tied to it.

Depending on when the major version release is planned, either the PR should be reconfigured to not turn anything on until the better interface is developed, or the better interface should be got in before the release.

[tautschnig]

As much as I agree that variable sensitivity is interesting, I don't think it fits this particular bill of compatibility-breaking changes?

[thk123]

@tautschnig I was more thinking about the change in interface, but since the old style isn't going to get in for the maintenance release it won't break compatibility.

It would be nice to get the variable-sensitivity-domain with new interface in before the major release so that the old interface can go in and then be improved without having to worry about breaking compatibility.

[tautschnig]

Point taken, and I think my subject line has been to unclear: the items that I listed in the initial comment are about changes that break compatibility at goto-program level, i.e., goto binaries compiled with an earlier version would need to be recompiled. Such isn't the case with internal APIs.

[reuk]

I don't think #835 falls into this category. It just improves the memory safety of the program, it doesn't affect the goto binary format or any other user-facing interfaces.

[smowton]

De-overload (and perhaps entirely rethink) the CATCH GOTO instruction. This currently serves three purposes:

1. Push an exception handler
2. Pop an exception handler
3. Catch an exception
   We should split it into an instruction per action (a la DECL and DEAD), as the overloading (and misleading naming) invites mistakes from analysis authors.

[TGWDB]

Closing as an old feature request.