Karoliine Holter

https://github.com/goblint/analyzer/blob/5cd8650a2872341152f48a7d1cd20ac9fa0de994/src/cdomain/value/cdomains/valueDomain.ml#L502-L507 By tracing a smaller example extracted from `sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.i`, it seems that this issue is caused by this todo about handling casts between different sizes.

Debugging revealed that this is caused by the line: https://github.com/goblint/analyzer/blob/a0309d10f311222c6f3757127dfe1c0bfd52e551/src/analyses/base.ml#L287 1. `evalbinop_mustbeequal` calls `evalbinop_base` with a1: `{&str}` a2: `0` t1: `struct a *` t2: `int` 2. In `evalbinop_base`, `Addr.to_mval addr`...

Decisions from GobCon on 09.07: > What should happen when we write to a pointer that is either known or NullPtr? > * a) Should we keep the NullPtr and...

The [`mallocFresh` extracted from `region`](https://github.com/goblint/analyzer/tree/region-mallocfresh) shows a race between `struct s *r = g->next;` (read) and `g->next = q;` (write) but there is no race on the access of `p->next...

The tests pass when we replace it with: ```c if AD.is_empty lval then st else AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ()) ``` 1....

I was satisfied with the fix that I proposed here, but I think @sim642 was unsure if it was the right fix for this. @michael-schwarz, could you please take a...

@sim642 made a run with `--set ana.malloc.unique_address_count 1` on sv-benchmarks with no-overflow property. This gives 31 new correct results with a 60s timeout. However, it costs us a 14% slowdown...

The SV-COMP task `termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c` can be used as a test case when addressing this issue.

This causes a spurious `NullPointerDereference` in SV-COMP task `ldv-regression/nested_structure-2.i`. The program location for the warning: `[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (./ldv-regression/nested_structure-2.i:17:3-17:9)` is the `return` statement of...

The following still needs fixing: `[Warning][Witness] invariant unconfirmed: applet_opts == (char const *)"lwmcL" (../../sv-benchmarks/c/busybox-1.22.0/wc-2.i:2458:3)` It's from one of the 7/31 tasks from `SoftwareSystems-Other-ReachSafety` that we are able to verify, and...