Fix 28-race_reach TODOs

[sim642]

Races-as-reachability tests in 28-race_reach have TODO assertions which we currently cannot prove:

• [ ] 22-deref_read_racefree.c

  Global q may still point to initial NULL in addition to &data in main (not privatized). This is probably why Goblint cannot prove the assertion despite having data = 0 in global invariant.

• [ ] 70-funloop_racefree.c, 73-funloop_hard_racefree.c

  cache[?].refs not privatized in access with symbolic lock for cache[?].refs_mutex (p-lock:*.refs_mutex).

• [ ] 74-tricky_address1_racefree.c, 75-tricky_address2_racefree.c, 76-tricky_address3_racefree.c

  a[?].datum not privatized in access with symbolic lock for a[?].mutex (p-lock:*.mutex).

• [ ] 79-equ_racefree.c

  A.datum not privatized in access with symbolic lock for A.mutex (p-lock:*.mutex).

• [ ] 85-list2_racefree.c

  The non-determinism in t1_fun causes regions A and B to collapse in insert because RegMap has {A, B} for list, t and node. Making region analysis path-sensitive at least prevents the regions from collapsing.

• [ ] 87-lists_racefree.c

  Considering the locking scheme, this needs --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --enable exp.region-offsets in PARAM as well? Then buckets[?].datum not privatized in access with symbolic lock for mutexes[?] (i-lock:mutexes[def_exc:*]).

• [ ] 91-arrayloop2_racefree.c, 93-evilcollapse_racefree.c

  ?.datum not privatized in access with symbolic lock for c.slots_mutex[?] (i-lock:c.slots_mutex[def_exc:*]). Offsets c.slot[?].datum (memory location) and c.slot[?].next.datum (region) aren't even valid because datum cannot be reached from c through normal field accesses. This might make its privatization harder?