diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 9ffefdf917e713a53bbed1c6b3f3581244ee39af..4a1e5e711d7024edf490b74237e69ea1eec76c58 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -21,6 +21,13 @@
# configure configure
###############################################################################
+############################
+Plugin E-ACSL <next-release>
+############################
+
+-* E-ACSL [2020-06-18] Fix support of VLA memory tracking.
+ (frama-c/e-acsl#119)
+
#############################
Plugin E-ACSL 21.0 (Scandium)
#############################
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 923affc32ced8756a88b0bc9bab3e60f61e07f35..9c7e60f4979d262a98e8ea79da9a41a0aa9d699d 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -105,12 +105,9 @@ let mk_rtl_call ~loc ?result fname args =
(** {2 Handling the E-ACSL's C-libraries, part II} *)
(* ************************************************************************** *)
-let mk_full_init_stmt ?(addr=true) vi =
+let mk_full_init_stmt vi =
let loc = vi.vdecl in
- let mk = mk_rtl_call ~loc "full_init" in
- match addr, Cil.unrollType vi.vtype with
- | _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
- | _ -> mk [ Cil.mkAddrOfVi vi ]
+ mk_rtl_call ~loc "full_init" [ Cil.evar ~loc vi ]
let mk_initialize ~loc (host, offset as lv) = match host, offset with
| Var _, NoOffset ->
@@ -150,11 +147,11 @@ let mk_store_stmt ?str_size vi =
let mk_duplicate_store_stmt ?str_size vi =
mk_named_store_stmt "store_block_duplicate" ?str_size vi
-let mk_delete_stmt vi =
+let mk_delete_stmt ?(is_addr=false) vi =
let loc = vi.vdecl in
let mk = mk_rtl_call ~loc "delete_block" in
- match Cil.unrollType vi.vtype with
- | TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
+ match is_addr, Cil.unrollType vi.vtype with
+ | _, TArray(_, Some _, _, _) | true, _ -> mk [ Cil.evar ~loc vi ]
| _ -> mk [ Cil.mkAddrOfVi vi ]
let mk_mark_readonly vi =
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index b286e62ca2ea8184a86152dfae56312102c76a39..c309ad478045a7e41d6582ae886931bce1b0fdcd 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -54,13 +54,15 @@ val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
(** Same as [mk_store_stmt] for [__e_acsl_duplicate_store_block] that first
checks for a previous allocation of the given varinfo. *)
-val mk_delete_stmt: varinfo -> stmt
+val mk_delete_stmt: ?is_addr:bool -> varinfo -> stmt
(** Same as [mk_store_stmt] for [__e_acsl_delete_block] that observes the
- de-allocation of the given varinfo. *)
+ de-allocation of the given varinfo.
+ If [is_addr] is false (default), take the address of varinfo. *)
-val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
+val mk_full_init_stmt: varinfo -> stmt
(** Same as [mk_store_stmt] for [__e_acsl_full_init] that observes the
- initialization of the given varinfo. *)
+ initialization of the given varinfo. The varinfo is the address to fully
+ initialize, no [addrOf] is taken. *)
val mk_initialize: loc:location -> lval -> stmt
(** Same as [mk_store_stmt] for [__e_acsl_initialize] that observes the
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 703b4a6f6f60fca6d7f3333d31c43d3baed817b4..a89178c89937f87f01466e80690473f37d7f64e6 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -138,7 +138,7 @@ let mk_init_function () =
let str_size = Cil.new_exp loc (SizeOfStr s) in
Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
:: Constructor.mk_store_stmt ~str_size vi
- :: Constructor.mk_full_init_stmt ~addr:false vi
+ :: Constructor.mk_full_init_stmt vi
:: Constructor.mk_mark_readonly vi
:: stmts)
stmts
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 58f3b018d525da5cea25fead897c3ca9e1a7a35a..a0357a168fdf9772d83de8409e5734b3062a43da 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -59,17 +59,7 @@ let rec inject_in_init env kf_opt vi off = function
let inject_in_local_init loc env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
- (* handle variable-length array allocation via [__fc_vla_alloc]. Here each
- instance of [__fc_vla_alloc] is rewritten to [alloca] (that is used to
- implement VLA) and further a custom call to [store_block] tracking VLA
- allocation is issued. *)
- (* KV: do not add handling [alloca] allocation here (or anywhere else for
- that matter). Handling of [alloca] should be implemented in Frama-C
- (eventually). This is such that each call to [alloca] becomes
- [__fc_vla_alloc]. It is already handled using the code below. *)
- fvi.vname <- Functions.Libc.actual_alloca;
- (* Since we need to pass [vi] by value, cannot use [Misc.mk_store_stmt]
- here. Do it manually. *)
+ (* add a store statement when creating a variable length array *)
let store = Constructor.mk_store_stmt ~str_size:sz vi in
let env = Env.add_stmt ~post:true env kf store in
init, env
@@ -122,12 +112,6 @@ let rename_caller loc args exp = match exp.enode with
vi.vname <- Functions.RTL.get_rtl_replacement_name vi.vname;
exp, args
- | Lval(Var vi , _) when Functions.Libc.is_vla_free_name vi.vname ->
- (* handle variable-length array allocation via [__fc_vla_free]. Rewrite its
- name to [delete_block]. The rest is in place. *)
- vi.vname <- Functions.RTL.mk_api_name "delete_block";
- exp, args
-
| Lval(Var vi, _)
when Options.Validate_format_strings.get ()
&& Functions.Libc.is_printf_name vi.vname
@@ -200,6 +184,17 @@ let inject_in_instr env kf stmt = function
| _ ->
env
in
+ (* if this is a call to free a vla, add a call to delete_block *)
+ let env =
+ if Functions.Libc.is_vla_free caller then
+ match args with
+ | [ { enode = CastE (_, { enode = Lval (Var vi, NoOffset) }) } ] ->
+ let delete_block = Constructor.mk_delete_stmt ~is_addr:true vi in
+ Env.add_stmt env kf delete_block
+ | _ -> Options.fatal "The normalization of __fc_vla_free() has changed"
+ else
+ env
+ in
Call(result, caller, args, loc), env
| Local_init(vi, linit, loc) ->
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index a7f26523d4c08bd8b4028b8522d8f3073ecb857c..0c6c931c4754a04db314b86e69710985c304155f 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -205,13 +205,43 @@ let change_printer =
let module Printer_class(X: Printer.PrinterClass) = struct
class printer = object
inherit X.printer as super
+
method !varinfo fmt vi =
- if vi.Cil_types.vghost || vi.Cil_types.vstorage <> Cil_types.Extern
- then
- super#varinfo fmt vi
- else
+ if Functions.Libc.is_vla_alloc_name vi.Cil_types.vname then
+ (* Replace VLA allocation with calls to [__builtin_alloca] *)
+ Format.fprintf fmt "%s" Functions.Libc.actual_alloca
+ else if (not vi.vghost) && vi.vstorage == Cil_types.Extern then
+ (* Replace calls to Frama-C builtins with calls to their original
+ version from the libc *)
let s = Str.replace_first r "" vi.Cil_types.vname in
Format.fprintf fmt "%s" s
+ else
+ (* Otherwise use the original printer *)
+ super#varinfo fmt vi
+
+ method !instr fmt i =
+ match i with
+ | Call(_, fct, _, _) when Functions.Libc.is_vla_free fct ->
+ (* Nothing to print: VLA deallocation is done automatically when
+ leaving the scope *)
+ Format.fprintf fmt "/* ";
+ super#instr fmt i;
+ Format.fprintf fmt " */"
+ | _ ->
+ super#instr fmt i
+
+ method !global fmt g =
+ let is_vla_builtin vi =
+ Functions.Libc.is_vla_alloc_name vi.Cil_types.vname ||
+ Functions.Libc.is_vla_free_name vi.Cil_types.vname
+ in
+ match g with
+ | GFunDecl (_, vi, _) when is_vla_builtin vi ->
+ (* Nothing to print: the VLA builtins don't have an original libc
+ version. *)
+ ()
+ | _ ->
+ super#global fmt g
end
end in
Printer.update_printer (module Printer_class: Printer.PrinterExtension)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
index 646d3b855887d7fdf258439c0fb0ee5483127a1f..d2039f2b5ee5f5dc7add5b7346d91dfabeb5e52a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
@@ -2,12 +2,6 @@
#include "stdio.h"
#include "stdlib.h"
int LEN = 10;
-/*@ assigns \nothing;
- frees p; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *p);
-
-/* compiler builtin:
- __attribute__((__FC_BUILTIN__)) void *__builtin_alloca(unsigned long size); */
int main(int argc, char **argv)
{
int __retres;
@@ -67,6 +61,7 @@ int main(int argc, char **argv)
}
__retres = 0;
__e_acsl_delete_block((void *)arr);
+ /* __fc_vla_free((void *)arr); */
__e_acsl_delete_block((void *)(& arr));
__e_acsl_memory_clean();
return __retres;