goto-analyzer fails with left-hand side typecasts

[tautschnig]

Running several experiments with goto-analyzer --vsd I saw a lot of reports of "invalid l-value" as reported by abstract_environmentt::assign. It turns out that all of these are caused by typecasts appearing on the left-hand side of assignments, which this method does not seem to account for. I tried to create a small reproducer, but actually ended up with a different problem. Take typecast.c as follows:

int main()
{
  int x;
  void *p = &x;
  *(int*)p = 42;
  __CPROVER_assert(x == 42, "must be 42");
}

Running goto-analyzer I get:

goto-analyzer --verify --vsd --vsd-pointers constants typecast.c
GOTO-ANALYZER version 5.79.0 (cbmc-5.79.0-15-gb5ff343b74-dirty) 64-bit x86_64 linux
Parsing typecast.c
Converting
Type-checking typecast
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Selecting abstract domain
Computing abstract states
--- begin invariant violation report ---
Invariant check failed
File: ../src/analyses/variable-sensitivity/write_stack.cpp:179 function: to_expression
Condition: !is_top_value()
Reason: Precondition
Backtrace:
[...]
--- end invariant violation report ---
Aborted (core dumped)