Description
CBMC version: 5.29.0
Operating system: Ubuntu20
Exact command line resulting in the issue: See below
What behaviour did you expect: n/a
What happened instead: n/a
The current implementation of the assigns clause considers the cross product of the writeable set (all the variable to which the program may write to) and the assigns clause set (all the variables included in the assigns clause). For example, let us consider the case where the writeable set contains A, B and the assigns clause set contains A', B'. When using the --enforce-contract flag with goto-instrument, every time a variable is defined, the generated goto program will assert the following: ( A == A' || A == B' ) && ( B == A' || B == B' ), while validating all elements in either set.
This is implemented here, where and element in the writeable set is represented by the called_target variable, while an element in the assigns clause set is represented by target.
The problem occurs when an invalid pointer is contained in the writeable set (which happens when an invalid pointer is passed as a parameter during a function call). In such a case, CBMC will try to validate the invalid pointer, which will cause an error.
A simple solution to this issue is proposed in #6077, however a better solution would involve checking the validity of writeable set elements during the creation of the goto program and handling invalid pointers as a special case regarding the generated assertion.