The original pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i has following in the global invariant:

• whoop_loff_t -> Address {&(alloc@...)}
• &(alloc@...) -> Blob (Int)
  I don't understand how NULL isn't in the address set of whoop_loff_t anymore, because it is zero-initialized to that.

In both of the minimized versions I've committed here, the NULL remains there and the malloc also adds unknown pointer:

• whoop_loff_t -> Address {NULL, ?}
• &(alloc@...) -> Blob (Bot)
  The PR handles both cases but it'd be great to actually also test that but I'm very confused how the original behavior is even possible.

I don't understand how NULL isn't in the address set of whoop_loff_t anymore, because it is zero-initialized to that.

We don't have early globals on in sv-comp. And it only goes to multithreading after whoop_loff_t is set if I see it correctly? So this should be the expected behavior, no?

But the 29/20 I committed should then behave the same way, by starting out single threaded as well, but for whatever reason it doesn't.

But the 29/20 I committed should then behave the same way, by starting out single threaded as well, but for whatever reason it doesn't.

True, that is indeed strange! I'll take a look maybe, I can see what's going on.

If you add #include <stdlib.h> to your example program, it behaves just like the big example.

I think we can merge this now

If you add #include <stdlib.h> to your example program, it behaves just like the big example.

Of course, thanks for noticing that! I now remember fixing a similar thing in a previous regression test.

It's so annoying though that due to malloc being so specialized we don't have any warnings about it even lacking a declaration and that int is implicitly assumed to be the return type, which really screws with base analysis.