From 34e59f10de040ee85ebf9530fee232465f992cb8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 Mar 2024 15:29:30 +0100
Subject: [PATCH] [Eva] Fixes reduction on the negation of ACSL predicate
valid_string.
---
src/plugins/eva/legacy/eval_terms.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 2943a97ab7d..ab2f98468fb 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -2046,6 +2046,8 @@ and reduce_by_valid_string ~alarm_mode env positive ~wide ~access arg =
let aux base offset acc =
let value = Cvalue.V.inject base offset in
let v, alarms = apply_logic_builtin wrapper env [value] in
+ (* Beware of not removing const strings on the negation of \valid_string. *)
+ let alarms = alarms || (access = Write && Base.is_read_only base) in
if (positive && Cvalue.V.is_bottom v)
|| (not positive && not alarms)
then acc
--
GitLab