From 93ce65d582e47e9e02840be9f9a573925d84dad5 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 19 Nov 2021 15:37:14 +0100 Subject: [PATCH] [libc] more precise postconditions for atomic gcc builtins --- share/libc/__fc_gcc_builtins.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/share/libc/__fc_gcc_builtins.h b/share/libc/__fc_gcc_builtins.h index 12410f1e896..1335394831f 100644 --- a/share/libc/__fc_gcc_builtins.h +++ b/share/libc/__fc_gcc_builtins.h @@ -263,48 +263,56 @@ int __builtin_popcountll (unsigned long long x); /*@ requires validity: \valid_read(mem); assigns \result \from *mem, indirect:model; + ensures load_value: \result == *mem; */ __UINT8_T __atomic_load_1(__UINT8_T* mem, int model); /*@ requires validity: \valid_read(mem); assigns \result \from *mem, indirect: model; + ensures load_value: \result == *mem; */ __UINT16_T __atomic_load_2(__UINT16_T* mem, int model); /*@ requires validity: \valid_read(mem); assigns \result \from *mem, indirect:model; + ensures load_value: \result == *mem; */ __UINT32_T __atomic_load_4(__UINT32_T* mem, int model); /*@ requires validity: \valid_read(mem); assigns \result \from *mem, indirect:model; + ensures load_value: \result == *mem; */ __UINT64_T __atomic_load_8(__UINT64_T* mem, int model); /*@ requires validity: \valid(mem); assigns *mem \from val, indirect: model; + ensures store_value: *mem == val; */ void __atomic_store_1(__UINT8_T* mem, __UINT8_T val, int model); /*@ requires validity: \valid(mem); assigns *mem \from val, indirect: model; + ensures store_value: *mem == val; */ void __atomic_store_2(__UINT16_T* mem, __UINT16_T val, int model); /*@ requires validity: \valid(mem); assigns *mem \from val, indirect: model; + ensures store_value: *mem == val; */ void __atomic_store_4(__UINT32_T* mem, __UINT32_T val, int model); /*@ requires validity: \valid(mem); assigns *mem \from val, indirect: model; + ensures store_value: *mem == val; */ void __atomic_store_8(__UINT64_T* mem, __UINT64_T val, int model); -- GitLab