Description
A recent change in CBMC made it an invariant of pointer_typet
that pointers have a width field. On my development branch, I've added assert(!type.get(ID_width).empty());
to to_pointer_type
so that I find all malformedpointer_typet
s.
This is fine, and I've found several places where pointer_typet
s are constructed incorrectly. The problem is that when the cross-compiled object files in the arch_flags
regression tests are loaded, they contain malformed pointers, which cause the new assertions to fail.
The instructions in the test.desc files are not especially clear: it's not obvious how to set up an ARM cross-compiler.
More detailed instructions should be added to the test.desc files, and new object files should be submitted, generated with a more recent version of goto-cc
.
Pinging @karkhaz and @tautschnig as they may be familiar with this process.