Pointers to struct members

[kroening]

Added test regression/cbmc/struct9 with 47170bd.

[smowton]

Problem is that in the double-deref (*(inner->GUARDp)) the first deref returns a byte-extract operation (since the inner aliases an outer), and then the second can't get a points-to set off of byte_extract and so returns invalid-object

[smowton]

Candidate fix in https://github.com/smowton/cbmc/tree/symex_deref_clean_struct_member, which in the case of a constant pointer offset returns an arbitrarily nested series of member-of and index-of expressions if possible, rather than resorting to byte-extract right away. That fixes the testcase posted:

Before, using the debug printing at symex_dereference.cpp:302:

**** inner!0@1
**** byte_extract_little_endian(outer!0@1, POINTER_OFFSET(inner!0@1), struct inner_struct { char *GUARDp; })

After:

**** inner!0@1
**** [email protected]

And with slight extension of the test program it can also generate expressions like:

**** inner!0@1
**** [email protected][1]

It doesn't however fix the general case where a real reinterpret case has happened, so byte-extract is perhaps the only reasonable way to express what has happened, and then further pointers are followed. At present invalid_object is offered up as a dangling nondet, hence the spurious counterexample, but I can't immediately think how to compile a program that derefs off a reinterpret except by generating a value set containing every object.

One other possible worrry: this of course introduces member_exprt where it hasn't been seen before. The rest of the code seemed to cope with these examples, but may be fragile in ways I haven't discovered yet.

[kroening]

May I have a pull request for this, please?

[smowton]

Submitted #283

[kroening]

Merged.