From 701430c5eefdabe8738409ed5351c1fd59228f34 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 7 Dec 2015 18:26:20 +0100
Subject: [PATCH] Fix the issue where literal strings in the code were not
replaced by the variables (which point to literal strings) generated by
E-ACSL
---
src/plugins/e-acsl/visit.ml | 16 +++++++++++++---
1 file changed, 13 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index c8497604695..bbb5bc6fff1 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -719,10 +719,20 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
if generate then Cil.DoChildrenPost handle_memory else Cil.DoChildren
+ (* Processing expressions for the purpose of replacing literal strings found
+ in the code with variables generated by E-ACSL. *)
method !vexpr _ =
- if generate then
- Cil.DoChildren
- else
+ if generate then begin
+ match is_initializer with
+ (* Do not touch global initialisers because they accept only constants *)
+ | true -> Cil.DoChildren
+ (* Replace literal strings elsewhere *)
+ | false -> Cil.DoChildrenPost
+ (fun e ->
+ let e, env = self#literal_string !function_env e in
+ function_env := env;
+ e)
+ end else
Cil.SkipChildren
method !vterm _ =
--
GitLab