Atomic operations support

[sim642]

There are multiple families of atomic operations:

• GCC __sync builtins: https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html.
• C11: https://en.cppreference.com/w/c/thread#Atomic_operations.

There are three aspects in which to improve precision:

• Not emitting race warnings for accesses by atomic functions. Do not produce racewarnings for types annotated as _Atomic #521 only applies to variables with C11 _Atomic, but not the __sync builtins used by various benchmarks. There should probably still be access events for them, but with an additional atomicity flag to exclude them from racing.
• Performing the respective operations on values as opposed to invalidating (suggested in Add missing library functions for Concrat benchmarks #996 (comment)).
• Treating limited statements on atomic variables as atomic altogether:

  Built-in increment and decrement operators and compound assignment are read-modify-write atomic operations with total sequentially consistent ordering (as if using memory_order_seq_cst).

[sim642]

There's now progress in sv-benchmarks to replace some __VERIFIER_atomics with C11/GCC atomics:

• https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1548,
• https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1549,
• https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1554,
• https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1556,
• https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1557.

I haven't checked how much it affects our results, but we might have to also adapt a bit to not lose our edge for superficial reasons.