diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index 06de2ff30084b994cf94d4990e059c9f338cc1bd..b8d78267e6cc6534fe9a4bd24ee62245b08b95a6 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -80,7 +80,6 @@ static void mark_readonly(void * ptr) {
/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
static int readonly (void *ptr) {
uintptr_t addr = (uintptr_t)ptr;
- DVALIDATE_ALLOCATED(addr, 1, addr);
return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index f601e15c4ebfce8bde5120a454f3cefd053d1518..0b1e549001a93ffe68d98bab4afe6c1a814edb36 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -327,13 +327,13 @@ static void validate_memory_layout() {
# define DVALIDATE_STATIC_ACCESS(_addr, _size) \
DVASSERT(IS_ON_STATIC(_addr), "Expected static location: %a\n ", _addr); \
DVASSERT(static_allocated((uintptr_t)_addr, _size,(uintptr_t)_addr), \
- "Operation on unallocated block [%a + %lu]\n ", _addr, _size)
+ "Operation on unallocated static block [%a + %lu]\n ", _addr, _size)
/* Same as ::DVALIDATE_STATIC_LOCATION but for a single memory location */
# define DVALIDATE_STATIC_LOCATION(_addr) \
DVASSERT(IS_ON_STATIC(_addr), "Expected static location: %a\n", _addr); \
DVASSERT(static_allocated_one((uintptr_t)_addr), \
- "Operation on unallocated block [%a]\n ", _addr)
+ "Operation on unallocated static block [%a]\n ", _addr)
/* Assert that every location belonging to the range [_addr, _addr + _size] is
* - belongs to a tracked static region (i.e., stack, TLS or global)
@@ -355,7 +355,7 @@ static void validate_memory_layout() {
/* Assert that memory block [_addr, _addr + _size] is allocated */
# define DVALIDATE_ALLOCATED(_addr, _size, _base) \
DVASSERT(allocated((uintptr_t)_addr, _size, (uintptr_t)_base), \
- "Operation on unallocated block [%a + %lu] with base %lu\n ", \
+ "Operation on unallocated block [%a + %lu] with base %a\n ", \
_addr, _size, _base)
/* Assert that memory block [_addr, _addr + _size] is allocated
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
index d52be564121ca61dc821df1d1de213a1344ca949..db06d1608c903c04c71dc2b00867e2c01e98617e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
@@ -13,27 +13,17 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- int *p;
- int *q;
- int a;
- int b;
- int c;
- char *pmin;
- char *pmax;
- int diff;
__e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& pmax),(size_t)8);
- __e_acsl_store_block((void *)(& pmin),(size_t)8);
- __e_acsl_store_block((void *)(& b),(size_t)4);
+ int *p = (int *)0;
__e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
- p = (int *)0;
- q = (int *)0;
- a = 1;
+ int *q = (int *)0;
+ int a = 1;
+ int b = 2;
+ __e_acsl_store_block((void *)(& b),(size_t)4);
__e_acsl_full_init((void *)(& b));
- b = 2;
- c = 3;
+ int c = 3;
__e_acsl_full_init((void *)(& p));
p = & b;
/*@ assert \valid(p); */
@@ -94,18 +84,19 @@ int main(int argc, char **argv)
(char *)"main",(char *)"!\\valid(p + 1)",31);
}
}
+ char *pmin = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& pmin),(size_t)8);
__e_acsl_full_init((void *)(& pmin));
- pmin = (char *)malloc(sizeof(int));
+ char *pmax = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& pmax),(size_t)8);
__e_acsl_full_init((void *)(& pmax));
- pmax = (char *)malloc(sizeof(int));
/*@ assert
Value: ptr_comparison: \pointer_comparable((void *)pmin, (void *)pmax);
*/
if ((unsigned long)pmin > (unsigned long)pmax) {
- char *t;
+ char *t = pmin;
__e_acsl_store_block((void *)(& t),(size_t)8);
__e_acsl_full_init((void *)(& t));
- t = pmin;
__e_acsl_full_init((void *)(& pmin));
pmin = pmax;
__e_acsl_full_init((void *)(& pmax));
@@ -118,7 +109,7 @@ int main(int argc, char **argv)
__e_acsl_initialize((void *)pmax,sizeof(char));
/*@ assert Value: mem_access: \valid(pmax); */
*pmax = (char)'L';
- diff = (int)(pmax - pmin);
+ int diff = (int)(pmax - pmin);
/*@ assert \valid(pmin); */
{
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
index f5a71822eb517779399c79fb801f5cc3f2f2211e..51cb3558778e1dd709c34ef1854bd9838cd97d38 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
@@ -11,19 +11,19 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("t is %d, going to %s\n"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
__gen_e_acsl_literal_string_3 = "UP";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,sizeof("UP"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
__gen_e_acsl_literal_string_2 = "RET";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("RET"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
__gen_e_acsl_literal_string_4 = "AGAIN";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,sizeof("AGAIN"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
return;
}
@@ -47,10 +47,13 @@ int main(int argc, char const **argv)
a = 1;
/*@ assert \valid(&a); */
{
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int));
- __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
- (char *)"main",(char *)"\\valid(&a)",25);
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)(& a));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(&a)",25);
+ }
}
if (t == 2) {
__gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
@@ -64,10 +67,13 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& b));
/*@ assert \valid(&b); */
{
- int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int));
- __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
- (char *)"main",(char *)"\\valid(&b)",36);
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+ (void *)(& b),(void *)(& b));
+ __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(&b)",36);
+ }
}
__gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
(char *)__gen_e_acsl_literal_string_4);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index aa98ce917a78fe13add39ee46ff574cbfe170643..bef3b9f0f0ae33f08f6b48d5e0521f3df324633a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -71,7 +71,7 @@ int main(void)
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - i),
sizeof(int),
(void *)(& t[2]),
- (void *)(& t[2] - i));
+ (void *)(& t[2]));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(&t[2] - i)",19);