Avoid crash in linking conflict report by providing correct type for …

[andreast271]

…dereference expression

CBMC currently crashes with an invariant check failure if there is a conflict discovered during linking.
Test case:
file one.c:

int f(char *i) { return  *i; }

file two.c:

int f(int *i) { return  *i; }

cbmc command:

cbmc one.c two.c

cbmc message without this commit:

--- begin invariant violation report ---
Invariant check failed
File: ../util/std_expr.h:3041 function: dereference_exprt
Condition: op.type().id()==ID_pointer
Reason: Precondition

cbmc message with this commit:

file two.c line 1: 
reason for conflict at *#this: conflict on POD

char
signed int
error: conflicting function declarations f
old definition in module one file one.c line 1
signed int (char *i)
new definition in module two file two.c line 1
signed int (signed int *i$link1)
CONVERSION ERROR

[xbauch]

clang-format would prefer spaces around =.

[xbauch]

Also assigning it the subtype of the first expression seems a bit random. Conditioning it works as well:

      if(conflict_path.type().id() == ID_pointer)
        conflict_path = dereference_exprt(conflict_path);

[andreast271]

I agree with your comments / suggestions and have updated the commit accordingly. I also added a regression test case for this defect.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 578ba08).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108103779