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 7e856ef6c22fe954171ad9befc133d239c017f41..70b77c7a4a677748383182144bf8bdbf004e7cdf 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 b08cea658aaa76e0fe4d3e40c163fb830dc8569f..88c378a96fb0a9192ee5f58680cb5fdd66b5cc72 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