[eacsl:runtime] Fix `\valid` and `\valid_read` when the memory location is an empty set

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

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