diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 06edca935965881a93c24f23401dc0211922ed8e..eb3472ecd74ebbc3e080aca963a45add033a0e97 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -55,7 +55,7 @@ SRC_PROJECT_INITIALIZER:=\
SRC_ANALYSES:= \
rte \
literal_strings \
- mmodel_analysis \
+ memory_tracking \
exit_points \
lscope \
interval \
@@ -73,7 +73,7 @@ SRC_CODE_GENERATOR:= \
loops \
quantif \
at_with_lscope \
- mmodel_translate \
+ memory_translate \
logic_functions \
logic_array \
translate \
@@ -114,9 +114,9 @@ PLUGIN_DEPENDENCIES:= RteGen
EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)
# Suppress a spurious warning with OCaml >= 4.04.0
-$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmo \
-$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
-$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmo \
+$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmi: E_ACSL_BFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmx: E_ACSL_OFLAGS+= -w -60
###############
# Local Flags #
@@ -160,7 +160,7 @@ PLUGIN_TESTS_DIRS := \
arith \
memory \
gmp-only \
- full-mmodel \
+ full-mtracking \
format \
temporal \
special
@@ -291,8 +291,8 @@ EACSL_TEST_FILES = \
tests/test_config_ci.in \
tests/gmp-only/test_config_ci \
tests/gmp-only/test_config_dev \
- tests/full-mmodel/test_config_ci \
- tests/full-mmodel/test_config_dev \
+ tests/full-mtracking/test_config_ci \
+ tests/full-mtracking/test_config_dev \
tests/builtin/test_config_ci \
tests/builtin/test_config_dev \
tests/temporal/test_config_ci \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index f5d1c3fe39a487370af0db226395887366102ade..3a8a5772d08405beb10cd4297ea7c93861d6426e 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -44,8 +44,8 @@ src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/mmodel_analysis.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/mmodel_analysis.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/memory_tracking.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/rte.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/rte.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
@@ -72,8 +72,8 @@ src/code_generator/loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/memory_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/memory_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/mmodel_translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/mmodel_translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/memory_translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/memory_translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/quantif.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/quantif.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/rational.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
@@ -113,8 +113,8 @@ tests/builtin/test_config_ci: .ignore
tests/builtin/test_config_dev: .ignore
tests/format/test_config_ci: .ignore
tests/format/test_config_dev: .ignore
-tests/full-mmodel/test_config_ci: .ignore
-tests/full-mmodel/test_config_dev: .ignore
+tests/full-mtracking/test_config_ci: .ignore
+tests/full-mtracking/test_config_dev: .ignore
tests/gmp-only/test_config_ci: .ignore
tests/gmp-only/test_config_dev: .ignore
tests/temporal/test_config_ci: .ignore
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 0e6a3ac2302a17cae489c61671fb46e4f7946ecc..023dd1cfc9de35ef187803485bfe157e36dfd759 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -43,11 +43,11 @@ let is_empty () = Varinfo.Hashtbl.length tbl = 0
Initializers (used to capture literal strings) are added through
[add_initializer] below. *)
let add vi =
- if Mmodel_analysis.must_model_vi vi then
+ if Memory_tracking.must_monitor_vi vi then
Varinfo.Hashtbl.replace tbl vi (ref [])
let add_initializer vi offset init =
- if Mmodel_analysis.must_model_vi vi then
+ if Memory_tracking.must_monitor_vi vi then
try
let l = Varinfo.Hashtbl.find tbl vi in
l := (offset, init) :: !l
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index cdc6486702d1fbcc234a0f0f7bf19b1f616e74c9..c7ea8438a11895d3bfe22dcb14b0b5f4d4b4764d 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -138,7 +138,7 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
| Var vi, NoOffset -> vi.vglob || vi.vformal
| _ -> false
in
- let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
+ let must_model = Memory_tracking.must_monitor_lval ~stmt ~kf lv in
if not (may_safely_ignore lv) && must_model then
let before = Cil.mkStmt ~valid_sid:true stmt.skind in
let new_stmt =
@@ -515,7 +515,7 @@ and inject_in_block (env: Env.t) kf blk =
if Functions.instrument kf then
List.fold_left
(fun acc vi ->
- if Mmodel_analysis.must_model_vi ~kf vi
+ if Memory_tracking.must_monitor_vi ~kf vi
then Smart_stmt.delete_stmt vi :: acc
else acc)
stmts
@@ -530,7 +530,7 @@ and inject_in_block (env: Env.t) kf blk =
blk.bstmts <-
List.fold_left
(fun acc vi ->
- if Mmodel_analysis.must_model_vi vi && not vi.vdefined
+ if Memory_tracking.must_monitor_vi vi && not vi.vdefined
then Smart_stmt.store_stmt vi :: acc
else acc)
blk.bstmts
@@ -702,7 +702,7 @@ let surround_function_with kf fundec stmt_begin stmt_end =
These functions track the usage of globals if the program being analyzed. *)
let inject_global_handler file main =
Options.feedback ~dkey ~level:2 "building global handler.";
- if Mmodel_analysis.use_model () then
+ if Memory_tracking.use_monitoring () then
(* Create [__e_acsl_globals_init] function *)
let vi_init, fundec_init = Global_observer.mk_init_function () in
let cil_fct_init = GFun(fundec_init, Location.unknown) in
@@ -786,16 +786,16 @@ let inject_global_handler file main =
file.globals <- file.globals @ globals_func
(** Add a call to [__e_acsl_memory_init] and [__e_acsl_memory_clean] if the
- memory model analysis is running.
+ memory tracking analysis is running.
[__e_acsl_memory_init] initializes memory storage and potentially records
program arguments. Parameters to [__e_acsl_memory_init] are addresses of
program arguments or NULLs if [main] is declared without arguments.
[__e_acsl_memory_clean] clean the memory allocated by
[__e_acsl_memory_init]. *)
-let inject_mmodel_handler main =
+let inject_mtracking_handler main =
(* Only inject memory init and memory clean if the memory model analysis is
running *)
- if Mmodel_analysis.use_model () then begin
+ if Memory_tracking.use_monitoring () then begin
let loc = Location.unknown in
let nulls = [ Cil.zero loc ; Cil.zero loc ] in
let handle_main main =
@@ -837,13 +837,13 @@ let inject_in_file file =
if not (Global_observer.is_empty () && Literal_strings.is_empty ()) then
inject_global_handler file main;
file.globals <- Logic_functions.add_generated_functions file.globals;
- inject_mmodel_handler main
+ inject_mtracking_handler main
let reset_all ast =
(* by default, do not run E-ACSL on the generated code *)
Options.Run.off ();
(* reset all the E-ACSL environments to their original states *)
- Mmodel_analysis.reset ();
+ Memory_tracking.reset ();
Logic_functions.reset ();
Literal_strings.reset ();
Global_observer.reset ();
diff --git a/src/plugins/e-acsl/src/code_generator/literal_observer.ml b/src/plugins/e-acsl/src/code_generator/literal_observer.ml
index 9cc7e7f8b5e566285e6ba08231578420f038fca2..8b3bd0f99193c163abc41e86d508bf8974a0b239 100644
--- a/src/plugins/e-acsl/src/code_generator/literal_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/literal_observer.ml
@@ -52,7 +52,7 @@ let subst_all_literals_in_exp env kf e =
(* the guard below could be optimized: if no annotation depends on this
string, then it is not required to monitor it.
(currently, the guard says: "no annotation uses the memory model" *)
- | Const (CStr s) when Mmodel_analysis.use_model () ->
+ | Const (CStr s) when Memory_tracking.use_monitoring () ->
let e, env = literal e.eloc !env_ref kf s in
env_ref := env;
Cil.ChangeTo e
diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.ml b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
index 629e30432278b7a6912f33453939a7476c31632e..1babc64d9246264cbd2fcf76094218ac2ca099ab 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
@@ -26,7 +26,7 @@ let tracking_stmt ?before fold mk_stmt env kf vars =
if Functions.instrument kf then
fold
(fun vi env ->
- if Mmodel_analysis.must_model_vi ~kf vi then
+ if Memory_tracking.must_monitor_vi ~kf vi then
Env.add_stmt ?before env kf (mk_stmt vi)
else
env)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.mli b/src/plugins/e-acsl/src/code_generator/memory_observer.mli
index 24b4556658713db974efb2a1ea95364b6864d633..7fb098d7655305e782dafe533d6a7b5af69528bf 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.mli
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.mli
@@ -27,7 +27,7 @@ open Cil_types
open Cil_datatype
val store: ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
-(** For each variable of the given list, if necessary according to the mmodel
+(** For each variable of the given list, if necessary according to the mtracking
analysis, add a call to [__e_acsl_store_block] in the given environment. *)
val duplicate_store:
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index 96f5c22ee29764fd99bded8ea64abf265fabb0d0..d0f6ced85f13d7305efda530e904f39ae1dd8cfc 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -216,7 +216,7 @@ let mk_stmt_from_assign loc lhs rhs =
(* Top-level handler for Set instructions *)
let set_instr ?(post=false) current_stmt loc lhs rhs env kf =
- if Mmodel_analysis.must_model_lval ~kf lhs then
+ if Memory_tracking.must_monitor_lval ~kf lhs then
Extlib.may_map
(fun stmt -> Env.add_stmt ~before:current_stmt ~post env kf stmt)
~dft:env
@@ -248,7 +248,7 @@ end = struct
Extlib.may_map
(fun (_, rhs, flow) ->
let env =
- if Mmodel_analysis.must_model_exp ~kf param then
+ if Memory_tracking.must_monitor_exp ~kf param then
let stmt = Mk.save_param ~loc flow rhs index in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else env
@@ -341,7 +341,7 @@ end = struct
let alloc = not has_def in
Extlib.may_map
(fun lhs ->
- if Mmodel_analysis.must_model_lval ~kf lhs then
+ if Memory_tracking.must_monitor_lval ~kf lhs then
call_with_ret ~alloc current_stmt loc lhs env kf
else env)
~dft:env
@@ -371,7 +371,7 @@ end = struct
inits
let instr current_stmt vi li loc env kf =
- if Mmodel_analysis.must_model_vi ~kf vi then
+ if Memory_tracking.must_monitor_vi ~kf vi then
match li with
| AssignInit init ->
handle_init current_stmt NoOffset loc vi init env kf
@@ -421,7 +421,7 @@ let handle_return_stmt loc ret env kf =
| _ -> Options.fatal "Something other than Lval in return"
let handle_return_stmt loc ret env kf =
- if Mmodel_analysis.must_model_exp ~kf ret then
+ if Memory_tracking.must_monitor_exp ~kf ret then
handle_return_stmt loc ret env kf
else
env
@@ -491,7 +491,7 @@ let handle_function_parameters kf env =
let env, _ = List.fold_left
(fun (env, index) param ->
let env =
- if Mmodel_analysis.must_model_vi ~kf param
+ if Memory_tracking.must_monitor_vi ~kf param
then track_argument param index env kf
else env
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 480059c4a519525c12412c38593cbdc08d9316d0..882a4b41f47538d813a323368c356c09f0040c83 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -583,7 +583,8 @@ and context_insensitive_term_to_exp kf env t =
if Misc.is_set_of_ptr_or_array t1.term_type ||
Misc.is_set_of_ptr_or_array t2.term_type then
(* case of arithmetic over set of pointers (due to use of ranges)
- should have already been handled in [mmodel_call_with_ranges] *)
+ should have already been handled in [Memory_translate.call_with_ranges]
+ *)
assert false;
(* binary operation over pointers *)
let ty = match t1.term_type with
@@ -696,19 +697,19 @@ and context_insensitive_term_to_exp kf env t =
e, env, sty, ""
| Tbase_addr(BuiltinLabel Here, t) ->
let name = "base_addr" in
- let e, env = Mmodel_translate.call ~loc kf name Cil.voidPtrType env t in
+ let e, env = Memory_translate.call ~loc kf name Cil.voidPtrType env t in
e, env, C_number, name
| Tbase_addr _ -> not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
let name = "offset" in
- let e, env = Mmodel_translate.call ~loc kf name size_t env t in
+ let e, env = Memory_translate.call ~loc kf name size_t env t in
e, env, C_number, name
| Toffset _ -> not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
let name = "block_length" in
- let e, env = Mmodel_translate.call ~loc kf name size_t env t in
+ let e, env = Memory_translate.call ~loc kf name size_t env t in
e, env, C_number, name
| Tblock_length _ -> not_yet env "labeled \\block_length"
| Tnull ->
@@ -965,7 +966,7 @@ and named_predicate_content_to_exp ?name kf env p =
| Pvalid_read _ -> "valid_read"
| _ -> assert false
in
- Mmodel_translate.call_valid ~loc kf name Cil.intType env t
+ Memory_translate.call_valid ~loc kf name Cil.intType env t
in
if !is_visiting_valid then begin
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
@@ -996,7 +997,7 @@ and named_predicate_content_to_exp ?name kf env p =
vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
Cil.one ~loc, env
| _ ->
- Mmodel_translate.call_with_size
+ Memory_translate.call_with_size
~loc
kf
"initialized"
@@ -1007,7 +1008,7 @@ and named_predicate_content_to_exp ?name kf env p =
| Pinitialized _ -> not_yet env "labeled \\initialized"
| Pallocable _ -> not_yet env "\\allocate"
| Pfreeable(BuiltinLabel Here, t) ->
- Mmodel_translate.call ~loc kf "freeable" Cil.intType env t
+ Memory_translate.call ~loc kf "freeable" Cil.intType env t
| Pfreeable _ -> not_yet env "labeled \\freeable"
| Pfresh _ -> not_yet env "\\fresh"
@@ -1095,8 +1096,8 @@ let () =
Quantif.predicate_to_exp_ref := named_predicate_to_exp;
At_with_lscope.term_to_exp_ref := term_to_exp;
At_with_lscope.predicate_to_exp_ref := named_predicate_to_exp;
- Mmodel_translate.term_to_exp_ref := term_to_exp;
- Mmodel_translate.predicate_to_exp_ref := named_predicate_to_exp;
+ Memory_translate.term_to_exp_ref := term_to_exp;
+ Memory_translate.predicate_to_exp_ref := named_predicate_to_exp;
Logic_functions.term_to_exp_ref := term_to_exp;
Logic_functions.named_predicate_to_exp_ref := named_predicate_to_exp;
Logic_array.translate_rte_ref := translate_rte