Writing through pointer of differently sized type

[stilscher]

In the following example an integer is written through a char pointer. The following assert should fail, because only part of the integer value was overwritten. But currently the assert succeeds and this should be fixed.

https://github.com/goblint/analyzer/blob/59d7885d2dd62b451bc8db2a089d7a9550c3da2a/tests/regression/02-base/74-int-written-with-char-pointer.c#L1-L9

This example has been added as regression test on this branch.

[michael-schwarz]

I guess while //FAIL is ideal, we'd be happy with //UNKNOWN! too here.

[sim642]

Now this seems tricky because we'll somehow have to keep track of the casts and do something special. We already perform a cast from char to int at that write, but since the value is in bounds, int domains just keep the 65 because that's what a cast normally would do. Instead we somehow need to invalidate it.

[michael-schwarz]

Yes, I think we can not just ignore the type of the left-hand side anymore and just go based off the address.

[sim642]

This point came up again in a discussion with @vesalvojdani regarding all the things that addresses and their offsets, including #816. It seems that our addresses need to be typed.