Skip to content
Snippets Groups Projects
Commit 50a040f9 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Fix the issue where literal strings in the code were not replaced by the

variables (which point to literal strings) generated by E-ACSL
parent a35669aa
No related branches found
No related tags found
No related merge requests found
......@@ -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 _ =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment