OC backend reports Safe on a reachable NULL dereference when the alias graph is non-empty

[leventeBajczi]

The OC backend reports Safe for a program with a reachable NULL dereference, whenever the
alias analysis produces a non-empty points-to graph. CEGAR gets the same program right, so the
error locations exist — OC's event graph does not see them.

Found while checking the one missed bug in the 8.0.x regression sweep (#564):
goblint-regression/09-regions_09-arraylist-deref [valid-memsafety], expected false, reported
true by MULTITHREAD_OC_BASIC_GENERIC3.

Reproducer

extern int __VERIFIER_nondet_int();
extern void abort(void);
extern void *malloc(unsigned int);
void assume_abort_if_not(int cond) { if(!cond) {abort();} }
#include <pthread.h>
struct s { int datum; struct s *next; };
struct s *new(int x) {
  struct s *p = malloc(sizeof(struct s));
  p->datum = x; p->next = (void *)0;
  return p;
}
void list_add(struct s *node, struct s *list) {
  struct s *temp = list->next;
  list->next = node;
  node->next = temp;
}
struct s *slot[10];
void *t_fun(void *arg) {
  int i = __VERIFIER_nondet_int();
  assume_abort_if_not(0 <= i && i < 10);
  struct s *q = slot[i]->next;   // NULL whenever i != j
  return (void *)0;
}
int main() {
  int j = __VERIFIER_nondet_int();
  assume_abort_if_not(0 <= j && j < 10);
  pthread_t t1;
  slot[j] = new(1);
  list_add(new(2), slot[j]);
  pthread_create(&t1, (void *)0, t_fun, (void *)0);
  pthread_join(t1, (void *)0);
  return 0;
}

slot[] is NULL-initialised; main fills only slot[j], and the thread dereferences slot[i]
for an independent nondeterministic i, so i != j is a NULL dereference.

--backend OC     -> (SafetyResult Safe)     <-- wrong
--backend CEGAR  -> (SafetyResult Unsafe)   <-- correct

What triggers it

Removing list_add — the only function that writes through pointer parameters — makes the alias
graph empty and OC then answers correctly:

variant	alias graph	OC verdict
reproducer as above	1 -> [1]	Safe (wrong)
same, without list_add	0 -> []	Unsafe (correct)
NULL deref in a thread, no aliasing	0 -> []	Unsafe (correct)
NULL deref in main, no aliasing	0 -> []	Unsafe (correct)

The original task shows the same pattern (Alias graph size: 4 -> [4, 4, 1, 1], verdict Safe), and
reductions of it that keep list_add stay wrong regardless of whether the mutex, the printf or
main's own dereference are removed.

Mechanism

XcfaOcChecker.check returns Safe outright when the event graph carries no violations:

if (eg.violations.isEmpty()) {
  return SafetyResult.safe(EmptyProof.getInstance())
}

XcfaToEventGraph only records a violation for a location with loc.error set, so the
memory-safety check locations are absent from the graph OC builds. OC runs its own frontend in a
subprocess with a different pass configuration (lbeLevel=NO_LBE, inProcess=false) than the
CEGAR configs, which is the likely place the instrumentation diverges.

An empty violation set is indistinguishable from "the property cannot be violated" here, so the
failure is silent. Returning Unknown when a MEMSAFETY property yields no violations would at least
make it non-silent, but the real fix is for the deref checks to reach the event graph.

Scope

Not a regression against 7.3.0 — that version returned unknown for this task. It is a wrong
answer the 8.x line now produces, costing −32 on the task above; how many other OC+memsafety tasks
are silently affected is not yet measured.