diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index c84976046952192cb8597814836315df775379e0..bbb5bc6fff1713914195892336d5a763fe3ec29c 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 _ =