2 full-slicer crashes

[polgreen]

To recreate both of these issues you will need this Xen binary:
https://drive.google.com/file/d/1Vco57D_iMhQ6N1EXqLTmF1wC9WiSN3mZ/view?usp=sharing
And this branch of cbmc:
https://github.com/diffblue/cbmc/tree/remove_asm_fix
(if you use develop, a different invariant is violated)

Issue 1

To recreate:

goto-instrument --remove-function-pointers xen-syms.binary test.binary
goto-instrument --full-slice test.binary output.binary

This triggers either this invariant: https://github.com/diffblue/cbmc/blob/develop/src/pointer-analysis/value_set_fi.cpp#L1282, or this invariant: https://github.com/diffblue/cbmc/blob/develop/src/pointer-analysis/value_set_fi.cpp#L412

The problem seems to be dereferencing pointers that are NULL. A temporary fix is to introduce this check before these invariants if(expr.op0().id() == ID_null_object) return;.

Issue 2

I've no idea why removing the function pointers in a separate step produces a different result to this, but it does. To recreate:

goto-instrument --full-slice xen-syms.binary output.binary

This terminates with "identifier not found", which comes from value_set_domain_fit::transform being called on something with no identifier and no LOC on the rhs.

[kroening]

The first issue is addressed in PR #2736

[kroening]

The second in PR #2741.

[polgreen]

I am running on CBMC with both of the above PR's cherry picked on and I get the following invariant violation from running `goto-instrument --full-slice A.binary B.binary'

--- begin invariant violation report ---
Invariant check failed
File: mp_arith.cpp:197 function: integer2size_t
Condition: n>=0 && n<=std::numeric_limits<std::size_t>::max()
Reason: Precondition

A.binary is here
https://s3.amazonaws.com/cbmc-public-bucket/A.binary

[polgreen]

With a different binary, I get the following invariant from running goto-instrument --full-slice C.binary D.binary

--- begin invariant violation report ---
Invariant check failed
File: value_set_fi.cpp:1285 function: assign_rec
Condition: type.id()==ID_array || type.id()==ID_incomplete_array || type.id()=="#REF#"
Reason: operand 0 of index expression must be an array

C.binary here:
https://s3.amazonaws.com/cbmc-public-bucket/C.binary

[kroening]

The problem with A.binary is fixed with PR #2822.