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/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 541d6252e8d8b64cc742d235bc164582829e1afc..e861862d1ce6eff8ad4e073cfd608c84c690214e 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,10 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2020-09-15] Deprecate -e-acsl-full-mmodel in favor of
+ -e-acsl-full-mtracking.
+- e-acsl-gcc [2020-09-15] Deprecate --full-mmodel in favor of
+ --full-mtracking.
-* E-ACSL [2020-08-28] Fix crash that may occur when translating
properties that have been proved valid by another plug-in
(frama-c/e-acsl#106).
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index c42ab93808d1fb2fbfb644ce3e4293bbeb443485..45caa5d91dc753ea7b10f85f37b2c7ed3b01dae8 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -87,9 +87,9 @@ plug-in is running (see examples of Sections~\ref{sec:no-main} and
The instrumentation in the generated program is partial for every program
without main containing memory-related annotations, except if the option
-\optionuse{-}{e-acsl-full-mmodel} or the \eacsl plug-in (of \shortopt{M} option
-of \eacslgcc) is provided. In that case, violations of such annotations are
-undetected.
+\optionuse{-}{e-acsl-full-mtracking} or the \eacsl plug-in (of \shortopt{M}
+option of \eacslgcc) is provided. In that case, violations of such annotations
+are undetected.
Consider the following example.
@@ -144,7 +144,7 @@ instrumented code (linked against this main) could print some warnings from the
\index{Function!Undefined}
The instrumentation in the generated program is partial for a program $p$ if $p$
-contains a memory-related annotation $a$ and an undefined function
+contains a memory-related annotation $a$ and an undefined function
$f$ such that:
\begin{itemize}
\item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index accd222ac1c299c54589bc2c69647b8855ab3ec6..f9dedfdf86881ca09adbaa043b83b45d4bb5087a 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -550,7 +550,7 @@ this means that
is, however, still possible to systematically instrument the code for handling
potential memory-related annotations even when it is not required. This
feature can be enabled using the \shortopt{M} switch of \eacslgcc or
-\shortopt{e-acsl-full-mmodel} option of the \eacsl plug-in.
+\shortopt{e-acsl-full-mtracking} option of the \eacsl plug-in.
\begin{important}
The above-mentioned static analysis is probably the less robust part of \eacsl
diff --git a/src/plugins/e-acsl/examples/known_bugs/let-alias.c b/src/plugins/e-acsl/examples/known_bugs/let-alias.c
index 25af1ec3080abc2de0e9850d8d478a7617aa7488..8529a4461186a5715ee39f30c252c1a5409f428e 100644
--- a/src/plugins/e-acsl/examples/known_bugs/let-alias.c
+++ b/src/plugins/e-acsl/examples/known_bugs/let-alias.c
@@ -2,7 +2,7 @@
DONTRUN:
*/
-/* let binding on alias: only work with -e-acsl-full-mmodel;
+/* let binding on alias: only work with -e-acsl-full-mtracking;
should not be the case. */
int main(void) {
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/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index e4c6801d21f29c194931cca19852edad9f241f9f..39e15364d47e040dab2ff1715b5a31109a079ed7 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -99,7 +99,7 @@ pass additional arguments to the \fBFrama-C\fP pre-processor.
.B -L, --frama-c-stdlib
use the \fBFrama-C\fP standard library instead of a system-wide one.
.TP
-.B -M, --full-mmodel
+.B -M, --full-mtracking
maximize memory-related instrumentation.
.TP
.B --temporal
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index 4e075e196a591c2729f55a6152d52ade99430459..b05f8fe127e674e8d15bae4d8787f5c43fc8b0c4 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -3,7 +3,7 @@
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2012-2018 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
+# CEA (Commissariat � l'�nergie atomique et aux �nergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
@@ -39,7 +39,7 @@ _eacsl_gcc() {
--frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model=
--e-acsl-extra=
--compile --compile-only --print-mmodels --frama-c-only --instrumented-only
- --gmp --full-mmodel --rte= --rte-select= --no-int-overflow
+ --gmp --full-mtracking --rte= --rte-select= --no-int-overflow
--no-stdlib --frama-c-stdlib --libc-replacements
--temporal --free-valid-address --weak-validity --validate-format-strings
--heap-size --stack-size"
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index c81e38218fb5c94dd3c75e247668f17b12f8e554..fe84dce4a7fd578c342bc564dcb4f41bdabdbcfd 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -32,6 +32,11 @@ error () {
fi
}
+# Print a warning message to STDERR.
+warning () {
+ echo "e-acsl-gcc: warning: $1" 1>&2
+}
+
# Check if a given executable name can be found by in the PATH
has_tool() {
which "$@" >/dev/null 2>&1 && return 0 || return 1
@@ -264,8 +269,8 @@ check_getopt;
# Getopt options
LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
- frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
- ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,keep-going,
+ frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,full-mtracking,gmp,
+ quiet,logfile:,ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,keep-going,
frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,
print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:,check,fail-with-code:,
temporal,weak-validity,stack-size:,heap-size:,rt-verbose,free-valid-address,
@@ -292,7 +297,7 @@ OPTION_OUTPUT_EXEC="a.out" # Generated executable name
OPTION_EACSL_OUTPUT_EXEC="" # Name of E-ACSL executable
OPTION_EACSL="-e-acsl" # Specifies E-ACSL run
OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
-OPTION_FULL_MMODEL= # Instrument as much as possible
+OPTION_FULL_MTRACKING= # Instrument as much as possible
OPTION_GMP= # Use GMP integers everywhere
OPTION_EACSL_MMODELS="segment" # Memory model used
OPTION_EACSL_SHARE= # Custom E-ACSL share directory
@@ -489,9 +494,13 @@ do
OPTION_FRAMA_STDLIB="-frama-c-stdlib"
;;
# Use as much memory-related instrumentation as possible
- -M|--full-mmodel)
+ -M|--full-mtracking|--full-mmodel)
+ if [ "$i" = "--full-mmodel" ]; then
+ warning "--full-mmodel is a deprecated alias for option --full-mtracking."
+ warning "Please use --full-mtracking instead."
+ fi
shift;
- OPTION_FULL_MMODEL="-e-acsl-full-mmodel"
+ OPTION_FULL_MTRACKING="-e-acsl-full-mtracking"
;;
# Use GMP everywhere
-g|--gmp)
@@ -780,7 +789,7 @@ if [ -n "$OPTION_EACSL" ]; then
$OPTION_EACSL
$OPTION_GMP
$OPTION_LIBC_REPLACEMENTS
- $OPTION_FULL_MMODEL
+ $OPTION_FULL_MTRACKING
$OPTION_TEMPORAL
$OPTION_VERBOSE
$OPTION_DEBUG
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
similarity index 97%
rename from src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
rename to src/plugins/e-acsl/src/analyses/memory_tracking.ml
index db85a8c4c96a1d183f0b84ae424531901996fb3d..e6225e41ed096b071d4f5ebd2068177bad27c632 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -692,7 +692,7 @@ end = struct
end
-let consolidated_must_model_vi vi =
+let consolidated_must_monitor_vi vi =
if Env.is_consolidated () then
Env.consolidated_mem vi
else begin
@@ -713,7 +713,7 @@ let consolidated_must_model_vi vi =
Env.consolidated_mem vi
end
-let must_model_vi ?kf ?stmt vi =
+let must_monitor_vi ?kf ?stmt vi =
let _kf = match kf, stmt with
| None, None | Some _, _ -> kf
| None, Some stmt -> Some (Kernel_function.find_englobing_kf stmt)
@@ -721,14 +721,14 @@ let must_model_vi ?kf ?stmt vi =
(* [JS 2013/05/07] that is unsound to take the env from the given stmt in
presence of aliasing with an address (see tests address.i).
TODO: could be optimized though *)
- consolidated_must_model_vi vi
+ consolidated_must_monitor_vi vi
(* match stmt, kf with
- | None, _ -> consolidated_must_model_vi vi
+ | None, _ -> consolidated_must_monitor_vi vi
| Some _, None ->
assert false
| Some stmt, Some kf ->
if not (Env.is_consolidated ()) then
- ignore (consolidated_must_model_vi vi);
+ ignore (consolidated_must_monitor_vi vi);
try
let tbl = Env.find kf in
try
@@ -736,7 +736,7 @@ let must_model_vi ?kf ?stmt vi =
Varinfo.Hptset.mem vi (Env.default_varinfos set)
with Not_found ->
(* new statement *)
- consolidated_must_model_vi vi
+ consolidated_must_monitor_vi vi
with Not_found ->
(* [kf] is dead code *)
false
@@ -761,8 +761,8 @@ and apply_on_vi_base_from_exp f ?kf ?stmt e = match e.enode with
| UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
Options.fatal "[pre_analysis] unexpected expression %a" Exp.pretty e
-let must_model_lval = apply_on_vi_base_from_lval must_model_vi
-let must_model_exp = apply_on_vi_base_from_exp must_model_vi
+let must_monitor_lval = apply_on_vi_base_from_lval must_monitor_vi
+let must_monitor_exp = apply_on_vi_base_from_exp must_monitor_vi
let must_never_monitor_lval ?kf ?stmt lv =
apply_on_vi_base_from_lval
@@ -782,27 +782,27 @@ let must_never_monitor_exp ?kf ?stmt lv =
(** {1 Public API} *)
(* ************************************************************************** *)
-let must_model_vi ?kf ?stmt vi =
+let must_monitor_vi ?kf ?stmt vi =
not (must_never_monitor vi)
&&
- (Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
+ (Options.Full_mtracking.get ()
+ || Error.generic_handle (must_monitor_vi ?kf ?stmt) false vi)
-let must_model_lval ?kf ?stmt lv =
+let must_monitor_lval ?kf ?stmt lv =
not (must_never_monitor_lval ?kf ?stmt lv)
&&
- (Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_lval ?kf ?stmt) false lv)
+ (Options.Full_mtracking.get ()
+ || Error.generic_handle (must_monitor_lval ?kf ?stmt) false lv)
-let must_model_exp ?kf ?stmt exp =
+let must_monitor_exp ?kf ?stmt exp =
not (must_never_monitor_exp ?kf ?stmt exp)
&&
- (Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_exp ?kf ?stmt) false exp)
+ (Options.Full_mtracking.get ()
+ || Error.generic_handle (must_monitor_exp ?kf ?stmt) false exp)
-let use_model () =
+let use_monitoring () =
not (Env.is_empty ())
- || Options.Full_mmodel.get ()
+ || Options.Full_mtracking.get ()
|| Env.has_heap_allocations ()
(*
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
similarity index 90%
rename from src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
rename to src/plugins/e-acsl/src/analyses/memory_tracking.mli
index 8c4967c2797f9c936b3c230b40a9cb0d476f6a37..07121a82a8e8bf5fefee8d8785d6efe93e0dfee2 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
@@ -28,18 +28,18 @@ open Cil_types
val reset: unit -> unit
(** Must be called to redo the analysis *)
-val use_model: unit -> bool
+val use_monitoring: unit -> bool
(** Is one variable monitored (at least)? *)
-val must_model_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
+val must_monitor_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
(** [must_model_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
[stmt] in the given function [kf] must be tracked by the memory model
library. *)
-val must_model_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
+val must_monitor_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
(** Same as {!must_model_vi}, for left-values *)
-val must_model_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
+val must_monitor_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
(** Same as {!must_model_vi}, for expressions *)
(*
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/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
similarity index 100%
rename from src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
rename to src/plugins/e-acsl/src/code_generator/memory_translate.ml
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.mli b/src/plugins/e-acsl/src/code_generator/memory_translate.mli
similarity index 100%
rename from src/plugins/e-acsl/src/code_generator/mmodel_translate.mli
rename to src/plugins/e-acsl/src/code_generator/memory_translate.mli
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
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 8c98ca1657933ca519eef73fa5697877efa50842..932ff7ea662055bb9bc6a51c4aff786fa7fce132 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -85,12 +85,13 @@ module Replace_libc_functions =
RTL alternatives"
end)
-module Full_mmodel =
+module Full_mtracking =
False
(struct
- let option_name = "-e-acsl-full-mmodel"
+ let option_name = "-e-acsl-full-mtracking"
let help = "maximal memory-related instrumentation"
end)
+let () = Full_mtracking.add_aliases ~deprecated:true [ "-e-acsl-full-mmodel" ]
module Builtins =
String_set
@@ -142,7 +143,7 @@ let () = Cmdline.run_after_configuring_stage version
let parameter_states =
[ Valid.self;
Gmp_only.self;
- Full_mmodel.self;
+ Full_mtracking.self;
Builtins.self;
Temporal_validity.self;
Validate_format_strings.self;
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index d5065c6a51dbbade2b491b5cf91fea75d17e7f23..ca303e1b515642f0e7155dd195ebc6a5f62e929a 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -25,7 +25,7 @@ include Plugin.S (** implementation of Log.S for E-ACSL *)
module Run: Parameter_sig.Bool
module Valid: Parameter_sig.Bool
module Gmp_only: Parameter_sig.Bool
-module Full_mmodel: Parameter_sig.Bool
+module Full_mtracking: Parameter_sig.Bool
module Project_name: Parameter_sig.String
module Builtins: Parameter_sig.String_set
module Temporal_validity: Parameter_sig.Bool
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c
index cc7640adddb94706ecf2548920699787ef11bf14..74b8476fdbf9b0c8e72eb96819d1157615fe6229 100644
--- a/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c
@@ -1,7 +1,7 @@
/* run.config_ci
COMMENT: frama-c/e-acsl#91, test for misplaced delete_block of local variable
in switch.
- STDOPT: #"-e-acsl-full-mmodel"
+ STDOPT: #"-e-acsl-full-mtracking"
*/
short a;
char b()
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
index 65de4748913a53fdc6a72a2215c32950353f5e66..636b97b921455af4ec13f54c6034decf21ba3975 100644
--- a/src/plugins/e-acsl/tests/format/test_config_dev
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -1,2 +1,2 @@
-MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mmodel
+MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking
MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config_ci b/src/plugins/e-acsl/tests/full-mmodel/test_config_ci
deleted file mode 100644
index 82cdcaaa69d16cc0e2427322763c59b35a07268b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/test_config_ci
+++ /dev/null
@@ -1 +0,0 @@
-STDOPT: #"-e-acsl-full-mmodel"
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config_dev b/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
deleted file mode 100644
index 840cd7e754b9378cae50629afe67859770850cbb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
+++ /dev/null
@@ -1 +0,0 @@
-MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mmodel
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/full-mmodel/README.md b/src/plugins/e-acsl/tests/full-mtracking/README.md
similarity index 87%
rename from src/plugins/e-acsl/tests/full-mmodel/README.md
rename to src/plugins/e-acsl/tests/full-mtracking/README.md
index 9e2bd153f80c9ad4ef7ffcb5754a14f665378aa7..6d17198369ac5aeb59a99b9d9ed37d83ac37f2fe 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/README.md
+++ b/src/plugins/e-acsl/tests/full-mtracking/README.md
@@ -1 +1 @@
-Like runtime, but also test instrumentation with --e-acsl-full-mmodel
+Like runtime, but also test instrumentation with --e-acsl-full-mtracking
diff --git a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i b/src/plugins/e-acsl/tests/full-mtracking/addrOf.i
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/addrOf.i
rename to src/plugins/e-acsl/tests/full-mtracking/addrOf.i
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/addrOf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.res.oracle
rename to src/plugins/e-acsl/tests/full-mtracking/oracle_ci/addrOf.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
similarity index 92%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
rename to src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
index 574d904ff3e9f01ffb34f47c1945664f8330ef7b..29818eff2cf2dafc7083b67ccf5598d9293b70dd 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
@@ -19,7 +19,7 @@ void f(void)
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,"Assertion","f",
- "\\initialized(p)","tests/full-mmodel/addrOf.i",10);
+ "\\initialized(p)","tests/full-mtracking/addrOf.i",10);
}
/*@ assert \initialized(p); */ ;
__e_acsl_delete_block((void *)(& p));
@@ -55,7 +55,7 @@ int main(void)
__e_acsl_full_init((void *)(& x));
f();
__e_acsl_assert(& x == & x,"Assertion","main","&x == &x",
- "tests/full-mmodel/addrOf.i",16);
+ "tests/full-mtracking/addrOf.i",16);
/*@ assert &x ≡ &x; */ ;
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.e-acsl.err.log b/src/plugins/e-acsl/tests/full-mtracking/oracle_dev/addrOf.e-acsl.err.log
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.e-acsl.err.log
rename to src/plugins/e-acsl/tests/full-mtracking/oracle_dev/addrOf.e-acsl.err.log
diff --git a/src/plugins/e-acsl/tests/full-mtracking/test_config_ci b/src/plugins/e-acsl/tests/full-mtracking/test_config_ci
new file mode 100644
index 0000000000000000000000000000000000000000..3b1ebb8a3ac607fb5b6543b24baedd44f3d1cbd4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mtracking/test_config_ci
@@ -0,0 +1 @@
+STDOPT: #"-e-acsl-full-mtracking"
diff --git a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev
new file mode 100644
index 0000000000000000000000000000000000000000..bdb600fef3fe5c8ec148408a9a4207cfb5bf1239
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev
@@ -0,0 +1 @@
+MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking
\ No newline at end of file