Add library functions for __atomic_{store,load}_n#884
Add library functions for __atomic_{store,load}_n#884michael-schwarz merged 3 commits intomasterfrom
__atomic_{store,load}_n#884Conversation
|
Why can't we just do actual assigning and reading of the pointed variable? EDIT: There are people who want to start using proper atomics in SV-COMP as well: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1331. |
We could, but tbh we need proper support at some point anyway, and this is only a stop-gap until then.
Yes, i also saw this. Though I am not sure what effect surrounding some accesses to a global with these while leaving others unaffected does. If such things actually are committed past the freeze deadline, I think it is fine to be cautious here for now, until we have proper support. |
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
CHANGES: Functionally equivalent to Goblint in SV-COMP 2023. * Add automatic configuration tuning (goblint/analyzer#772). * Add many library function specifications (goblint/analyzer#865, goblint/analyzer#868, goblint/analyzer#878, goblint/analyzer#884, goblint/analyzer#886). * Reorganize library stubs (goblint/analyzer#814, goblint/analyzer#845). * Add Trace Event Format output to timing (goblint/analyzer#844). * Optimize domains for address and path sets (goblint/analyzer#803, goblint/analyzer#809).
Calls occur in sv-comp. This is a stop-gap measure before we get proper support for C11 in Goblint. References #868
(These are indeed builtins despite their name not starting with
__builtin: https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html)