diff --git a/share/libc/__fc_gcc_builtins.h b/share/libc/__fc_gcc_builtins.h index ea170e8855e06c55c970dfeb4ee1dacdc88e088b..15d03160d6d504e285709f98b92f77b37845b544 100644 --- a/share/libc/__fc_gcc_builtins.h +++ b/share/libc/__fc_gcc_builtins.h @@ -339,10 +339,10 @@ __UINT32_T __atomic_exchange_4(__UINT32_T* mem, __UINT32_T val, int model); */ __UINT64_T __atomic_exchange_8(__UINT64_T* mem, __UINT64_T val, int model); -/*@ requires validity: \valid(mem) && \valid_read(expected); - assigns *mem \from *mem, indirect: *expected, desired, +/*@ requires validity: \valid(mem) && \valid(expected); + assigns *mem \from *mem, desired, indirect: *expected, indirect: success_model, indirect: weak; - assigns *expected \from *expected, indirect: *mem, desired, + assigns *expected \from *expected, *mem, indirect: desired, indirect: failure_model, indirect: weak; assigns \result \from indirect: *mem, indirect: *expected; */ @@ -353,10 +353,10 @@ _Bool __atomic_compare_exchange_1(__UINT8_T* mem, int success_model, int failure_model); -/*@ requires validity: \valid(mem) && \valid_read(expected); - assigns *mem \from *mem, indirect: *expected, desired, +/*@ requires validity: \valid(mem) && \valid(expected); + assigns *mem \from *mem, desired, indirect: *expected, indirect: success_model, indirect: weak; - assigns *expected \from *expected, indirect: *mem, desired, + assigns *expected \from *expected, *mem, indirect: desired, indirect: failure_model, indirect: weak; assigns \result \from indirect: *mem, indirect: *expected; */ @@ -367,10 +367,10 @@ _Bool __atomic_compare_exchange_2(__UINT16_T* mem, int success_model, int failure_model); -/*@ requires validity: \valid(mem) && \valid_read(expected); - assigns *mem \from *mem, indirect: *expected, desired, +/*@ requires validity: \valid(mem) && \valid(expected); + assigns *mem \from *mem, desired, indirect: *expected, indirect: success_model, indirect: weak; - assigns *expected \from *expected, indirect: *mem, desired, + assigns *expected \from *expected, *mem, indirect: desired, indirect: failure_model, indirect: weak; assigns \result \from indirect: *mem, indirect: *expected; */ @@ -381,10 +381,10 @@ _Bool __atomic_compare_exchange_4(__UINT32_T* mem, int success_model, int failure_model); -/*@ requires validity: \valid(mem) && \valid_read(expected); - assigns *mem \from *mem, indirect: *expected, desired, +/*@ requires validity: \valid(mem) && \valid(expected); + assigns *mem \from *mem, desired, indirect: *expected, indirect: success_model, indirect: weak; - assigns *expected \from *expected, indirect: *mem, desired, + assigns *expected \from *expected, *mem, indirect: desired, indirect: failure_model, indirect: weak; assigns \result \from indirect: *mem, indirect: *expected; */ diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index 9e2fa656c310fb16960eeecf4a4f44200e2301af..5d807699a4a84d56b8f18925829cec6e122b72c6 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -9326,13 +9326,13 @@ unsigned int __atomic_exchange_4(unsigned int *mem, unsigned int val, unsigned long long __atomic_exchange_8(unsigned long long *mem, unsigned long long val, int model); -/*@ requires validity: \valid(mem) ∧ \valid_read(expected); +/*@ requires validity: \valid(mem) ∧ \valid(expected); assigns *mem, *expected, \result; assigns *mem - \from *mem, (indirect: *expected), desired, (indirect: success_model), + \from *mem, desired, (indirect: *expected), (indirect: success_model), (indirect: weak); assigns *expected - \from *expected, (indirect: *mem), desired, (indirect: failure_model), + \from *expected, *mem, (indirect: desired), (indirect: failure_model), (indirect: weak); assigns \result \from (indirect: *mem), (indirect: *expected); */ @@ -9341,13 +9341,13 @@ _Bool __atomic_compare_exchange_1(unsigned char *mem, unsigned char desired, _Bool weak, int success_model, int failure_model); -/*@ requires validity: \valid(mem) ∧ \valid_read(expected); +/*@ requires validity: \valid(mem) ∧ \valid(expected); assigns *mem, *expected, \result; assigns *mem - \from *mem, (indirect: *expected), desired, (indirect: success_model), + \from *mem, desired, (indirect: *expected), (indirect: success_model), (indirect: weak); assigns *expected - \from *expected, (indirect: *mem), desired, (indirect: failure_model), + \from *expected, *mem, (indirect: desired), (indirect: failure_model), (indirect: weak); assigns \result \from (indirect: *mem), (indirect: *expected); */ @@ -9356,13 +9356,13 @@ _Bool __atomic_compare_exchange_2(unsigned short *mem, unsigned short desired, _Bool weak, int success_model, int failure_model); -/*@ requires validity: \valid(mem) ∧ \valid_read(expected); +/*@ requires validity: \valid(mem) ∧ \valid(expected); assigns *mem, *expected, \result; assigns *mem - \from *mem, (indirect: *expected), desired, (indirect: success_model), + \from *mem, desired, (indirect: *expected), (indirect: success_model), (indirect: weak); assigns *expected - \from *expected, (indirect: *mem), desired, (indirect: failure_model), + \from *expected, *mem, (indirect: desired), (indirect: failure_model), (indirect: weak); assigns \result \from (indirect: *mem), (indirect: *expected); */ @@ -9370,13 +9370,13 @@ _Bool __atomic_compare_exchange_4(unsigned int *mem, unsigned int *expected, unsigned int desired, _Bool weak, int success_model, int failure_model); -/*@ requires validity: \valid(mem) ∧ \valid_read(expected); +/*@ requires validity: \valid(mem) ∧ \valid(expected); assigns *mem, *expected, \result; assigns *mem - \from *mem, (indirect: *expected), desired, (indirect: success_model), + \from *mem, desired, (indirect: *expected), (indirect: success_model), (indirect: weak); assigns *expected - \from *expected, (indirect: *mem), desired, (indirect: failure_model), + \from *expected, *mem, (indirect: desired), (indirect: failure_model), (indirect: weak); assigns \result \from (indirect: *mem), (indirect: *expected); */