Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
7507c9f0
Commit
7507c9f0
authored
3 years ago
by
Virgile Prevosto
Browse files
Options
Downloads
Patches
Plain Diff
[atomic] use unsigned arguments
parent
292f40c5
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
share/libc/__fc_gcc_builtins.h
+72
-72
72 additions, 72 deletions
share/libc/__fc_gcc_builtins.h
with
72 additions
and
72 deletions
share/libc/__fc_gcc_builtins.h
+
72
−
72
View file @
7507c9f0
...
@@ -264,73 +264,73 @@ int __builtin_popcountll (unsigned long long x);
...
@@ -264,73 +264,73 @@ int __builtin_popcountll (unsigned long long x);
requires validity: \valid_read(mem);
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT8_T
__atomic_load_1
(
__INT8_T
*
mem
,
int
model
);
__
U
INT8_T
__atomic_load_1
(
__
U
INT8_T
*
mem
,
int
model
);
/*@
/*@
requires validity: \valid_read(mem);
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect: model;
assigns \result \from *mem, indirect: model;
*/
*/
__INT16_T
__atomic_load_2
(
__INT16_T
*
mem
,
int
model
);
__
U
INT16_T
__atomic_load_2
(
__
U
INT16_T
*
mem
,
int
model
);
/*@
/*@
requires validity: \valid_read(mem);
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT32_T
__atomic_load_4
(
__INT32_T
*
mem
,
int
model
);
__
U
INT32_T
__atomic_load_4
(
__
U
INT32_T
*
mem
,
int
model
);
/*@
/*@
requires validity: \valid_read(mem);
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT64_T
__atomic_load_8
(
__INT64_T
*
mem
,
int
model
);
__
U
INT64_T
__atomic_load_8
(
__
U
INT64_T
*
mem
,
int
model
);
/*@
/*@
requires validity: \valid(mem);
requires validity: \valid(mem);
assigns *mem \from val, indirect: model;
assigns *mem \from val, indirect: model;
*/
*/
void
__atomic_store_1
(
__INT8_T
*
mem
,
__INT8_T
val
,
int
model
);
void
__atomic_store_1
(
__
U
INT8_T
*
mem
,
__
U
INT8_T
val
,
int
model
);
/*@
/*@
requires validity: \valid(mem);
requires validity: \valid(mem);
assigns *mem \from val, indirect: model;
assigns *mem \from val, indirect: model;
*/
*/
void
__atomic_store_2
(
__INT16_T
*
mem
,
__INT16_T
val
,
int
model
);
void
__atomic_store_2
(
__
U
INT16_T
*
mem
,
__
U
INT16_T
val
,
int
model
);
/*@
/*@
requires validity: \valid(mem);
requires validity: \valid(mem);
assigns *mem \from val, indirect: model;
assigns *mem \from val, indirect: model;
*/
*/
void
__atomic_store_4
(
__INT32_T
*
mem
,
__INT32_T
val
,
int
model
);
void
__atomic_store_4
(
__
U
INT32_T
*
mem
,
__
U
INT32_T
val
,
int
model
);
/*@
/*@
requires validity: \valid(mem);
requires validity: \valid(mem);
assigns *mem \from val, indirect: model;
assigns *mem \from val, indirect: model;
*/
*/
void
__atomic_store_8
(
__INT64_T
*
mem
,
__INT64_T
val
,
int
model
);
void
__atomic_store_8
(
__
U
INT64_T
*
mem
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(mem);
/*@ requires validity: \valid(mem);
assigns *mem \from val, indirect:model;
assigns *mem \from val, indirect:model;
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT8_T
__atomic_exchange_1
(
__INT8_T
*
mem
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_exchange_1
(
__
U
INT8_T
*
mem
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(mem);
/*@ requires validity: \valid(mem);
assigns *mem \from val, indirect:model;
assigns *mem \from val, indirect:model;
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT16_T
__atomic_exchange_2
(
__INT16_T
*
mem
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_exchange_2
(
__
U
INT16_T
*
mem
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(mem);
/*@ requires validity: \valid(mem);
assigns *mem \from val, indirect:model;
assigns *mem \from val, indirect:model;
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT32_T
__atomic_exchange_4
(
__INT32_T
*
mem
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_exchange_4
(
__
U
INT32_T
*
mem
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(mem);
/*@ requires validity: \valid(mem);
assigns *mem \from val, indirect:model;
assigns *mem \from val, indirect:model;
assigns \result \from *mem, indirect:model;
assigns \result \from *mem, indirect:model;
*/
*/
__INT64_T
__atomic_exchange_8
(
__INT64_T
*
mem
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_exchange_8
(
__
U
INT64_T
*
mem
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(mem) && \valid_read(expected);
/*@ requires validity: \valid(mem) && \valid_read(expected);
assigns *mem \from *mem, indirect: *expected, desired,
assigns *mem \from *mem, indirect: *expected, desired,
...
@@ -340,9 +340,9 @@ __INT64_T __atomic_exchange_8(__INT64_T* mem, __INT64_T val, int model);
...
@@ -340,9 +340,9 @@ __INT64_T __atomic_exchange_8(__INT64_T* mem, __INT64_T val, int model);
assigns \result \from indirect: *mem, indirect: *expected;
assigns \result \from indirect: *mem, indirect: *expected;
*/
*/
_Bool
__atomic_compare_exchange_1
(
_Bool
__atomic_compare_exchange_1
(
__INT8_T
*
mem
,
__
U
INT8_T
*
mem
,
__INT8_T
*
expected
,
__
U
INT8_T
*
expected
,
__INT8_T
desired
,
__
U
INT8_T
desired
,
_Bool
weak
,
int
success_model
,
int
failure_model
);
_Bool
weak
,
int
success_model
,
int
failure_model
);
/*@ requires validity: \valid(mem) && \valid_read(expected);
/*@ requires validity: \valid(mem) && \valid_read(expected);
...
@@ -353,9 +353,9 @@ _Bool __atomic_compare_exchange_1(
...
@@ -353,9 +353,9 @@ _Bool __atomic_compare_exchange_1(
assigns \result \from indirect: *mem, indirect: *expected;
assigns \result \from indirect: *mem, indirect: *expected;
*/
*/
_Bool
__atomic_compare_exchange_2
(
_Bool
__atomic_compare_exchange_2
(
__INT16_T
*
mem
,
__
U
INT16_T
*
mem
,
__INT16_T
*
expected
,
__
U
INT16_T
*
expected
,
__INT16_T
desired
,
__
U
INT16_T
desired
,
_Bool
weak
,
int
success_model
,
int
failure_model
);
_Bool
weak
,
int
success_model
,
int
failure_model
);
/*@ requires validity: \valid(mem) && \valid_read(expected);
/*@ requires validity: \valid(mem) && \valid_read(expected);
...
@@ -366,9 +366,9 @@ _Bool __atomic_compare_exchange_2(
...
@@ -366,9 +366,9 @@ _Bool __atomic_compare_exchange_2(
assigns \result \from indirect: *mem, indirect: *expected;
assigns \result \from indirect: *mem, indirect: *expected;
*/
*/
_Bool
__atomic_compare_exchange_4
(
_Bool
__atomic_compare_exchange_4
(
__INT32_T
*
mem
,
__
U
INT32_T
*
mem
,
__INT32_T
*
expected
,
__
U
INT32_T
*
expected
,
__INT32_T
desired
,
__
U
INT32_T
desired
,
_Bool
weak
,
int
success_model
,
int
failure_model
);
_Bool
weak
,
int
success_model
,
int
failure_model
);
/*@ requires validity: \valid(mem) && \valid_read(expected);
/*@ requires validity: \valid(mem) && \valid_read(expected);
...
@@ -379,250 +379,250 @@ _Bool __atomic_compare_exchange_4(
...
@@ -379,250 +379,250 @@ _Bool __atomic_compare_exchange_4(
assigns \result \from indirect: *mem, indirect: *expected;
assigns \result \from indirect: *mem, indirect: *expected;
*/
*/
_Bool
__atomic_compare_exchange_8
(
_Bool
__atomic_compare_exchange_8
(
__INT64_T
*
mem
,
__
U
INT64_T
*
mem
,
__INT64_T
*
expected
,
__
U
INT64_T
*
expected
,
__INT64_T
desired
,
__
U
INT64_T
desired
,
_Bool
weak
,
int
success_model
,
int
failure_model
);
_Bool
weak
,
int
success_model
,
int
failure_model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_add_fetch_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_add_fetch_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_sub_fetch_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_sub_fetch_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_and_fetch_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_and_fetch_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_xor_fetch_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_xor_fetch_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_or_fetch_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_or_fetch_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_nand_fetch_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_nand_fetch_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_add_fetch_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_add_fetch_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_sub_fetch_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_sub_fetch_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_and_fetch_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_and_fetch_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_xor_fetch_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_xor_fetch_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_or_fetch_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_or_fetch_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_nand_fetch_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_nand_fetch_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_add_fetch_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_add_fetch_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_sub_fetch_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_sub_fetch_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_and_fetch_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_and_fetch_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_xor_fetch_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_xor_fetch_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_or_fetch_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_or_fetch_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_nand_fetch_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_nand_fetch_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_add_fetch_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_add_fetch_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_sub_fetch_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_sub_fetch_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_and_fetch_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_and_fetch_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_xor_fetch_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_xor_fetch_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_or_fetch_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_or_fetch_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_nand_fetch_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_nand_fetch_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_fetch_add_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_fetch_add_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_fetch_sub_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_fetch_sub_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_fetch_and_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_fetch_and_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_fetch_xor_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_fetch_xor_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_fetch_or_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_fetch_or_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT8_T
__atomic_fetch_nand_1
(
__INT8_T
*
ptr
,
__INT8_T
val
,
int
model
);
__
U
INT8_T
__atomic_fetch_nand_1
(
__
U
INT8_T
*
ptr
,
__
U
INT8_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_fetch_add_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_fetch_add_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_fetch_sub_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_fetch_sub_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_fetch_and_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_fetch_and_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_fetch_xor_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_fetch_xor_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_fetch_or_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_fetch_or_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT16_T
__atomic_fetch_nand_2
(
__INT16_T
*
ptr
,
__INT16_T
val
,
int
model
);
__
U
INT16_T
__atomic_fetch_nand_2
(
__
U
INT16_T
*
ptr
,
__
U
INT16_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_fetch_add_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_fetch_add_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_fetch_sub_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_fetch_sub_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_fetch_and_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_fetch_and_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_fetch_xor_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_fetch_xor_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_fetch_or_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_fetch_or_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT32_T
__atomic_fetch_nand_4
(
__INT32_T
*
ptr
,
__INT32_T
val
,
int
model
);
__
U
INT32_T
__atomic_fetch_nand_4
(
__
U
INT32_T
*
ptr
,
__
U
INT32_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_fetch_add_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_fetch_add_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_fetch_sub__8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_fetch_sub__8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_fetch_and_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_fetch_and_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_fetch_xor_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_fetch_xor_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_fetch_or_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_fetch_or_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid(ptr);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
*/
__INT64_T
__atomic_fetch_nand_8
(
__INT64_T
*
ptr
,
__INT64_T
val
,
int
model
);
__
U
INT64_T
__atomic_fetch_nand_8
(
__
U
INT64_T
*
ptr
,
__
U
INT64_T
val
,
int
model
);
/*@ requires validity: \valid((char*)ptr);
/*@ requires validity: \valid((char*)ptr);
assigns \result \from *((char*)ptr);
assigns \result \from *((char*)ptr);
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment