diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 007d64d2489222988c70aab46b2e4f6e9ac3b35d..a4f74bc205af61d14b74d1eb2858549055584bd5 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 3387cb48196b592ded4465313f97293ec2586884..576d50e93ce9e1f11f25433ecae4e35b2ffce24e 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 bba8b1b0900724fe2ebc9f53dbfcc4720078a7b7..1ac0850f13ad7937f856416fc5ea43ade0a44e74 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 e7d1b0f5a427acca6b2d5b7e2bc89d6c8adc0b33..2e3d42bdb5d29f4e24c625d3902c56a1e2b14d56 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 6fb1f72709bfc725960f7f3546fc242e3668b048..d7bb71ccae05b325d7b83953d4f3af716a8b3f6b 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 6dea7f2ed2919b1dce27acfa2f1bc8aaa2d10de9..de12cb45574f55de6f26fcacb0b4d585c7fdfff1 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 c836d2a9c76353e6af712aaa01089db36d0b0a1e..e97975c050f33847eb9ab812b7681dd24ab44e3f 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 ()