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/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/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