From 6c0ab273cf128df47917e7c30c8bfb1ad13c8938 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 23 Sep 2020 14:12:16 +0200
Subject: [PATCH] [Eva] Fixes Eva parameters names in various comments and
messages.
---
src/plugins/nonterm/nonterm_run.ml | 2 +-
src/plugins/value/domains/cvalue/builtins_malloc.ml | 2 +-
src/plugins/value/domains/cvalue/builtins_print_c.ml | 2 +-
src/plugins/value/engine/compute_functions.ml | 4 ++--
src/plugins/value/engine/transfer_stmt.ml | 2 +-
src/plugins/value/utils/value_perf.ml | 2 +-
src/plugins/value/values/cvalue_backward.ml | 2 +-
7 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 007d64d2489..a4f74bc205a 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -239,7 +239,7 @@ let check_unreachable_statements kf ~to_ignore ~dead_code ~warned_kfs =
are ignored if:
1. the function is in the list of functions to be ignored;
2. or the function has a body AND its specification is not being used
- via -val-use-spec.
+ via -eva-use-spec.
In case 2, the call is ignored because non-terminating statements inside
it will already be reported. *)
let ignore_kf name =
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 3387cb48196..576d50e93ce 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -297,7 +297,7 @@ let add_zeroes = add_v (V_Or_Uninitialized.initialized Cvalue.V.singleton_zero)
[orig_state]: state before any allocation, returned in case of failure;
[state_after_alloc]: state in case the allocation is successful;
[returns_null]: if given, forces the result to consider/ignore the
- possibility of failure, despite -val-alloc-returns-null. *)
+ possibility of failure, despite -eva-alloc-returns-null. *)
let wrap_fallible_alloc ?returns_null ret orig_state state_after_alloc =
let default_returns_null = Value_parameters.AllocReturnsNull.get () in
let returns_null = Extlib.opt_conv default_returns_null returns_null in
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index bba8b1b0900..1ac0850f13a 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -140,7 +140,7 @@ let pretty_pointer_assignment fmt typname lv v =
Kernel.abort ~current:true
"pretty_pointer_assignment expected cardinal zero or one@ \
for value %a (lv %s);@ \
- (did you forget -val-no-alloc-returns-null?)" Cvalue.V.pretty v lv
+ (did you forget -eva-no-alloc-returns-null?)" Cvalue.V.pretty v lv
let types = Hashtbl.create 7;;
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index e7d1b0f5a42..2e3d42bdb5d 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -55,7 +55,7 @@ let options_ok () =
Value_parameters.UsePrototype.iter (fun kf -> check_assigns kf)
(* Do something tasteless in case the user did not put a spec on functions
- for which he set [-val-use-spec]: generate an incorrect one ourselves *)
+ for which he set [-eva-use-spec]: generate an incorrect one ourselves *)
let generate_specs () =
let aux kf =
if need_assigns kf then begin
@@ -156,7 +156,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Compute a call to [kf] in the state [state]. The evaluation will
be done either using the body of [kf] or its specification, depending
- on whether the body exists and on option [-val-use-spec]. [call_kinstr]
+ on whether the body exists and on option [-eva-use-spec]. [call_kinstr]
is the instruction at which the call takes place, and is used to update
the statuses of the preconditions of [kf]. If [show_progress] is true,
the callstack and additional information are printed. *)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 6fb1f72709b..d7bb71ccae0 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -239,7 +239,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Value (valuation, lloc, ltyp) ->
(* Tries to interpret the assignment as a copy for the returned value
of a function call, on struct and union types, and when
- -val-warn-copy-indeterminate is disabled. *)
+ -eva-warn-copy-indeterminate is disabled. *)
let lval_copy =
if is_ret || Cil.isStructOrUnionType ltyp || do_copy_at kinstr
then find_lval expr
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index 6dea7f2ed29..de12cb45574 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -356,7 +356,7 @@ let reset_perf () =
(* --- Flamegraphs --- *)
(* -------------------------------------------------------------------------- *)
-(* Set to [Some _] if option [-val-dump-flamegraph] is set and [main] is
+(* Set to [Some _] if option [-eva-flamegraph] is set and [main] is
currently being analyzed and the file is ok. Otherwise, set to [None]. *)
let oc_flamegraph = ref None
diff --git a/src/plugins/value/values/cvalue_backward.ml b/src/plugins/value/values/cvalue_backward.ml
index c836d2a9c76..e97975c050f 100644
--- a/src/plugins/value/values/cvalue_backward.ml
+++ b/src/plugins/value/values/cvalue_backward.ml
@@ -339,7 +339,7 @@ let downcast_enabled ~ik_src ~ik_dst =
if Cil.isSigned ik_dst
then
Kernel.SignedDowncast.get () ||
- (* In this case, -val-warn-signed-converted-downcast behaves exactly
+ (* In this case, -eva-warn-signed-converted-downcast behaves exactly
as -warn-signed-downcast *)
(Cil.isSigned ik_src && Value_parameters.WarnSignedConvertedDowncast.get ())
else Kernel.UnsignedDowncast.get ()
--
GitLab