diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2020-10-19 00:37:55 +0200 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2020-10-19 20:46:08 +0200 |
| commit | 7f33e55f0b4b011543a7e529331576429270b738 (patch) | |
| tree | b0acd008b6a74102e88afce1f8b755fb36065992 /validation | |
| parent | efa1869dd78b2a4f7cef19e52a586a0b2bc2b0fb (diff) | |
| parent | 9e8c9fc89934bfb88e93a2e8f87a7b12b2586e44 (diff) | |
| download | sparse-dev-7f33e55f0b4b011543a7e529331576429270b738.tar.gz | |
Merge branch 'builtin-atomic' into next
* fix and complete the evaluation of atomic builtins
Diffstat (limited to 'validation')
| -rw-r--r-- | validation/builtin-atomic-clear.c | 15 | ||||
| -rw-r--r-- | validation/builtin-sync-fetch.c | 24 |
2 files changed, 39 insertions, 0 deletions
diff --git a/validation/builtin-atomic-clear.c b/validation/builtin-atomic-clear.c new file mode 100644 index 00000000..ef430c64 --- /dev/null +++ b/validation/builtin-atomic-clear.c @@ -0,0 +1,15 @@ +void foo(void *ptr, _Bool *bptr, volatile void *vptr, volatile _Bool *vbptr, int mo) +{ + __atomic_clear(ptr, mo); + __atomic_clear(bptr, mo); + __atomic_clear(vptr, mo); + __atomic_clear(vbptr, mo); +} + +/* + * check-name: builtin-atomic-clear + * + * check-error-start +builtin-atomic-clear.c:1:6: warning: symbol 'foo' was not declared. Should it be static? + * check-error-end + */ diff --git a/validation/builtin-sync-fetch.c b/validation/builtin-sync-fetch.c new file mode 100644 index 00000000..45139a3c --- /dev/null +++ b/validation/builtin-sync-fetch.c @@ -0,0 +1,24 @@ +static int ok_int(int *ptr, int val) +{ + return __sync_add_and_fetch(ptr, val); +} + +static long* ok_ptr(long **ptr, long *val) +{ + return __sync_add_and_fetch(ptr, val); +} + +static void chk_ret_ok(long *ptr, long val) +{ + _Static_assert([typeof(__sync_add_and_fetch(ptr, val))] == [long], ""); +} + +static int chk_val(int *ptr, long val) +{ + // OK: val is converted to an int + return __sync_add_and_fetch(ptr, val); +} + +/* + * check-name: builtin-sync-fetch + */ |