diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 7178eea308baa39f99a9b24256212fe49a9e5d13..b9e34c5015cb39aed04e9a6ea38d14108cebe7e1 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -253,6 +253,11 @@ type option_setting =
| Int of (int -> unit)
| String of (string -> unit)
+let option_setting_and_warn warn = function
+ | Unit f -> Unit (fun () -> warn (); f ())
+ | Int f -> Int (fun i -> warn (); f i)
+ | String f -> String (fun s -> warn (); f s)
+
exception Cannot_parse of string * string
let raise_error name because = raise (Cannot_parse(name, because))
@@ -436,7 +441,8 @@ module Plugin: sig
val add_group: ?memo:bool -> plugin:string -> string -> string * bool
val add_option: string -> group:string -> cmdline_option -> unit
val add_aliases:
- orig:string -> string -> group:string -> string list -> cmdline_option list
+ orig:string -> string -> group:string -> ?visible:bool -> ?deprecated:bool
+ -> string list -> cmdline_option list
val replace_option_setting:
string -> plugin:string -> group:string -> option_setting -> unit
val replace_option_help:
@@ -525,7 +531,7 @@ end = struct
(* table name_of_the_original_option --> aliases *)
let aliases_tbl = Hashtbl.create 7
- let add_aliases ~orig shortname ~group names =
+ let add_aliases ~orig shortname ~group ?(visible=true) ?(deprecated=false) names =
(* mostly inline [add_option] and perform additional actions *)
let options_group = find_group shortname group in
let option = List.find (fun o -> o.oname = orig) !options_group in
@@ -533,7 +539,19 @@ end = struct
if name = "" then invalid_arg "empty alias name";
Hashtbl.replace all_options name option;
Option_names.add name true;
- let alias = { option with oname = name } in
+ let setting =
+ if deprecated
+ then
+ let warn () =
+ Kernel_log.warning ~once:true
+ "@[%s is@ a deprecated alias@ for option %s.@ \
+ Please use %s instead.@]"
+ name option.oname option.oname
+ in
+ option_setting_and_warn warn option.setting
+ else option.setting
+ in
+ let alias = { option with oname = name; ovisible = visible; setting; } in
options_group := alias :: !options_group;
alias
in
@@ -723,8 +741,8 @@ let add_option_without_action
ohelp = help; ext_help = ext_help; ovisible = visible;
setting = Unit (fun () -> assert false) }
-let add_aliases orig ~plugin ~group stage aliases =
- let l = Plugin.add_aliases ~orig plugin ~group aliases in
+let add_aliases orig ~plugin ~group ?visible ?deprecated stage aliases =
+ let l = Plugin.add_aliases ~orig plugin ~group ?visible ?deprecated aliases in
let add = match stage with
| Early -> Early_Stage.add_for_parsing
| Extending -> Extending_Stage.add_for_parsing
@@ -899,7 +917,8 @@ let low_print_option_help fmt print_invisible o =
print_helpline fmt (name ^ ty) o.ohelp o.ext_help;
List.iter
(fun o ->
- print_helpline fmt (o.oname ^ ty) ("alias for option " ^ name) "")
+ if print_invisible || o.ovisible then
+ print_helpline fmt (o.oname ^ ty) ("alias for option " ^ name) "")
(Plugin.find_option_aliases o)
end;
true
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index b3eda2c34f96f9ace1ebe4bac1372807ef829d21..025cb25859989a8d7aaf8889f1ad4ae3d0c8ea16 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -313,13 +313,18 @@ val add_aliases:
string ->
plugin:string ->
group:Group.t ->
+ ?visible: bool ->
+ ?deprecated: bool ->
stage ->
string list ->
unit
(** [add_aliases orig plugin group aliases] adds a list of aliases to the given
option name [orig].
+ If [visible] is set to false, the aliases do not appear in help messages.
+ If [deprecated] is set to true, the use of the aliases emits a warning.
@Invalid_argument if an alias name is the empty string
- @since Carbon-20110201 *)
+ @since Carbon-20110201
+ @modify Frama-c+dev add [visible] and [deprecated] arguments. *)
val replace_option_setting:
string -> plugin:string -> group:Group.t -> option_setting -> unit
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 533be6968e7c37f0b8e0eb30919a465623537770..5675500ced75e97c56b01bcc5e0cf583f2798f12 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -223,14 +223,15 @@ struct
~plugin X.option_name Typed_parameter.ty ~journalize:false p
else p
- let add_aliases list =
- add_aliases list;
+ let add_aliases ?visible ?deprecated list =
+ add_aliases ?visible ?deprecated list;
match !negative_option_ref with
| None -> ()
| Some negative_option ->
let negative_list = List.map negate_name list in
let plugin = P.shortname in
- Cmdline.add_aliases negative_option ~plugin ~group stage negative_list
+ Cmdline.add_aliases
+ negative_option ~plugin ~group ?visible ?deprecated stage negative_list
end
@@ -1719,8 +1720,8 @@ struct
f ();
end
- let add_aliases list =
- add_aliases list;
+ let add_aliases ?visible ?deprecated list =
+ add_aliases ?visible ?deprecated list;
Output.add_aliases (List.map (fun alias -> alias ^ "-print") list)
end
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 9ab4f1cca7e940a4f2b0cc4ca127f70c19a78f68..89a439f71b324967ac4c0775bf8eaf4587a86af8 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -179,10 +179,13 @@ module type S_no_parameter = sig
val equal: t -> t -> bool
- val add_aliases: string list -> unit
+ val add_aliases: ?visible: bool -> ?deprecated:bool -> string list -> unit
(** Add some aliases for this option. That is other option names which have
exactly the same semantics that the initial option.
- @raise Invalid_argument if one of the strings is empty *)
+ If [visible] is set to false, the aliases do not appear in help messages.
+ If [deprecated] is set to true, the use of the aliases emits a warning.
+ @raise Invalid_argument if one of the strings is empty
+ @modify Frama-c+dev add [visible] and [deprecated] arguments. *)
(**/**)
val is_set: unit -> bool
diff --git a/src/kernel_services/cmdline_parameters/parameter_state.ml b/src/kernel_services/cmdline_parameters/parameter_state.ml
index a61ea576898dec21a9e3a700a6231b9967de394e..8941eec275878ca1c8a2910fbc536089dd161f2a 100644
--- a/src/kernel_services/cmdline_parameters/parameter_state.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_state.ml
@@ -270,8 +270,9 @@ struct
let option_name = X.option_name
- let add_aliases =
- Cmdline.add_aliases option_name ~plugin:P.shortname ~group stage
+ let add_aliases ?visible ?deprecated =
+ Cmdline.add_aliases
+ option_name ~plugin:P.shortname ~group stage ?visible ?deprecated
let print_help fmt =
Cmdline.print_option_help fmt ~plugin:P.shortname ~group option_name
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 06ec07489dc851480fc9b9964637474f4ba26b4c..067694ad12cb107d320981e31c57ea563506903a 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -44,7 +44,8 @@ module type S_no_log = sig
module Config: Parameter_sig.Specific_dir
val help: Cmdline.Group.t
val messages: Cmdline.Group.t
- val add_plugin_output_aliases: string list -> unit
+ val add_plugin_output_aliases:
+ ?visible:bool -> ?deprecated:bool -> string list -> unit
end
module type S = sig
@@ -795,14 +796,14 @@ struct
let is_kernel = is_kernel () in
Warn_category.add_set_hook (parse_warn_directives is_kernel)
- let add_plugin_output_aliases aliases =
+ let add_plugin_output_aliases ?visible ?deprecated aliases =
let aliases = List.filter (fun alias -> alias <> "") aliases in
let optname suffix = List.map (fun alias -> "-" ^ alias ^ suffix) aliases in
- Help.add_aliases (optname "-help");
- Verbose.add_aliases (optname "-verbose");
- Debug_category.add_aliases (optname "-msg-key");
- Warn_category.add_aliases (optname "-warn-key");
- LogToFile.add_aliases (optname "-log")
+ Help.add_aliases ?visible ?deprecated (optname "-help");
+ Verbose.add_aliases ?visible ?deprecated (optname "-verbose");
+ Debug_category.add_aliases ?visible ?deprecated (optname "-msg-key");
+ Warn_category.add_aliases ?visible ?deprecated (optname "-warn-key");
+ LogToFile.add_aliases ?visible ?deprecated (optname "-log")
let () = reset_plugin ()
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index a5e41ee354ec50753ba9200ccb84281524757210..16c14c026ae910efbfd982597627c683983bf5ba 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -64,12 +64,14 @@ module type S_no_log = sig
(** The group containing options -*-debug and -*-verbose.
@since Boron-20100401 *)
- val add_plugin_output_aliases: string list -> unit
- (** Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log,
- -plugin-msg-key, and -plugin-warn-key.
- [add_plugin_output_aliases [alias]] adds the aliases -alias-help,
- -alias-verbose, etc.
- @since 18.0-Argon *)
+ val add_plugin_output_aliases:
+ ?visible:bool -> ?deprecated:bool -> string list -> unit
+ (** Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log,
+ -plugin-msg-key, and -plugin-warn-key.
+ [add_plugin_output_aliases [alias]] adds the aliases -alias-help,
+ -alias-verbose, etc.
+ @since 18.0-Argon
+ @modify Frama-c+dev add [visible] and [deprecated] arguments. *)
end
(** Provided plug-general services for plug-ins.
diff --git a/src/plugins/e-acsl/tests/arith/array.i b/src/plugins/e-acsl/tests/arith/array.i
index 192094bfbdee5042d17c0e6225eb70a1cc87cbf1..4ef7b8e882fb2b7aa57e48eb425b5436fd70349b 100644
--- a/src/plugins/e-acsl/tests/arith/array.i
+++ b/src/plugins/e-acsl/tests/arith/array.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: arrays
- STDOPT: #"-slevel 5"
+ STDOPT: #"-eva-slevel 5"
*/
int T1[3],T2[4];
@@ -113,4 +113,4 @@ int main(void) {
vlas(3);
return 0;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/e-acsl/tests/constructs/invariant.i b/src/plugins/e-acsl/tests/constructs/invariant.i
index 76cbdb63c7169236217d0cb3a519aea09562eafd..8bc1eeee091a422a69c6b9ad3d8f2454f1b6e7c8 100644
--- a/src/plugins/e-acsl/tests/constructs/invariant.i
+++ b/src/plugins/e-acsl/tests/constructs/invariant.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: invariant
- STDOPT: +"-slevel 11"
+ STDOPT: +"-eva-slevel 11"
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/constructs/loop.i b/src/plugins/e-acsl/tests/constructs/loop.i
index 4b0b3193ee1d889a17180daf26e085cd7a67cd0c..bbab3b09f21b67d29a1dda970db34f0b93f9f35b 100644
--- a/src/plugins/e-acsl/tests/constructs/loop.i
+++ b/src/plugins/e-acsl/tests/constructs/loop.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: loop invariants
- STDOPT: +"-slevel 160"
+ STDOPT: +"-eva-slevel 160"
*/
void simple_loop() {
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/with_value.i b/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
index b147374aa576d736dc929426f708f2517ac1377e..b030fa5e58dbcbe8a8d388fcc49097265f53ec38 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
+++ b/src/plugins/loop_analysis/tests/loop_analysis/with_value.i
@@ -1,5 +1,5 @@
/*run.config
-OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -val -val-show-progress -then -loop
+OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -eva -eva-show-progress -then -loop
*/
void f1(int n) {
diff --git a/src/plugins/nonterm/tests/nonterm/builtin_termination.c b/src/plugins/nonterm/tests/nonterm/builtin_termination.c
index 514e4202b09dcbed1e566fe0dd3d9ad6259937fe..dff850dc8ae96f040640768d57556b09b73aeedb 100644
--- a/src/plugins/nonterm/tests/nonterm/builtin_termination.c
+++ b/src/plugins/nonterm/tests/nonterm/builtin_termination.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-val-builtin strlen:Frama_C_strlen"
+ STDOPT: #"-eva-builtin strlen:Frama_C_strlen"
*/
#include <string.h>
diff --git a/src/plugins/nonterm/tests/nonterm/n6.c b/src/plugins/nonterm/tests/nonterm/n6.c
index 1e4af5d6d67b75e8bb8b4124e1bda8e552a45444..e75e048ec1fc1ff024374bca11425471f09bc9f3 100644
--- a/src/plugins/nonterm/tests/nonterm/n6.c
+++ b/src/plugins/nonterm/tests/nonterm/n6.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-val-builtin memcpy:Frama_C_memcpy"
+ STDOPT: #"-eva-builtin memcpy:Frama_C_memcpy"
*/
#include <string.h>
diff --git a/src/plugins/nonterm/tests/test_config b/src/plugins/nonterm/tests/test_config
index 1d678ae3e1a635f06f7c8fbf7e30a0da5d6f7ffe..91f0e5ec1ff948b34ba561fc9d7369be7fd38b87 100644
--- a/src/plugins/nonterm/tests/test_config
+++ b/src/plugins/nonterm/tests/test_config
@@ -1 +1 @@
-OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -val -val-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
+OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
diff --git a/src/plugins/report/tests/report/csv.c b/src/plugins/report/tests/report/csv.c
index 3bd7c80288ace2904e9724cdcea46b67ba38123c..536cfb432f2702af8035011868cad8ee785095d9 100644
--- a/src/plugins/report/tests/report/csv.c
+++ b/src/plugins/report/tests/report/csv.c
@@ -1,6 +1,6 @@
/* run.config
LOG: csv.csv
- OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -slevel 1
+ OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart
*/
volatile v;
diff --git a/src/plugins/studia/tests/test_config b/src/plugins/studia/tests/test_config
index 0875cfb7318e90da7861ddc6596bba50d8040b3d..dc79c97068c8125cbff6a916b7fed6d7b881d5f2 100644
--- a/src/plugins/studia/tests/test_config
+++ b/src/plugins/studia/tests/test_config
@@ -1 +1 @@
-OPT: -val -journal-disable -out -input -deps
+OPT: -eva -journal-disable -out -input -deps
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 38dedbe7db7a8ebfdc5589d3a4a4e190d957c579..67d4ce541f13af42b3fdf814fb3de7554a8ca573 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -64,8 +64,8 @@ include Plugin.Register
"automatically computes variation domains for the variables of the program"
end)
-let () = Help.add_aliases [ "-value-h"; "-val-h" ]
-let () = add_plugin_output_aliases [ "value" ]
+let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ]
+let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ]
(* Debug categories. *)
let dkey_initial_state = register_category "initial-state"
@@ -109,7 +109,7 @@ module ForceValues =
let help = "Compute values"
let output_by_default = true
end)
-let () = ForceValues.add_aliases ["-val"]
+let () = ForceValues.add_aliases ~deprecated:true ["-val"]
let domains = add_group "Abstract Domains"
let precision_tuning = add_group "Precision vs. time"
@@ -373,7 +373,6 @@ module NoResultsFunctions =
function f"
end)
let () = add_dep NoResultsFunctions.parameter
-let () = NoResultsFunctions.add_aliases ["-no-results-function"]
let () = Parameter_customize.set_group performance
module ResultsAll =
@@ -383,7 +382,6 @@ module ResultsAll =
let help = "Record values for each of the statements of the program."
end)
let () = add_dep ResultsAll.parameter
-let () = ResultsAll.add_aliases ["-results"]
let () = Parameter_customize.set_group performance
module JoinResults =
@@ -393,7 +391,6 @@ module JoinResults =
let help = "Precompute consolidated states once Eva is computed"
let default = true
end)
-let () = JoinResults.add_aliases ["-val-join-results"]
let () = Parameter_customize.set_group performance
module EqualityStorage =
@@ -463,7 +460,6 @@ module AllRoundingModesConstants =
or being converted to higher precision"
end)
let () = add_correctness_dep AllRoundingModesConstants.parameter
-let () = AllRoundingModesConstants.add_aliases ["-all-rounding-modes-constants"]
let () = Parameter_customize.set_group alarms
module UndefinedPointerComparisonPropagateAll =
@@ -475,9 +471,6 @@ module UndefinedPointerComparisonPropagateAll =
the emission of an alarm"
end)
let () = add_correctness_dep UndefinedPointerComparisonPropagateAll.parameter
-let () =
- UndefinedPointerComparisonPropagateAll.add_aliases
- ["-undefined-pointer-comparison-propagate-all"]
let () = Parameter_customize.set_group alarms
module WarnPointerComparison =
@@ -491,24 +484,6 @@ module WarnPointerComparison =
end)
let () = WarnPointerComparison.set_possible_values ["all"; "pointer"; "none"]
let () = add_correctness_dep WarnPointerComparison.parameter
-let () = WarnPointerComparison.add_aliases ["-val-warn-undefined-pointer-comparison"]
-
-
-let () = Parameter_customize.set_group alarms
-let () = Parameter_customize.is_invisible ()
-module WarnLeftShiftNegative =
- True
- (struct
- let option_name = "-val-warn-left-shift-negative"
- let help =
- "Emit alarms when left-shifting negative integers"
- end)
-let () = add_correctness_dep WarnLeftShiftNegative.parameter
-let () = WarnLeftShiftNegative.add_update_hook
- (fun _ v ->
- warning "This option is deprecated. Use %s instead"
- Kernel.LeftShiftNegative.name;
- Kernel.LeftShiftNegative.set v)
let () = Parameter_customize.set_group alarms
module WarnSignedConvertedDowncast =
@@ -521,9 +496,6 @@ module WarnSignedConvertedDowncast =
destination range."
end)
let () = add_correctness_dep WarnSignedConvertedDowncast.parameter
-let () =
- WarnSignedConvertedDowncast.add_aliases
- ["-val-warn-signed-converted-downcast"]
let () = Parameter_customize.set_group alarms
@@ -537,7 +509,6 @@ module WarnPointerSubstraction =
offsets. When unset, do not warn but generate imprecise offsets."
end)
let () = add_correctness_dep WarnPointerSubstraction.parameter
-let () = WarnPointerSubstraction.add_aliases ["-val-warn-pointer-subtraction"]
let () = Parameter_customize.set_group alarms
module IgnoreRecursiveCalls =
@@ -548,7 +519,6 @@ module IgnoreRecursiveCalls =
"Pretend function calls that would be recursive do not happen. Causes unsoundness"
end)
let () = add_correctness_dep IgnoreRecursiveCalls.parameter
-let () = IgnoreRecursiveCalls.add_aliases ["-val-ignore-recursive-calls"]
let () = Parameter_customize.set_group alarms
@@ -563,7 +533,6 @@ module WarnCopyIndeterminate =
functions by '=-@all'."
end)
let () = add_correctness_dep WarnCopyIndeterminate.parameter
-let () = WarnCopyIndeterminate.add_aliases ["-val-warn-copy-indeterminate"]
let () = WarnCopyIndeterminate.Category.(set_default (all ()))
let () = Parameter_customize.set_group alarms
@@ -575,7 +544,6 @@ module ReduceOnLogicAlarms =
emitted while the predicate is evaluated (experimental)"
end)
let () = add_correctness_dep ReduceOnLogicAlarms.parameter
-let () = ReduceOnLogicAlarms.add_aliases ["-val-reduce-on-logic-alarms"]
let () = Parameter_customize.set_group alarms
module InitializedLocals =
@@ -587,7 +555,6 @@ module InitializedLocals =
initialization."
end)
let () = add_correctness_dep InitializedLocals.parameter
-let () = InitializedLocals.add_aliases ["-val-initialized-locals"]
(* ------------------------------------------------------------------------- *)
(* --- Initial context --- *)
@@ -603,7 +570,6 @@ module AutomaticContextMaxDepth =
let help = "Use <n> as the depth of the default context for Eva. (defaults to 2)"
end)
let () = add_correctness_dep AutomaticContextMaxDepth.parameter
-let () = AutomaticContextMaxDepth.add_aliases ["-context-depth"]
let () = Parameter_customize.set_group initial_context
module AutomaticContextMaxWidth =
@@ -616,7 +582,6 @@ module AutomaticContextMaxWidth =
end)
let () = AutomaticContextMaxWidth.set_range ~min:1 ~max:max_int
let () = add_correctness_dep AutomaticContextMaxWidth.parameter
-let () = AutomaticContextMaxWidth.add_aliases ["-context-width"]
let () = Parameter_customize.set_group initial_context
module AllocatedContextValid =
@@ -627,7 +592,6 @@ module AllocatedContextValid =
and then use NULL (defaults to false)"
end)
let () = add_correctness_dep AllocatedContextValid.parameter
-let () = AllocatedContextValid.add_aliases ["-context-valid-pointers"]
let () = Parameter_customize.set_group initial_context
module InitializationPaddingGlobals =
@@ -643,7 +607,6 @@ module InitializationPaddingGlobals =
end)
let () = InitializationPaddingGlobals.set_possible_values ["yes"; "no"; "maybe"]
let () = add_correctness_dep InitializationPaddingGlobals.parameter
-let () = InitializationPaddingGlobals.add_aliases ["-val-initialization-padding-globals"]
(* ------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -691,7 +654,6 @@ module WideningDelay =
"Do not widen before the <n>-th iteration (defaults to 3)"
end)
let () = WideningDelay.set_range ~min:1 ~max:max_int
-let () = WideningDelay.add_aliases ["-wlevel"]
let () = add_precision_dep WideningDelay.parameter
let () = Parameter_customize.set_group precision_tuning
@@ -721,7 +683,6 @@ module SemanticUnrollingLevel =
(defaults to 0)"
end)
let () = add_precision_dep SemanticUnrollingLevel.parameter
-let () = SemanticUnrollingLevel.add_aliases ["-slevel"]
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
@@ -746,7 +707,6 @@ module SlevelFunction =
let default = Kernel_function.Map.empty
end)
let () = add_precision_dep SlevelFunction.parameter
-let () = SlevelFunction.add_aliases ["-slevel-function"]
let () = Parameter_customize.set_group precision_tuning
module SlevelMergeAfterLoop =
@@ -759,7 +719,6 @@ module SlevelMergeAfterLoop =
of a loop are merged before entering the next excution."
end)
let () = add_precision_dep SlevelMergeAfterLoop.parameter
-let () = SlevelMergeAfterLoop.add_aliases ["-val-slevel-merge-after-loop"]
let () = Parameter_customize.set_group precision_tuning
module MinLoopUnroll =
@@ -865,7 +824,6 @@ module SplitReturnFunction =
let default = Kernel_function.Map.empty
end)
let () = add_precision_dep SplitReturnFunction.parameter
-let () = SplitReturnFunction.add_aliases ["-val-split-return-function"]
let () = Parameter_customize.set_group precision_tuning
module SplitReturn =
@@ -893,7 +851,6 @@ let () =
abort "@[@[incorrect argument for option %s@ (%s).@]"
SplitReturn.name s))
let () = add_precision_dep SplitReturn.parameter
-let () = SplitReturn.add_aliases ["-val-split-return"]
(* --- Misc --- *)
@@ -910,7 +867,6 @@ module ILevel =
(defaults to 8, must be between 4 and 128)"
end)
let () = add_precision_dep ILevel.parameter
-let () = ILevel.add_aliases ["-val-ilevel"]
let () = ILevel.add_update_hook (fun _ i -> Int_set.set_small_cardinal i)
let () = ILevel.set_range 4 256
@@ -947,7 +903,6 @@ module BuiltinsOverrides =
let default = Kernel_function.Map.empty
end)
let () = add_precision_dep BuiltinsOverrides.parameter
-let () = BuiltinsOverrides.add_aliases ["-val-builtin"]
(* Exported in Eva.mli. *)
let use_builtin key name =
@@ -964,7 +919,6 @@ module BuiltinsAuto =
known C functions"
end)
let () = add_correctness_dep BuiltinsAuto.parameter
-let () = BuiltinsAuto.add_aliases ["-val-builtins-auto"]
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.set_negative_option_name ""
@@ -975,7 +929,6 @@ module BuiltinsList =
let help = "List existing builtins, and which functions they \
are automatically associated to (if any)"
end)
-let () = BuiltinsList.add_aliases ["-val-builtins-list"]
let () = Parameter_customize.set_group precision_tuning
module LinearLevel =
@@ -989,7 +942,6 @@ module LinearLevel =
Defaults to 0."
end)
let () = add_precision_dep LinearLevel.parameter
-let () = LinearLevel.add_aliases ["-val-subdivide-non-linear"]
let () = Parameter_customize.set_group precision_tuning
module LinearLevelFunction =
@@ -1026,7 +978,6 @@ module UsePrototype =
their definitions"
end)
let () = add_precision_dep UsePrototype.parameter
-let () = UsePrototype.add_aliases ["-val-use-spec"]
let () = Parameter_customize.set_group precision_tuning
module SkipLibcSpecs =
@@ -1037,7 +988,6 @@ module SkipLibcSpecs =
standard library of Frama-C, when their bodies are evaluated"
end)
let () = add_precision_dep SkipLibcSpecs.parameter
-let () = SkipLibcSpecs.add_aliases ["-val-skip-stdlib-specs"]
let () = Parameter_customize.set_group precision_tuning
@@ -1049,7 +999,6 @@ module RmAssert =
so that the user needs to inspect fewer of them"
end)
let () = add_precision_dep RmAssert.parameter
-let () = RmAssert.add_aliases ["-remove-redundant-alarms"]
let () = Parameter_customize.set_group precision_tuning
module MemExecAll =
@@ -1061,7 +1010,6 @@ module MemExecAll =
Callstacks for which the analysis has not been recomputed \
are incorrectly shown as dead in the GUI."
end)
-let () = MemExecAll.add_aliases ["-memexec-all"]
let () =
MemExecAll.add_set_hook
(fun _bold bnew ->
@@ -1084,7 +1032,6 @@ module ArrayPrecisionLevel =
less than n values. (defaults to 200)"
end)
let () = add_precision_dep ArrayPrecisionLevel.parameter
-let () = ArrayPrecisionLevel.add_aliases ["-plevel"]
let () = ArrayPrecisionLevel.add_update_hook
(fun _ v -> Offsetmap.set_plevel v)
@@ -1190,29 +1137,6 @@ module ValShowProgress =
let option_name = "-eva-show-progress"
let help = "Show progression messages during analysis"
end)
-let () = ValShowProgress.add_aliases ["-val-show-progress"]
-
-let () = Parameter_customize.set_group messages
-let () = Parameter_customize.is_invisible ()
-module ValShowInitialState =
- True
- (struct
- let option_name = "-val-show-initial-state"
- (* deprecated in Silicon *)
- let help = "[deprecated] Show initial state before analysis starts. \
- This option has been replaced by \
- -eva-msg-key=[-]initial-state and has no effect anymore."
- end)
-let () =
- ValShowInitialState.add_set_hook
- (fun _ new_ ->
- if new_ then
- Kernel.warning "@[Option -val-show-initial-state has no effect, \
- it has been replaced by -eva-msg-key=initial-state@]"
- else
- Kernel.warning "@[Option -no-val-show-initial-state has no effect, \
- it has been replaced by -eva-msg-key=-initial-state@]"
- )
let () = Parameter_customize.set_group messages
module ValShowPerf =
@@ -1221,7 +1145,6 @@ module ValShowPerf =
let option_name = "-eva-show-perf"
let help = "Compute and show a summary of the time spent analyzing function calls"
end)
-let () = ValShowPerf.add_aliases ["-val-show-perf"]
let () = Parameter_customize.set_group messages
module ValPerfFlamegraphs =
@@ -1234,7 +1157,6 @@ module ValPerfFlamegraphs =
let arg_name = "file"
let default = ""
end)
-let () = ValPerfFlamegraphs.add_aliases ["-val-flamegraph"]
let () = Parameter_customize.set_group messages
@@ -1246,7 +1168,6 @@ module ShowSlevel =
let arg_name = "n"
let help = "Period for showing consumption of the alloted slevel during analysis"
end)
-let () = ShowSlevel.add_aliases ["-val-show-slevel"]
let () = ShowSlevel.set_range ~min:1 ~max:max_int
let () = Parameter_customize.set_group messages
@@ -1256,35 +1177,6 @@ module PrintCallstacks =
let option_name = "-eva-print-callstacks"
let help = "When printing a message, also show the current call stack"
end)
-let () = PrintCallstacks.add_aliases ["-val-print-callstacks"]
-
-let () = Parameter_customize.set_group messages
-let () = Parameter_customize.is_invisible ()
-module AlarmsWarnings =
- True
- (struct
- let option_name = "-val-warn-on-alarms"
- let help = "[DEPRECATED: use warning key alarm to manage alarms] \
- If set (default), possible alarms are printed in \
- the analysis log as warnings, otherwise as plain feedback"
- end)
-
-let () =
- AlarmsWarnings.add_set_hook
- (fun _ f ->
- match get_warn_status wkey_alarm with
- | Log.Wabort | Log.Werror | Log.Werror_once ->
- warning "alarms already set to produce an error. \
- Ignoring -val-warn-on-alarms"
- | Log.Winactive | Log.Wactive | Log.Wfeedback ->
- set_warn_status wkey_alarm (if f then Log.Wactive else Log.Wfeedback)
- | Log.Wonce | Log.Wfeedback_once ->
- (* Keep the 'once' status. Note that this will only happen if user
- is mixing old and new style of warning management, thus it becomes
- difficult to interpret the desired action.
- *)
- set_warn_status wkey_alarm
- (if f then Log.Wonce else Log.Wfeedback_once))
let () = Parameter_customize.set_group messages
module ReportRedStatuses =
@@ -1322,36 +1214,6 @@ module InterpreterMode =
let help = "Stop at first call to a library function, if main() has \
arguments, on undecided branches"
end)
-let () = InterpreterMode.add_aliases ["-val-interpreter-mode"]
-
-let () = Parameter_customize.set_group interpreter
-let () = Parameter_customize.is_invisible ()
-module ObviouslyTerminatesFunctions =
- Fundec_set
- (struct
- let option_name = "-obviously-terminates-function"
- let arg_name = "f"
- let help = "deprecated"
- end)
-let () = add_dep ObviouslyTerminatesFunctions.parameter
-let () = ObviouslyTerminatesFunctions.add_update_hook
- (fun _ _ ->
- warning "Option -obviously-terminates-function is no longer supported. \
- Ignoring.")
-
-let () = Parameter_customize.set_group interpreter
-let () = Parameter_customize.is_invisible ()
-module ObviouslyTerminatesAll =
- False
- (struct
- let option_name = "-obviously-terminates"
- let help = "undocumented and deprecated"
- end)
-let () = add_dep ObviouslyTerminatesAll.parameter
-let () = ObviouslyTerminatesAll.add_update_hook
- (fun _ _ ->
- warning "Option -obviously-terminates is no longer supported. \
- Ignoring.")
let () = Parameter_customize.set_group interpreter
module StopAtNthAlarm =
@@ -1361,7 +1223,6 @@ module StopAtNthAlarm =
let arg_name = "n"
let help = "Abort the analysis when the nth alarm is emitted."
end)
-let () = StopAtNthAlarm.add_aliases ["-val-stop-at-nth-alarm"]
(* -------------------------------------------------------------------------- *)
(* --- Ugliness required for correctness --- *)
@@ -1465,7 +1326,6 @@ module AllocFunctions =
By default, contains malloc, calloc and realloc."
let default = Datatype.String.Set.of_list ["malloc"; "calloc"; "realloc"]
end)
-let () = AllocFunctions.add_aliases ["-val-malloc-functions"]
let () = AllocFunctions.add_aliases ["-eva-malloc-functions"]
let () = Parameter_customize.set_group malloc
@@ -1476,7 +1336,6 @@ module AllocReturnsNull=
let help = "Memory allocation built-ins (malloc, calloc, realloc) are \
modeled as nondeterministically returning a null pointer"
end)
-let () = AllocReturnsNull.add_aliases ["-val-alloc-returns-null"]
let () = Parameter_customize.set_group malloc
module MallocLevel =
@@ -1488,7 +1347,61 @@ module MallocLevel =
let help = "Set to [m] the number of precise dynamic allocations \
besides the initial one, for each callstack (defaults to 0)"
end)
-let () = MallocLevel.add_aliases ["-val-mlevel"]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Deprecated aliases --- *)
+(* -------------------------------------------------------------------------- *)
+
+let deprecated_aliases : ((module Parameter_sig.S) * string) list =
+ [ (module SemanticUnrollingLevel), "-slevel"
+ ; (module SlevelFunction), "-slevel-function"
+ ; (module NoResultsFunctions), "-no-results-function"
+ ; (module ResultsAll), "-results"
+ ; (module JoinResults), "-val-join-results"
+ ; (module AllRoundingModesConstants), "-all-rounding-modes-constants"
+ ; (module UndefinedPointerComparisonPropagateAll), "-undefined-pointer-comparison-propagate-all"
+ ; (module WarnPointerComparison), "-val-warn-undefined-pointer-comparison"
+ ; (module WarnSignedConvertedDowncast), "-val-warn-signed-converted-downcast"
+ ; (module WarnPointerSubstraction), "-val-warn-pointer-subtraction"
+ ; (module IgnoreRecursiveCalls), "-val-ignore-recursive-calls"
+ ; (module WarnCopyIndeterminate), "-val-warn-copy-indeterminate"
+ ; (module ReduceOnLogicAlarms), "-val-reduce-on-logic-alarms"
+ ; (module InitializedLocals), "-val-initialized-locals"
+ ; (module AutomaticContextMaxDepth), "-context-depth"
+ ; (module AutomaticContextMaxWidth), "-context-width"
+ ; (module AllocatedContextValid), "-context-valid-pointers"
+ ; (module InitializationPaddingGlobals), "-val-initialization-padding-globals"
+ ; (module WideningDelay), "-wlevel"
+ ; (module SlevelMergeAfterLoop), "-val-slevel-merge-after-loop"
+ ; (module SplitReturnFunction), "-val-split-return-function"
+ ; (module SplitReturn), "-val-split-return"
+ ; (module ILevel), "-val-ilevel"
+ ; (module BuiltinsOverrides), "-val-builtin"
+ ; (module BuiltinsAuto), "-val-builtins-auto"
+ ; (module BuiltinsList), "-val-builtins-list"
+ ; (module LinearLevel), "-val-subdivide-non-linear"
+ ; (module UsePrototype), "-val-use-spec"
+ ; (module SkipLibcSpecs), "-val-skip-stdlib-specs"
+ ; (module RmAssert), "-remove-redundant-alarms"
+ ; (module MemExecAll), "-memexec-all"
+ ; (module ArrayPrecisionLevel), "-plevel"
+ ; (module ValShowProgress), "-val-show-progress"
+ ; (module ValShowPerf), "-val-show-perf"
+ ; (module ValPerfFlamegraphs), "-val-flamegraph"
+ ; (module ShowSlevel), "-val-show-slevel"
+ ; (module PrintCallstacks), "-val-print-callstacks"
+ ; (module InterpreterMode), "-val-interpreter-mode"
+ ; (module StopAtNthAlarm), "-val-stop-at-nth-alarm"
+ ; (module AllocFunctions), "-val-malloc-functions"
+ ; (module AllocReturnsNull), "-val-alloc-returns-null"
+ ; (module MallocLevel), "-val-mlevel"
+ ]
+
+let add_deprecated_alias ((module P: Parameter_sig.S), name) =
+ P.add_aliases ~visible:false ~deprecated:true [name]
+
+let () = List.iter add_deprecated_alias deprecated_aliases
+
(* -------------------------------------------------------------------------- *)
(* --- Meta options --- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 495d7b1fa9a873b7736c2651944fe2a0f9843cf3..8e5d5161ad55a36f7c1a0aa95951030a81299bb3 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -131,12 +131,10 @@ module SplitReturnFunction:
module SplitGlobalStrategy: State_builder.Ref with type data = Split_strategy.t
module ValShowProgress: Parameter_sig.Bool
-module ValShowInitialState: Parameter_sig.Bool
module ValShowPerf: Parameter_sig.Bool
module ValPerfFlamegraphs: Parameter_sig.String
module ShowSlevel: Parameter_sig.Int
module PrintCallstacks: Parameter_sig.Bool
-module AlarmsWarnings: Parameter_sig.Bool
module ReportRedStatuses: Parameter_sig.String
module NumerorsLogFile: Parameter_sig.String
diff --git a/src/plugins/variadic/tests/defined/multiple-va_start.c b/src/plugins/variadic/tests/defined/multiple-va_start.c
index f10b950af4c838805aba204a01e12bd156170ff5..9a3ff2627482f4dafd5936536c0cca47f9c85bf0 100644
--- a/src/plugins/variadic/tests/defined/multiple-va_start.c
+++ b/src/plugins/variadic/tests/defined/multiple-va_start.c
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-no-val-alloc-returns-null"
+STDOPT: +"-eva-no-alloc-returns-null"
*/
diff --git a/src/plugins/variadic/tests/defined/va_copy.c b/src/plugins/variadic/tests/defined/va_copy.c
index 3ad479a98de2c3ca4ad8c618d41f9c81fd0ac54f..129708fa9f349eddef4af0f3f4c241ea17a7987a 100644
--- a/src/plugins/variadic/tests/defined/va_copy.c
+++ b/src/plugins/variadic/tests/defined/va_copy.c
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-no-val-alloc-returns-null"
+STDOPT: +"-eva-no-alloc-returns-null"
*/
diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config
index 9d83090791bf7d3f4f62b2e69990d30fefd28fc8..e076935b23463006f8f89ffcddb93f7f2748c691 100644
--- a/src/plugins/variadic/tests/test_config
+++ b/src/plugins/variadic/tests/test_config
@@ -1 +1 @@
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
diff --git a/tests/builtins/allocated.c b/tests/builtins/allocated.c
index b09b532881c9ef6a322b5ad7292035bbdfd3d66e..3015ea59f137e0993b6a6c5d782d1c38e07fb3c3 100644
--- a/tests/builtins/allocated.c
+++ b/tests/builtins/allocated.c
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: +"-slevel 1 -eva-mlevel 0"
- STDOPT: +"-slevel 999 -eva-alloc-builtin fresh"
+ STDOPT: +"-eva-slevel 1 -eva-mlevel 0"
+ STDOPT: +"-eva-slevel 999 -eva-alloc-builtin fresh"
*/
#define assert_bottom(exp) if (nondet) {exp; Frama_C_show_each_unreachable();}
diff --git a/tests/builtins/gcc_zero_length_array.c b/tests/builtins/gcc_zero_length_array.c
index b990a598b0e4f9c25888f70e5a482fa9dfc4757f..18d39c75f5f6b3902363c7cbff8fb3da2689e321 100644
--- a/tests/builtins/gcc_zero_length_array.c
+++ b/tests/builtins/gcc_zero_length_array.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-machdep gcc_x86_32 -eva-alloc-builtin fresh -slevel 11"
+ STDOPT: +"-machdep gcc_x86_32 -eva-alloc-builtin fresh -eva-slevel 11"
*/
#include <stdlib.h>
diff --git a/tests/builtins/linked_list.c b/tests/builtins/linked_list.c
index 8ae291e74744e1efa73304be82e7569309ae407f..dfa85bbfb98d8203d21c9e88aef1012bfc63a6f1 100644
--- a/tests/builtins/linked_list.c
+++ b/tests/builtins/linked_list.c
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: #"-load-module variadic -eva-no-builtins-auto"
- STDOPT: #"-load-module variadic -plevel 100 -big-ints-hex 257 -eva-no-builtins-auto"
- STDOPT: #"-load-module variadic -slevel 12 -big-ints-hex 257 -eva-no-builtins-auto"
+ STDOPT: #"-load-module variadic -eva-plevel 100 -big-ints-hex 257 -eva-no-builtins-auto"
+ STDOPT: #"-load-module variadic -eva-slevel 12 -big-ints-hex 257 -eva-no-builtins-auto"
*/
#include "__fc_define_size_t.h"
diff --git a/tests/builtins/malloc-deps.c b/tests/builtins/malloc-deps.c
index 312e2534df54f1c9d390c49abe5465673dc598cb..1bb43e5021c1eb4b3d88ff639219613a9f099871 100644
--- a/tests/builtins/malloc-deps.c
+++ b/tests/builtins/malloc-deps.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
+ OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -eva-slevel 5 -eva-msg-key malloc
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c
index d5a922355cef26fc4fd6fd482771381ce6dea6ba..8b2a9551ec09b64cec7500533acb4043d6d4df68 100644
--- a/tests/builtins/malloc-optimistic.c
+++ b/tests/builtins/malloc-optimistic.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-memexec"
+ STDOPT: +"-eva-slevel 30 -eva-slevel-merge-after-loop @all -eva-memexec"
*/
#include <stddef.h>
//@ assigns \result \from \nothing;
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index fb9377fa0041f543e133230dab5ca534fcc32b61..989d36b908624a16151ca3120929f4bce1961862 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0 -eva-alloc-builtin by_stack
+ OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -eva-mlevel 0 -eva-alloc-builtin by_stack
*/
#include <stdlib.h>
diff --git a/tests/builtins/malloc_multiple.c b/tests/builtins/malloc_multiple.c
index 6c807d486a22e8a16f05c7447c7342a1fe0d8f18..81e2a9cc9f717679e7e98ff2047b2c5360f23bdc 100644
--- a/tests/builtins/malloc_multiple.c
+++ b/tests/builtins/malloc_multiple.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -slevel 50 -eva-mlevel 5
+ OPT: -eva @EVA_CONFIG@ -eva-slevel 50 -eva-mlevel 5
*/
#include<stdlib.h>
#define MAX 10
diff --git a/tests/builtins/memcpy.c b/tests/builtins/memcpy.c
index 3b438a803377db9cfbd9a59047e0389b70807c0d..97d2feee02e28b3480fb59d201ccdef64954943e 100644
--- a/tests/builtins/memcpy.c
+++ b/tests/builtins/memcpy.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-calldeps -slevel-function init:2000 -eva-msg-key imprecision -plevel 150 -main main_all -inout -no-deps -absolute-valid-range 100000-100001 -then -load-module report -report"
+ STDOPT: +"-calldeps -eva-slevel-function init:2000 -eva-msg-key imprecision -eva-plevel 150 -main main_all -inout -no-deps -absolute-valid-range 100000-100001 -then -load-module report -report"
*/
#include "string.h"
diff --git a/tests/builtins/memset.c b/tests/builtins/memset.c
index 2cbdd6386c6b0dddcd8e89164c9bc57d1e9d6e1b..bb8f0dfe496fc13e55f5da853a8c84c7c4f858f1 100644
--- a/tests/builtins/memset.c
+++ b/tests/builtins/memset.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-calldeps -eva-msg-key imprecision -plevel 500" +"-inout -no-deps"
+ STDOPT: #"-calldeps -eva-msg-key imprecision -eva-plevel 500" +"-inout -no-deps"
*/
#include "string.h"
diff --git a/tests/builtins/realloc.c b/tests/builtins/realloc.c
index 77b69e12e8cb4c541f63607aa0e74f438c74bb10..bb11b50a7a742bc565e774e73a1fb06614a3c025 100644
--- a/tests/builtins/realloc.c
+++ b/tests/builtins/realloc.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 10 -eva-alloc-builtin by_stack -eva-warn-copy-indeterminate @all"
+ STDOPT: +"-eva-slevel 10 -eva-alloc-builtin by_stack -eva-warn-copy-indeterminate @all"
*/
#include <stdlib.h>
diff --git a/tests/builtins/realloc_multiple.c b/tests/builtins/realloc_multiple.c
index 1e5825544465ea4e4bc1ffee2f459fdbb5a5ef05..f5ceb25223f231da7434d019c3ddbca738ff6925 100644
--- a/tests/builtins/realloc_multiple.c
+++ b/tests/builtins/realloc_multiple.c
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-malloc-functions malloc,realloc"
- STDOPT: +"-slevel 10 -eva-alloc-builtin fresh -eva-malloc-functions malloc,realloc -eva-alloc-returns-null"
+ STDOPT: +"-eva-slevel 10 -eva-alloc-builtin fresh -eva-alloc-functions malloc,realloc"
+ STDOPT: +"-eva-slevel 10 -eva-alloc-builtin fresh -eva-alloc-functions malloc,realloc -eva-alloc-returns-null"
*/
#include <stdlib.h>
#include "__fc_builtin.h"
diff --git a/tests/builtins/vla.c b/tests/builtins/vla.c
index 1bfefb182d06e2679293d8d33e3554699c84ebdf..8e8c0eaaad38f34dc565f043ee5dccb8aa962b0a 100644
--- a/tests/builtins/vla.c
+++ b/tests/builtins/vla.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-slevel 10 -eva-builtins-auto"
+ STDOPT: #"-eva-slevel 10 -eva-builtins-auto"
*/
void f(int i) {
diff --git a/tests/float/const3.i b/tests/float/const3.i
index e4bbf48c12d42cb84187e6d84c89c9c3d513f7ee..4e06fb90429a435a24a5ca0d21bbe6d7bb7a307c 100644
--- a/tests/float/const3.i
+++ b/tests/float/const3.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-warn-decimal-float all"
- STDOPT: #"-warn-decimal-float all -all-rounding-modes-constants -float-hex"
+ STDOPT: #"-warn-decimal-float all -eva-all-rounding-modes-constants -float-hex"
*/
double f1 = 1e-40f;
diff --git a/tests/float/const4.i b/tests/float/const4.i
index 0a2be77cb0a4cd47298e3221d20b0e40eba2d0dc..605bad01de2fd3490a144ba6fc2f01c551ed731f 100644
--- a/tests/float/const4.i
+++ b/tests/float/const4.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-warn-decimal-float all"
- STDOPT: #"-warn-decimal-float all -all-rounding-modes-constants"
+ STDOPT: #"-warn-decimal-float all -eva-all-rounding-modes-constants"
*/
double f1 = 3.4e38f;
diff --git a/tests/float/dr.i b/tests/float/dr.i
index 8c2a6c88e235ce2ee009b2016a1176d877dcfe37..b3322030be3ae533c195c498cb48389105283c45 100644
--- a/tests/float/dr.i
+++ b/tests/float/dr.i
@@ -1,7 +1,7 @@
/* run.config*
STDOPT:
STDOPT: #"-float-hex"
- STDOPT: #"-all-rounding-modes-constants"
+ STDOPT: #"-eva-all-rounding-modes-constants"
*/
float big = 100e30f;
diff --git a/tests/float/extract_bits.i b/tests/float/extract_bits.i
index 2f1c3b541cf97a2988bad93da7b58dca27a567bf..083727447193a64d526f1560c853c0a34b6c084e 100644
--- a/tests/float/extract_bits.i
+++ b/tests/float/extract_bits.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
- OPT: -eva @EVA_CONFIG@ -slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
+ OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
*/
float f = 3.14;
diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index 4d258f382ae1e2e040e0e55988c3b6a782ca1b64..d210fe4a31538f2594517d4668c813392b557e6b 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,10 +1,10 @@
/* run.config*
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -eva-slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
*/
#include "__fc_builtin.h"
diff --git a/tests/float/precise_cos_sin.c b/tests/float/precise_cos_sin.c
index 19fde982cfb2f8367bf5c8b2c201a61dec312b8b..f6e6f36e9077b0036d3ebd983c20cc6a0e5f4eb0 100644
--- a/tests/float/precise_cos_sin.c
+++ b/tests/float/precise_cos_sin.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -slevel 1000 -journal-disable -float-normal
+ OPT: -eva @EVA_CONFIG@ -eva-slevel 1000 -journal-disable -float-normal
*/
#include <__fc_builtin.h>
diff --git a/tests/float/round10d.i b/tests/float/round10d.i
index a11f0172affbc62e6d6e3c270aa8887463b70d62..1d6ebe39de506c8e31fe6ea441ba25cfbd408cbd 100644
--- a/tests/float/round10d.i
+++ b/tests/float/round10d.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @EVA_CONFIG@ -float-normal -journal-disable -no-results
+ OPT: -eva @EVA_CONFIG@ -float-normal -journal-disable -eva-no-results
*/
int main()
diff --git a/tests/float/some.c b/tests/float/some.c
index d7713ce8d71d088a7ba48407e83dfc02d1901648..8eb3f38ea73da66b5c52a6779382e274a9a6a3ee 100644
--- a/tests/float/some.c
+++ b/tests/float/some.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -eva-show-slevel 10 -slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -no-results
- OPT: -slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -no-results
+ OPT: -eva-show-slevel 10 -eva-slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double -DN=55" -float-normal -journal-disable -eva-no-results
+ OPT: -eva-slevel 100 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float -DN=26" -float-normal -journal-disable -eva-no-results
*/
FLOAT t[N] = { 1. } ;
diff --git a/tests/float/sqrt.c b/tests/float/sqrt.c
index 02a8d3995c82eddf9ff4ccc105a5652f10113a7a..da6743b0866b14d00ea51c2886806bc546008c96 100644
--- a/tests/float/sqrt.c
+++ b/tests/float/sqrt.c
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: #"-slevel 10 -big-ints-hex 257"
- STDOPT: #"-slevel 10 -big-ints-hex 257 -machdep ppc_32"
+ STDOPT: #"-eva-slevel 10 -big-ints-hex 257"
+ STDOPT: #"-eva-slevel 10 -big-ints-hex 257 -machdep ppc_32"
*/
#include <math.h>
diff --git a/tests/float/widen.c b/tests/float/widen.c
index 8ad29d4d152106a1e0431b2e410abdd38a783694..c685b88be02d1fea3968895deb8f5587c021a88f 100644
--- a/tests/float/widen.c
+++ b/tests/float/widen.c
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: #"-warn-special-float non-finite -wlevel 3"
- STDOPT: #"-warn-special-float none -wlevel 3"
+ STDOPT: #"-warn-special-float non-finite -eva-widening-delay 3"
+ STDOPT: #"-warn-special-float none -eva-widening-delay 3"
*/
volatile int rand;
diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c
index 6c5b0285d74841904ecffe54670abca54e6c0b93..d0dce5401ae9737d1baa182b6bbd0bd2d46f4209 100644
--- a/tests/idct/ieee_1180_1990.c
+++ b/tests/idct/ieee_1180_1990.c
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
+ STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -eva-remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
*/
/* IEEE_1180_1990: a testbed for IDCT accuracy
* Copyright (C) 2001 Renaud Pacalet
diff --git a/tests/impact/alias.i b/tests/impact/alias.i
index f1cc091ed52634e22d631e54007aef47f741febe..1b4edfb05d19133efb9ed8b7154bdd0dce8041cd 100644
--- a/tests/impact/alias.i
+++ b/tests/impact/alias.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-impact-pragma f" +"-lib-entry" +"-main f" +"-remove-redundant-alarms"
+ STDOPT: +"-impact-pragma f" +"-lib-entry" +"-main f" +"-eva-remove-redundant-alarms"
*/
int P,c;
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 2fa988b1e5dc0edf41ab46dd4743b4a77b728a36..342d79af62894d72d30d5a03c8e9c215baf37229 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
+ OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
#include "string.h"
diff --git a/tests/libc/ctype.c b/tests/libc/ctype.c
index a874a223d2888bdcbd9b35573a073beae5a94a42..a54bd13b6a3e38d4186600899a89e5bdf886a15b 100644
--- a/tests/libc/ctype.c
+++ b/tests/libc/ctype.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-slevel 4"
+ STDOPT: #"-eva-slevel 4"
*/
#include <stdio.h>
#include <ctype.h>
diff --git a/tests/libc/netdb_c.c b/tests/libc/netdb_c.c
index 6e8f905b5d80c9afc8f77fadc6e5de394469710c..c2f9a8c9d3440b2ab3533704693e336e39164350 100644
--- a/tests/libc/netdb_c.c
+++ b/tests/libc/netdb_c.c
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-eva-split-return auto -slevel 2"
+ STDOPT: #"-eva-split-return auto -eva-slevel 2"
*/
// Extract based on Linux Programmer's Manual, GETADDRINFO(3) man page
#include <sys/types.h>
diff --git a/tests/libc/signal_h.c b/tests/libc/signal_h.c
index f8aa063de2edf99c21e12b0d14a974e35ab24b0c..c0d539f925a32964ca7764d56389e9467bf68d3d 100644
--- a/tests/libc/signal_h.c
+++ b/tests/libc/signal_h.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-slevel 2"
+ STDOPT: #"-eva-slevel 2"
*/
#include <signal.h>
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index d1dbd85a5a3e9ed1ac0f06f6f455c15bd8006039..33dc8110214a11851008f465801601bf39f23e1b 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
- STDOPT: #"-eva-no-builtins-auto -slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
+ STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
+ STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
STDOPT: #"-eva-no-builtins-auto"
*/ // slevel is used to unroll loops
diff --git a/tests/libc/string_c.c b/tests/libc/string_c.c
index 05e5dc7c140cd844555e21f6bfb9dbbdd56a3635..e5bff29eaf38398b3cf99d6cddebd238e1d08fc0 100644
--- a/tests/libc/string_c.c
+++ b/tests/libc/string_c.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-no-builtins-auto -slevel 1000 -eva-no-skip-stdlib-specs"
+ STDOPT: #"-eva-no-builtins-auto -eva-slevel 1000 -eva-no-skip-stdlib-specs"
*/ // slevel is used to unroll loops
#include "string.c"
diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c
index 9168f43d7369f9d476d037a417f24a713326f6c4..4470a3d07b525b8b4e45e785be34dd8d5dcfa151 100644
--- a/tests/libc/string_c_generic.c
+++ b/tests/libc/string_c_generic.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-includeshare/libc/string.c -slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
+ STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-includeshare/libc/string.c -eva-slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/string_c_strchr.c b/tests/libc/string_c_strchr.c
index 54ed8fab06ee3065c2a13d88a927732181b67b38..83ea787bc73c2df126834751d060407781a888b1 100644
--- a/tests/libc/string_c_strchr.c
+++ b/tests/libc/string_c_strchr.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
+ STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -eva-slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/string_c_strstr.c b/tests/libc/string_c_strstr.c
index 9f0613b351594afcadd9c41bc092315d666f320e..3dd1d13d8904d0e92b9b44ca207323abdd1715f6 100644
--- a/tests/libc/string_c_strstr.c
+++ b/tests/libc/string_c_strstr.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strstr:30 -eva-no-skip-stdlib-specs"
+ STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/sys_stat_h.c b/tests/libc/sys_stat_h.c
index 65ddbfc889097a4af94054d53d6bdac3dc8a428c..24a4b3335118005af0fc3e28cfd303f9d32a1b7e 100644
--- a/tests/libc/sys_stat_h.c
+++ b/tests/libc/sys_stat_h.c
@@ -1,5 +1,5 @@
/*run.config
- STDOPT: #"-slevel 2"
+ STDOPT: #"-eva-slevel 2"
*/
#include <sys/stat.h>
#include <fcntl.h>
diff --git a/tests/libc/sys_wait_h.c b/tests/libc/sys_wait_h.c
index 9eec66c206b1cf766f568412161746f6c6576255..0fe9b221ce15d3d053c1dcccfbe1bbf98007212e 100644
--- a/tests/libc/sys_wait_h.c
+++ b/tests/libc/sys_wait_h.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-slevel 4"
+ STDOPT: #"-eva-slevel 4"
*/
#include <sys/wait.h>
diff --git a/tests/libc/termios.c b/tests/libc/termios.c
index 6ba105607a2194a45ec1f905eadd6c9dfa0727a8..78100d57f84a221223fb79f5d0bbf1f2558699c1 100644
--- a/tests/libc/termios.c
+++ b/tests/libc/termios.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 2"
+ STDOPT: +"-eva-slevel 2"
*/
#include <termios.h>
#include <fcntl.h>
diff --git a/tests/libc/time_h.c b/tests/libc/time_h.c
index c56c8ef3b96cdefead7c20068c10df481f78ba28..30db0860b50e42b76f98891bfd19e15bd06b8d86 100644
--- a/tests/libc/time_h.c
+++ b/tests/libc/time_h.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-slevel 4"
+ STDOPT: #"-eva-slevel 4"
*/
#include <time.h>
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index 8c3104215bf71005b84e6d834a103ebe75056110..8f0f40681fda9b3925c1fc47c67b7fc35893b381 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -1,6 +1,6 @@
/*run.config
- STDOPT: #"-slevel 12" #"-val-split-return auto"
- STDOPT: #"-variadic-no-translation" #"-slevel 12" #"-val-split-return auto"
+ STDOPT: #"-eva-slevel 12" #"-eva-split-return auto"
+ STDOPT: #"-variadic-no-translation" #"-eva-slevel 12" #"-eva-split-return auto"
*/
#define _GNU_SOURCE
#define _XOPEN_SOURCE 600
diff --git a/tests/libc/wchar_c_h.c b/tests/libc/wchar_c_h.c
index ff2b3f2a7d1855818d0732ce7f70aa47fd13be19..8dadb46e2f8bf6ed9d7b3339bb0b193e6a4a08b8 100644
--- a/tests/libc/wchar_c_h.c
+++ b/tests/libc/wchar_c_h.c
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: +"-cpp-extra-args=-DTEST_IMPLEMENTATION=1" +"-slevel 1000"
- STDOPT: +"-slevel 1000"
+ STDOPT: +"-cpp-extra-args=-DTEST_IMPLEMENTATION=1" +"-eva-slevel 1000"
+ STDOPT: +"-eva-slevel 1000"
COMMENT: slevel is used to ensure all loops are unrolled (including in the
COMMENT: implementation). 'goto exit' avoids recomputing split branches.
*/
diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i
index e6d7a20671adcc1bc1e8fd39bb40fec6d3986a45..3d9d35c81d6a7ba665b909e1634f71e3af5289a6 100644
--- a/tests/misc/issue109.i
+++ b/tests/misc/issue109.i
@@ -1,6 +1,6 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva @EVA_CONFIG@ -slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
*/
void main() {
int i, j = 0;
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index 9791791713a0969b77c7df865881d4d485122d32..e4f063807c12972b188952fa735a10024d17c844 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -1,7 +1,7 @@
/* run.config
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DNONCONST
- OPT: -eva @EVA_CONFIG@ -slevel 1 -eva-msg-key widen-hints
+ OPT: -eva @EVA_CONFIG@ -eva-slevel 1 -eva-msg-key widen-hints
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
*/
#define N 2
diff --git a/tests/misc/widen_hints_float.c b/tests/misc/widen_hints_float.c
index db243cd089d58c8bd1eed80efc483b44fd8ec6fc..a01f0a357842a423528cc508dfc39663b307f0a8 100644
--- a/tests/misc/widen_hints_float.c
+++ b/tests/misc/widen_hints_float.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-val-subdivide-non-linear 20"
+ STDOPT: #"-eva-subdivide-non-linear 20"
*/
diff --git a/tests/pdg/top_pdg_input.c b/tests/pdg/top_pdg_input.c
index 7a0e2f57246d1bb5247027af4152bb4142fbe4ff..1fa9bc5856422277ce593946c82f6b026885afe5 100644
--- a/tests/pdg/top_pdg_input.c
+++ b/tests/pdg/top_pdg_input.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-eva -pdg -out -input -deps -no-results-function no_results -eva-no-builtins-auto -load-module pdg -pdg -then -main main_asm"
+ STDOPT: +"-eva -pdg -out -input -deps -eva-no-results-function no_results -eva-no-builtins-auto -load-module pdg -pdg -then -main main_asm"
*/
volatile int nondet;
int no_results() {return 1;}
diff --git a/tests/scope/bts383.c b/tests/scope/bts383.c
index db156cbcfc2619ecba73c24ce6c579bdeec6daee..1f9c07e1e441d144e289dbb78e776694a126d944 100644
--- a/tests/scope/bts383.c
+++ b/tests/scope/bts383.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -print -journal-disable -scope-verbose 1 -remove-redundant-alarms -context-width 3
+ OPT: -eva @EVA_CONFIG@ -print -journal-disable -scope-verbose 1 -eva-remove-redundant-alarms -eva-context-width 3
*/
/*
echo '!Db.Scope.check_asserts();;' \
diff --git a/tests/scope/no-effect.i b/tests/scope/no-effect.i
index 47f41d8fb6b43f9b3a8da29ecc200377f28d7d1b..7b75f9e1d9f28d1b4893aa62a97fa4c8ca2eb3a7 100644
--- a/tests/scope/no-effect.i
+++ b/tests/scope/no-effect.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: @EVA_CONFIG@ -eva -print -journal-disable -scope-verbose 1 -remove-redundant-alarms
+ OPT: @EVA_CONFIG@ -eva -print -journal-disable -scope-verbose 1 -eva-remove-redundant-alarms
*/
typedef struct {
diff --git a/tests/slicing/if_many_values.i b/tests/slicing/if_many_values.i
index 11bf03bc16c2907a4eb2eb466a28e8bac5de15d6..55807dadf286d3685bc3ee45af146cde7b69d55c 100644
--- a/tests/slicing/if_many_values.i
+++ b/tests/slicing/if_many_values.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-slice-value r -journal-disable -slevel 101 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
+ STDOPT: +"-slice-value r -journal-disable -eva-slevel 101 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
**/
int r=1;
diff --git a/tests/slicing/keep_annot.i b/tests/slicing/keep_annot.i
index ae570853dfd277f7d4d21ce5cd9431a8ffa98a79..adbfac557cdd72ec714389f10b6ff0cd2d834f07 100644
--- a/tests/slicing/keep_annot.i
+++ b/tests/slicing/keep_annot.i
@@ -1,8 +1,8 @@
/* run.config
- STDOPT: +"-context-valid-pointers -lib-entry -main f -slice-assert f -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-context-valid-pointers -lib-entry -main f -slice-assert f -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-context-valid-pointers -lib-entry -main L -slice-pragma L -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-context-valid-pointers -lib-entry -main L -slice-pragma L -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-eva-context-valid-pointers -lib-entry -main f -slice-assert f -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-eva-context-valid-pointers -lib-entry -main f -slice-assert f -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-eva-context-valid-pointers -lib-entry -main L -slice-pragma L -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-eva-context-valid-pointers -lib-entry -main L -slice-pragma L -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-slice-return bts1110 -main bts1110 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
diff --git a/tests/slicing/unravel-variance.i b/tests/slicing/unravel-variance.i
index e30a4aebcb2fa7acd21f6d33caa29b6cfa798426..554c7a94398639cd00d2809946b0248bb1bb4726 100644
--- a/tests/slicing/unravel-variance.i
+++ b/tests/slicing/unravel-variance.i
@@ -1,9 +1,9 @@
/* run.config
- STDOPT: +"-slice-calls printf1 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-slice-calls printf2 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-slice-calls printf3 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-slice-calls printf4 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-slice-calls printf5 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-calls printf1 -journal-disable -float-normal -eva-remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-calls printf2 -journal-disable -float-normal -eva-remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-calls printf3 -journal-disable -float-normal -eva-remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-calls printf4 -journal-disable -float-normal -eva-remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-calls printf5 -journal-disable -float-normal -eva-remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
*/
/* Small example devired from examples given for UNRAVEL tool : */
diff --git a/tests/syntax/loop-case-switch-for-unroll.c b/tests/syntax/loop-case-switch-for-unroll.c
index c379555af57ec055957c8c275177345fa51eb177..7785be51b6a9e2495750bee02becb6c8fd846b61 100644
--- a/tests/syntax/loop-case-switch-for-unroll.c
+++ b/tests/syntax/loop-case-switch-for-unroll.c
@@ -1,7 +1,7 @@
/* run.config
- STDOPT: +"-slevel 100 -eva"
- STDOPT: +"-ulevel 1 -slevel 100 -eva"
- STDOPT: +"-ulevel 2 -slevel 100 -eva"
+ STDOPT: +"-eva-slevel 100 -eva"
+ STDOPT: +"-ulevel 1 -eva-slevel 100 -eva"
+ STDOPT: +"-ulevel 2 -eva-slevel 100 -eva"
COMMENT: compile and run with GCC, save output to a file, and compare it to
the result of Frama-C piped to:
"| grep Frama_C_show_each | sed 's/^.*Frama_C_show_each_//'"
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 4ccad645f15c61425fcf07b5c25f80d4d7bc3108..66da8b7cf4882b0214a9cc46294e20ff7f81668b 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -1,6 +1,6 @@
/* run.config
STDOPT: +"-eva @EVA_CONFIG@"
- STDOPT: +"-eva @EVA_CONFIG@ -main main2 -slevel 3"
+ STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
*/
enum { SIX = 6 } ;
volatile foo;
diff --git a/tests/value/CruiseControl.c b/tests/value/CruiseControl.c
index eb8c3acf07ffdf0a1248b0bbd0cbd3c6ffc8edc0..868f2ad6eb779e75abf4b56ef98017892d881cef 100644
--- a/tests/value/CruiseControl.c
+++ b/tests/value/CruiseControl.c
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- STDOPT: #"-float-normal tests/value/CruiseControl_const.c -lib-entry -main CruiseControl -context-depth 10 -context-valid-pointers"
+ STDOPT: #"-float-normal tests/value/CruiseControl_const.c -lib-entry -main CruiseControl -eva-context-depth 10 -eva-context-valid-pointers"
*/
/*$************* SCADE_KCG KCG Version 5.1.1 (build i10) **************
diff --git a/tests/value/ai_annot.i b/tests/value/ai_annot.i
index 9a531689e600c192c4a5ac0c314b0cd7c1f58d93..16034a0e0f48ea1185d1aca2066ddbc5c08bdcde 100644
--- a/tests/value/ai_annot.i
+++ b/tests/value/ai_annot.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-load-module scope -scope-verbose 2 -remove-redundant-alarms -context-width 3"
+ STDOPT: #"-load-module scope -scope-verbose 2 -eva-remove-redundant-alarms -eva-context-width 3"
*/
diff --git a/tests/value/alias.i b/tests/value/alias.i
index 048db0914217733f9dd52f7839b5144870d7f2b9..4b91cf96a5b9397faf75c5a65279b01cff0312ba 100644
--- a/tests/value/alias.i
+++ b/tests/value/alias.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-no-results-function f"
+ STDOPT: #"-eva-no-results-function f"
STDOPT: #"-main main3"
STDOPT: #"-main main4 -absolute-valid-range 0-0xFF"
STDOPT: #"-main main5"
diff --git a/tests/value/base_addr_offset_block_length.i b/tests/value/base_addr_offset_block_length.i
index 4a20889d500dc60519782ff4c15c287bfb360174..b3aad4d14b7a622e69f1e547cd8f84ef8434dfbd 100644
--- a/tests/value/base_addr_offset_block_length.i
+++ b/tests/value/base_addr_offset_block_length.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -context-width 3 -then -slevel 3
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-context-width 3 -then -eva-slevel 3
*/
diff --git a/tests/value/big_lib_entry.i b/tests/value/big_lib_entry.i
index 88a7fbc821ae225258a104cb7fd8e57aa28b6445..0c2770eab0fefe3254629223350644dbbf8493e2 100644
--- a/tests/value/big_lib_entry.i
+++ b/tests/value/big_lib_entry.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -context-width 4 -eva-initialization-padding-globals no
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -eva-context-width 4 -eva-initialization-padding-globals no
*/
typedef struct {
diff --git a/tests/value/bts1306.i b/tests/value/bts1306.i
index f6b51b857843812b7e4d12234621aee910cce851..81f9cc8f329ead372748ebd5eea97821b99bc0bd 100644
--- a/tests/value/bts1306.i
+++ b/tests/value/bts1306.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -slevel 0 -eva @EVA_CONFIG@ -print -then -slevel 10 -eva -print
+ OPT: -no-autoload-plugins -load-module from,inout,eva -constfold -eva-slevel 0 -eva @EVA_CONFIG@ -print -then -eva-slevel 10 -eva -print
*/
void g(double x) { double y= x*x; }
diff --git a/tests/value/bug0245.i b/tests/value/bug0245.i
index 584d53f784613d1e5fdaf284e2aab0cdaf4d85c2..1408f3e7deeb0460eecff7c912685185868d8438 100644
--- a/tests/value/bug0245.i
+++ b/tests/value/bug0245.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-slevel 4"
+ STDOPT: #"-eva-slevel 4"
*/
int R,*p,S,*q;
diff --git a/tests/value/builtins_split.c b/tests/value/builtins_split.c
index a04c5fcd46b8fc0e048b6a8e50fc2fce6d7b9639..cc38f28c313dbd9e2c022b8eabe768de8f2a38c8 100644
--- a/tests/value/builtins_split.c
+++ b/tests/value/builtins_split.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-eva-show-progress -slevel 100"
+ STDOPT: +"-eva-show-progress -eva-slevel 100"
*/
int *p;
diff --git a/tests/value/case_analysis.i b/tests/value/case_analysis.i
index 7d9214dd079a84c2c58e219dd718d5a27b99bb24..40be501257b9f1b5edca5e3a305db685148deb04 100644
--- a/tests/value/case_analysis.i
+++ b/tests/value/case_analysis.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -slevel 30 -journal-disable -float-normal
+ OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -eva-slevel 30 -journal-disable -float-normal
*/
diff --git a/tests/value/cmp_ptr.i b/tests/value/cmp_ptr.i
index 198a11aacafb3b00f5ac7bc29616a246c9dfba81..da2355d605ce612d4dc434c9509789e2602949a7 100644
--- a/tests/value/cmp_ptr.i
+++ b/tests/value/cmp_ptr.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-main main -eva-msg-key pointer-comparison"
- STDOPT: #"-undefined-pointer-comparison-propagate-all -eva-msg-key pointer-comparison"
+ STDOPT: #"-eva-undefined-pointer-comparison-propagate-all -eva-msg-key pointer-comparison"
*/
int *p,T[10]={0,1,2,3,4,5,6,7,8,9};
diff --git a/tests/value/cmp_ptr_follow_all_branches.i b/tests/value/cmp_ptr_follow_all_branches.i
index 2e5292ae2db3c924c1586872f139a8dfd3a55378..71e72fec503aa835b228de03a8e238e7ac627b69 100644
--- a/tests/value/cmp_ptr_follow_all_branches.i
+++ b/tests/value/cmp_ptr_follow_all_branches.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-eva-msg-key pointer-comparison"
- STDOPT: #"-undefined-pointer-comparison-propagate-all -eva-msg-key pointer-comparison"
+ STDOPT: #"-eva-undefined-pointer-comparison-propagate-all -eva-msg-key pointer-comparison"
*/
int a;
diff --git a/tests/value/cond_integer_cast_of_float.i b/tests/value/cond_integer_cast_of_float.i
index 3a6d8768ec945afce02f2c361459b3d97e9903f7..9d1350ea671348d2759998a9ec5b3f9a2473455b 100644
--- a/tests/value/cond_integer_cast_of_float.i
+++ b/tests/value/cond_integer_cast_of_float.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -no-results -then -float-hex -main mainbis
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-results -then -float-hex -main mainbis
*/
typedef double D;
typedef float F;
diff --git a/tests/value/context_width.i b/tests/value/context_width.i
index b9209213bc3f93315d7fdb4fbd476f53caee2776..e2f3d39895a2dbbebc76cb98c263efac2e5aa080 100644
--- a/tests/value/context_width.i
+++ b/tests/value/context_width.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-context-width 3 -then -print -then -context-width 1"
+ STDOPT: +"-eva-context-width 3 -then -print -then -eva-context-width 1"
*/
int a;
diff --git a/tests/value/div.i b/tests/value/div.i
index dcea8cf46d46eb257041662c2645467b92d170aa..3ac38b6068dae4271ea190752b7b1efcac5fe878 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-load-module scope -remove-redundant-alarms"
+ STDOPT: #"-load-module scope -eva-remove-redundant-alarms"
OPT: -no-autoload-plugins -load-module eva,inout -rte -then -eva @EVA_CONFIG@
*/
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
diff --git a/tests/value/domains.i b/tests/value/domains.i
index 434324fc2f5dd1047505aed2df088c06631bdccb..22b198ea39fc8bd5e37848ce41c3dbf82294acd3 100644
--- a/tests/value/domains.i
+++ b/tests/value/domains.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges -slevel 2"
+ STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges -eva-slevel 2"
*/
/* Tests five domains together. */
diff --git a/tests/value/exit_paths.i b/tests/value/exit_paths.i
index 9182998fe6295a704b306442e1a23c2847412ba3..3d0ac19e03486b4f1ec0f3113323621116a48f5c 100644
--- a/tests/value/exit_paths.i
+++ b/tests/value/exit_paths.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-wlevel 1"
+ STDOPT: +"-eva-widening-delay 1"
*/
#include "__fc_builtin.h"
diff --git a/tests/value/gauges.c b/tests/value/gauges.c
index ab2963f70b41dbb3f18e2a7915fc2d81a7c0d5d4..8acfac2c4118ae76f68f363d01f00159e02e04f9 100644
--- a/tests/value/gauges.c
+++ b/tests/value/gauges.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +" -slevel-function main8_aux:2,main5_bis:4 -eva-msg-key d-gauges"
+ STDOPT: +" -eva-slevel-function main8_aux:2,main5_bis:4 -eva-msg-key d-gauges"
*/
#include <stdlib.h>
diff --git a/tests/value/invalid_loc_return.i b/tests/value/invalid_loc_return.i
index 729b0a9038c108492f02071ee645ab7160d7b6ba..7cdc2deecad080c2053ea4fc300c48efb525a793 100644
--- a/tests/value/invalid_loc_return.i
+++ b/tests/value/invalid_loc_return.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-main main1 -then -slevel 3 -main main2"
+ STDOPT: +"-main main1 -then -eva-slevel 3 -main main2"
*/
int foo() {
diff --git a/tests/value/lazy.i b/tests/value/lazy.i
index 11f7d183bfbe11ea5176b9d9d758e079701fafbc..5b4b95d35dcbe6e6dade2a74277075ba902d34b7 100644
--- a/tests/value/lazy.i
+++ b/tests/value/lazy.i
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: #"-eva-msg-key pointer-comparison"
- STDOPT: #"-undefined-pointer-comparison-propagate-all -eva-msg-key pointer-comparison"
+ STDOPT: #"-eva-undefined-pointer-comparison-propagate-all -eva-msg-key pointer-comparison"
*/
int a=-1;
int b, d;
diff --git a/tests/value/library.i b/tests/value/library.i
index bbb69d46eb94dd04abf1dc6f3a0f186c14c315f0..6f7615e06383c9692c4e0050d7f06e36194411b3 100644
--- a/tests/value/library.i
+++ b/tests/value/library.i
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- STDOPT: +"-eva-msg-key initial-state -eva-initialization-padding-globals no -lib-entry -main main -context-depth 3 -then -main main2 -then -context-width 4"
+ STDOPT: +"-eva-msg-key initial-state -eva-initialization-padding-globals no -lib-entry -main main -eva-context-depth 3 -then -main main2 -then -eva-context-width 4"
*/
int f_int(int x);
diff --git a/tests/value/local_slevel.i b/tests/value/local_slevel.i
index 985751249a226ba99972a87bab0d0d6f723ede39..f8a28e1829933eca449024a9d5c635fb03a98f24 100644
--- a/tests/value/local_slevel.i
+++ b/tests/value/local_slevel.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +" -load-module frama-c-constant_propagation -slevel-function main2:100000 -print -then -scf -then-on propagated -eva -eva-show-progress -no-scf"
+ STDOPT: +" -load-module frama-c-constant_propagation -eva-slevel-function main2:100000 -print -then -scf -then-on propagated -eva -eva-show-progress -no-scf"
*/
int *p;
diff --git a/tests/value/logic_ptr_cast.i b/tests/value/logic_ptr_cast.i
index 6f4c7af2f12976ac4cab2c017bad0db2d826d135..64eb43489d69f0c135df3a29dda3d8eee22bb6c2 100644
--- a/tests/value/logic_ptr_cast.i
+++ b/tests/value/logic_ptr_cast.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -print -journal-disable -no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -print -journal-disable -eva-no-results
*/
int *p;
int t[90];
diff --git a/tests/value/loopfun.i b/tests/value/loopfun.i
index 030e2654b43ef017571f659a983d660c59ed3315..2db5a9837a566a70e3ab9b52f690bedb21f26e14 100644
--- a/tests/value/loopfun.i
+++ b/tests/value/loopfun.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 50 -no-results"
+ STDOPT: +"-eva-slevel 50 -eva-no-results"
STDOPT: +"-eva-warn-key=missing-loop-unroll=feedback -eva-warn-key=missing-loop-unroll:for=active -main main2"
*/
static int a = 7;
diff --git a/tests/value/loopinv.c b/tests/value/loopinv.c
index fbb89b089a48133c41a3cfa20648cb9a5b2c633d..26f3a1e37b27e5b099b572084544f16092a6d911 100644
--- a/tests/value/loopinv.c
+++ b/tests/value/loopinv.c
@@ -1,5 +1,5 @@
/* run.config*
-OPT: @EVA_CONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -slevel-function main2:20 -pp-annot -eva -then -report
+OPT: @EVA_CONFIG@ -no-autoload-plugins -load-module from,inout,eva,report -eva-slevel-function main2:20 -pp-annot -eva -then -report
*/
/*@ requires valid: \valid(&t[0..s-1]);
diff --git a/tests/value/modulo.i b/tests/value/modulo.i
index 81d342ce9470528e1e0573acd12de263133c6269..70e4fe6ceec0abdb7f206548ce5e2a3274d0dc25 100644
--- a/tests/value/modulo.i
+++ b/tests/value/modulo.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-slevel-function pgcd1:100,pgcd2:100,pgcd3:100"
+ STDOPT: #"-eva-slevel-function pgcd1:100,pgcd2:100,pgcd3:100"
*/
int A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R;
volatile v;
diff --git a/tests/value/narrow_behaviors.i b/tests/value/narrow_behaviors.i
index 64d98062b974c7c2c08a6c2cd4fecf86ea31f830..ba639b21956aaca1ad7e86a4a7f6159bafa98f78 100644
--- a/tests/value/narrow_behaviors.i
+++ b/tests/value/narrow_behaviors.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 10 -eva-verbose 2"
+ STDOPT: +"-eva-slevel 10 -eva-verbose 2"
*/
extern int nondet;
diff --git a/tests/value/no_results.c b/tests/value/no_results.c
index 1f2355186c9fb157e5d69aa965e1476a3dee0c14..39549decf2a333dd2d54028da0eba8b96aa41c0a 100644
--- a/tests/value/no_results.c
+++ b/tests/value/no_results.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-no-results-function init -calldeps -slevel 10000" +"-inout"
+ STDOPT: #"-eva-no-results-function init -calldeps -eva-slevel 10000" +"-inout"
*/
#define N 3000
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 3e988afe4882c009bbfa39e4f7c73ed77f551148..7bfb7aff0243d6fb76ac66ee9a5adf16a98cbed9 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -1,3 +1,5 @@
+[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
+ Please use -eva-slevel instead.
[kernel] Parsing tests/value/summary.i (no preprocessing)
[rte] annotating function alarms
[rte] annotating function bottom
diff --git a/tests/value/plevel.i b/tests/value/plevel.i
index 01f7e73dd47f3ea92749bdb166413b7fdaca4c8a..202526dc0dec493b2a96fdf8f34786145210a30e 100644
--- a/tests/value/plevel.i
+++ b/tests/value/plevel.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-plevel 40 -big-ints-hex 0x55"
+ STDOPT: #"-eva-plevel 40 -big-ints-hex 0x55"
*/
int t[0xFFFF];
diff --git a/tests/value/pointer_comparison.c b/tests/value/pointer_comparison.c
index 2dcf42073538d749686ebbd0fe38cc7fc6cb9e30..40717af44c5547544a81941d440e3e5673642187 100644
--- a/tests/value/pointer_comparison.c
+++ b/tests/value/pointer_comparison.c
@@ -1,6 +1,6 @@
/* run.config*
STDOPT: +" -load-module report -report-print-properties -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
- STDOPT: +" -load-module report -report-print-properties -undefined-pointer-comparison-propagate-all -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
+ STDOPT: +" -load-module report -report-print-properties -eva-undefined-pointer-comparison-propagate-all -eva-warn-undefined-pointer-comparison none -eva-msg-key pointer-comparison -then -report -then -eva-warn-undefined-pointer-comparison pointer -then -report -then -eva-warn-undefined-pointer-comparison all -then -report"
*/
int x,y,*p;
int main(){
diff --git a/tests/value/precise_locations.i b/tests/value/precise_locations.i
index 06340dba48ae65c8c9ed814351463b7a34cc27ab..942739895819533255887b5f61ec8f7e124fd806 100644
--- a/tests/value/precise_locations.i
+++ b/tests/value/precise_locations.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -plevel 250"
+ STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -eva-plevel 250"
*/
struct s {
diff --git a/tests/value/ptr_call_object.c b/tests/value/ptr_call_object.c
index f8872244f28601965d84fa91fbc764ea07d893ea..b02914deb9630d848e1bcbfaa8c4f4b0d00af6ae 100644
--- a/tests/value/ptr_call_object.c
+++ b/tests/value/ptr_call_object.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 2"
+ STDOPT: +"-eva-slevel 2"
*/
struct obj {
diff --git a/tests/value/recol.c b/tests/value/recol.c
index 5d0d3e258cafc1c7999e035c68337ba922a2b1db..46f6de92f5ab375b405205aee08f18c3c344ddcf 100644
--- a/tests/value/recol.c
+++ b/tests/value/recol.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
- OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -no-warn-signed-overflow
+ OPT: -no-autoload-plugins -load-module eva,inout -eva @EVA_CONFIG@ -eva-slevel 100 -cpp-extra-args="-DPTEST " -journal-disable -machdep ppc_32 -no-warn-signed-overflow
*/
#ifndef PTEST
diff --git a/tests/value/redundant_alarms.c b/tests/value/redundant_alarms.c
index cd26fec1a2c7ab4b10c2b944536d16f4ceff23ee..a6b1785cd3d19a218c1a13b55ca62b8bda5344d0 100644
--- a/tests/value/redundant_alarms.c
+++ b/tests/value/redundant_alarms.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
+ OPT: -no-autoload-plugins -load-module inout,scope,slicing,sparecode @EVA_CONFIG@ -eva-warn-copy-indeterminate=-@all,main3 -scope-msg-key rm_asserts -scope-verbose 2 -eva-remove-redundant-alarms -print -slice-threat main1 -then-on 'Slicing export' -print
**/
volatile int v;
diff --git a/tests/value/reevaluate_alarms.i b/tests/value/reevaluate_alarms.i
index c0fc49d5b7698af6fe344bb15d79cd2b2d8686c3..9085a0a7185533f1b36bbf543d4b94b45f86db36 100644
--- a/tests/value/reevaluate_alarms.i
+++ b/tests/value/reevaluate_alarms.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-load-module report -report -then -slevel 10"
+ STDOPT: +"-load-module report -report -then -eva-slevel 10"
*/
diff --git a/tests/value/slevelex.i b/tests/value/slevelex.i
index ed8cb52583d2b6106297347ee22912b246e0d648..2c2546796fb9969c93cfc2ca1e32577ee02f9b91 100644
--- a/tests/value/slevelex.i
+++ b/tests/value/slevelex.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-slevel 5 -slevel-function main:0 -slevel-function gu:21 -slevel-function ginc:21"
+ STDOPT: #"-eva-slevel 5 -eva-slevel-function main:0 -eva-slevel-function gu:21 -eva-slevel-function ginc:21"
*/
volatile int c;
diff --git a/tests/value/split_return.i b/tests/value/split_return.i
index 3873c1b9d225aa0b381b5f54405ac272f630d88f..8cfc8a21a7528455accae9f91f3678fc12e51767 100644
--- a/tests/value/split_return.i
+++ b/tests/value/split_return.i
@@ -1,10 +1,10 @@
/* run.config*
- STDOPT: +"-deterministic -eva-no-memexec -slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3,uninit:2,main9:2 -eva-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4,uninit:0,escaping:0 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -permissive -then -load-module report -report"
- STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -slevel 6 -eva-split-return auto -eva-split-return-function f7:0:3 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -load-module report -report"
+ STDOPT: +"-deterministic -eva-no-memexec -eva-slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3,uninit:2,main9:2 -eva-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4,uninit:0,escaping:0 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -permissive -then -load-module report -report"
+ STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return auto -eva-split-return-function f7:0:3 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -load-module report -report"
COMMENT: below command must fail, as -permissive is not set
- STDOPT: +"-deterministic -eva-no-memexec -eva -slevel-function NON_EXISTING:4 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
- STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -slevel 6 -eva-split-return full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
- STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -slevel 6 -eva-split-return full -eva-split-return-function f7:0:3 -eva-split-return-function f2:full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -eva-split-return-function f2:auto"
+ STDOPT: +"-deterministic -eva-no-memexec -eva -eva-slevel-function NON_EXISTING:4 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+ STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+ STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return full -eva-split-return-function f7:0:3 -eva-split-return-function f2:full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -eva-split-return-function f2:auto"
*/
/*@ assigns \result \from \nothing;
diff --git a/tests/value/summary.i b/tests/value/summary.i
index d73b4b42d73532f315dedb80d1c927415566d9eb..8d5d6efd3f583a37f9ef638481739269650a8d07 100644
--- a/tests/value/summary.i
+++ b/tests/value/summary.i
@@ -3,7 +3,7 @@
STDOPT: +"-eva-msg-key=summary -main minimal"
STDOPT: +"-eva-msg-key=summary -main bottom"
STDOPT: +"-eva-msg-key=summary -main main"
- STDOPT: +"-rte -eva-msg-key=summary -main main"
+ STDOPT: +"-rte -eva-msg-key=summary -main main -slevel 0"
*/
/* Tests the summary on the smallest possible program. */
diff --git a/tests/value/traces/test1.c b/tests/value/traces/test1.c
index b6097db5d277c05f882ffbd7b5794ca3be9eaf55..2eda2c29eb845ca3b7a6c489f0be9bbd3a1b7c14 100644
--- a/tests/value/traces/test1.c
+++ b/tests/value/traces/test1.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces"
+ STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10 -eva-traces-project" +"-then-last -eva -print -eva-msg-key=-d-traces"
*/
extern volatile int entropy_source;
diff --git a/tests/value/traces/test2.i b/tests/value/traces/test2.i
index 506b765112f7299a247614388e37f77a0529ca2e..11d8611c60a21d9fa6a6fa1869ebc776758e2f7b 100644
--- a/tests/value/traces/test2.i
+++ b/tests/value/traces/test2.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces"
+ STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10 -eva-traces-project" +"-then-last -eva -print -eva-msg-key=-d-traces"
*/
diff --git a/tests/value/traces/test3.i b/tests/value/traces/test3.i
index 80f30b09d39867dbe21a746c0ab0eb775ec9cc98..1878979fbfec0ed04f1df12c27e4377881fa2b30 100644
--- a/tests/value/traces/test3.i
+++ b/tests/value/traces/test3.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10 -eva-traces-project" +"-then-last -val -print -value-msg-key=-d-traces"
+ STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10 -eva-traces-project" +"-then-last -eva -print -eva-msg-key=-d-traces"
*/
int g;
diff --git a/tests/value/traces/test4.i b/tests/value/traces/test4.i
index 5cb5ad20e108eb43f8bd401375b2f9eaa8b35790..ef512f629ee089ba990926f3d9abde6584129e19 100644
--- a/tests/value/traces/test4.i
+++ b/tests/value/traces/test4.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10"
+ STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10"
*/
/* Test of join inside a loop */
diff --git a/tests/value/traces/test5.i b/tests/value/traces/test5.i
index 60775951cadfd3c59496c198156438b766b3451e..d3f122845da8990429ab62d1f98d30ebd81bfb4b 100644
--- a/tests/value/traces/test5.i
+++ b/tests/value/traces/test5.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-eva-domains traces -value-msg-key d-traces -slevel 10" +"-then-last -val -slevel 10 -print -no-eva-traces-domain"
+ STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10" +"-then-last -eva -eva-slevel 10 -print -no-eva-traces-domain"
*/
diff --git a/tests/value/uninit_callstack.i b/tests/value/uninit_callstack.i
index 3c1d29d57655fbf18f9134cfc186dd1b45ace78a..6adb7e5120047524db8d21d776a7d7f5d76c9abc 100644
--- a/tests/value/uninit_callstack.i
+++ b/tests/value/uninit_callstack.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -no-results
+ OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -journal-disable -eva-no-results
*/
int *p, x;
diff --git a/tests/value/widen_on_non_monotonic.i b/tests/value/widen_on_non_monotonic.i
index c20b8bc79102a5e523696f80da4ed5c5508ef0b0..1242896475e2675dda3c994f558ac1da7d0e512c 100644
--- a/tests/value/widen_on_non_monotonic.i
+++ b/tests/value/widen_on_non_monotonic.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-slevel 20"
+ STDOPT: #"-eva-slevel 20"
*/
/* Problem with Value's memory model, that does not guarantee that we call