From 4ad7247c8aa70a6d7a2c4b6f2a6e360d6d0eab59 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 6 Oct 2020 10:50:23 +0200
Subject: [PATCH] [eacsl:runtime] Fix `\valid` and `\valid_read` when the
memory location is an empty set
---
.../bittree_model/e_acsl_bittree_observation_model.c | 10 ++++++++--
.../segment_model/e_acsl_segment_observation_model.c | 7 ++++++-
2 files changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index 7e856ef6c22..70b77c7a4a6 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -229,7 +229,10 @@ static bt_block* lookup_allocated(void* ptr, size_t size, void *ptr_base) {
/* return whether the size bytes of ptr are readable/writable */
int valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
bt_block * blk = lookup_allocated(ptr, size, ptr_base);
- return blk != NULL && !blk->is_readonly
+ return
+ size == 0
+ ||
+ blk != NULL && !blk->is_readonly
#ifdef E_ACSL_TEMPORAL
&& temporal_valid(ptr_base, addrof_base)
#endif
@@ -239,7 +242,10 @@ int valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
/* return whether the size bytes of ptr are readable */
int valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
bt_block * blk = lookup_allocated(ptr, size, ptr_base);
- return blk != NULL
+ return
+ size == 0
+ ||
+ blk != NULL
#ifdef E_ACSL_TEMPORAL
&& temporal_valid(ptr_base, addrof_base)
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
index b08cea658aa..88c378a96fb 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
@@ -86,6 +86,8 @@ void mark_readonly(void *ptr) {
int valid(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
return
+ size == 0
+ ||
allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
&& !readonly(ptr)
#ifdef E_ACSL_TEMPORAL
@@ -95,7 +97,10 @@ int valid(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
}
int valid_read(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
- return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
+ return
+ size == 0
+ ||
+ allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
#ifdef E_ACSL_TEMPORAL
&& temporal_valid(ptr_base, addrof_base)
#endif
--
GitLab