Add some hacky atomic privatizations

docs/user-guide/annotating.md

@@ -66,3 +66,4 @@ Include `goblint.h` when using these.
 * `__goblint_assume_join(id)` is like `pthread_join(id, NULL)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
   Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
   _Misuse of this annotation can cause unsoundness._
+* `__goblint_globalize(ptr)` forces data pointed to by `ptr` to be treated as global by simulating it escaping the thread.

lib/goblint/runtime/include/goblint.h

@@ -3,6 +3,7 @@ void __goblint_assume(int exp);
 void __goblint_assert(int exp);
 
 void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
+void __goblint_globalize(void *ptr);
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);