CONTRACTS: ignore __CPROVER_dead_object assignments

[remi-delmas-3000]

Fixes model-checking/kani#3796.

This change fixes spurious violations on GOTO models generated from MIR programs by Kani. MIR programs declare all stack-allocated place variables at the top of the function regardless of the original scope of the variable, and uses storageLive and storageDead events to delimit their dynamic lifetime. Kani uses a DECL to introduce place variables and uses dynamic assignments to __CPROVER_dead_object to encode storageLive and storageDead. DFCC instrumentation would only pick up storageDead events, not storageLive, resulting in spurious proof failures.

With this change we go back to relying only on DECL/DEAD for object liftetime tracking in DFCC and completely ignoring dynamic assignments to __CPROVER_dead_object. This means that contract instrumentation won't be able to detect bad accesses to objects for which the lifetime is managed via __CPROVER_dead_object anymore, for instance: dynamic stack-allocated objects created using alloca, or MIR place variables (that have their address taken) as encoded by Kani. As a consequence, --pointer-checks have to be enabled when analysing contracts-instrumented code.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 78.82%. Comparing base (b3e9976) to head (b6bae90).
Report is 24 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8554      +/-   ##
===========================================
- Coverage    78.89%   78.82%   -0.08%     
===========================================
  Files         1730     1730              
  Lines       198858   199101     +243     
  Branches     18345    18317      -28     
===========================================
+ Hits        156895   156939      +44     
- Misses       41963    42162     +199     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.