Skip to content
Snippets Groups Projects
Commit db205902 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Refactor valid and valid_read using allocated

parent f60b1116
No related branches found
No related tags found
No related merge requests found
...@@ -77,31 +77,6 @@ static void mark_readonly(void * ptr) { ...@@ -77,31 +77,6 @@ static void mark_readonly(void * ptr) {
/* E-ACSL annotations */ /* E-ACSL annotations */
/* ****************** */ /* ****************** */
static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
uintptr_t addr = (uintptr_t)ptr;
uintptr_t base = (uintptr_t)ptr_base;
if (IS_ON_HEAP(addr))
return heap_allocated(addr, size, base);
else if (IS_ON_STACK(addr) || IS_ON_TLS(addr))
return static_allocated(addr, size, base);
else if (IS_ON_GLOBAL(addr))
return static_allocated(addr, size, base) && !global_readonly(addr);
else if (!IS_ON_VALID(addr))
return 0;
return 0;
}
static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
uintptr_t addr = (uintptr_t)ptr;
uintptr_t base = (uintptr_t)ptr_base;
TRY_SEGMENT_WEAK(addr,
return heap_allocated(addr, size, base),
return static_allocated(addr, size, base));
if (!IS_ON_VALID(addr))
return 0;
return 0;
}
/** \brief Return 1 if a given memory location is read-only and 0 otherwise */ /** \brief Return 1 if a given memory location is read-only and 0 otherwise */
static int readonly (void *ptr) { static int readonly (void *ptr) {
uintptr_t addr = (uintptr_t)ptr; uintptr_t addr = (uintptr_t)ptr;
...@@ -109,6 +84,14 @@ static int readonly (void *ptr) { ...@@ -109,6 +84,14 @@ static int readonly (void *ptr) {
return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0; return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
} }
static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base) && !readonly(ptr);
}
static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base);
}
/*! NB: The implementation for this function can also be specified via /*! NB: The implementation for this function can also be specified via
* \p base_addr macro that will eventually call ::TRY_SEGMENT. The following * \p base_addr macro that will eventually call ::TRY_SEGMENT. The following
* implementation is preferred for performance reasons. */ * implementation is preferred for performance reasons. */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment