diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index cd4ef32136c15f52f83a89a6089bee1d4f98f126..4d65f1e3c4fcd02e14c3eca1c1433af754bff333 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -380,7 +380,7 @@ module ResultsAll =
True
(struct
let option_name = "-eva-results"
- let help = "record values for any of the statements of the program."
+ let help = "record values for each of the statements of the program."
end)
let () = add_dep ResultsAll.parameter
let () = ResultsAll.add_aliases ["-results"]
@@ -390,7 +390,7 @@ module JoinResults =
Bool
(struct
let option_name = "-eva-join-results"
- let help = "precompute consolidated states once value is computed"
+ let help = "precompute consolidated states once Eva is computed"
let default = true
end)
let () = JoinResults.add_aliases ["-val-join-results"]
@@ -458,7 +458,9 @@ module AllRoundingModesConstants =
False
(struct
let option_name = "-eva-all-rounding-modes-constants"
- let help = "Take into account the possibility of constants not being converted to the nearest representable value, or being converted to higher precision"
+ let help = "Take into account the possibility of constants not being \
+ converted to the nearest representable value, \
+ or being converted to higher precision"
end)
let () = add_correctness_dep AllRoundingModesConstants.parameter
let () = AllRoundingModesConstants.add_aliases ["-all-rounding-modes-constants"]
@@ -468,7 +470,9 @@ module UndefinedPointerComparisonPropagateAll =
False
(struct
let option_name = "-eva-undefined-pointer-comparison-propagate-all"
- let help = "if the target program appears to contain undefined pointer comparisons, propagate both outcomes {0; 1} in addition to the emission of an alarm"
+ let help = "if the target program appears to contain undefined pointer \
+ comparisons, propagate both outcomes {0; 1} in addition to \
+ the emission of an alarm"
end)
let () = add_correctness_dep UndefinedPointerComparisonPropagateAll.parameter
let () =
@@ -568,7 +572,7 @@ module ReduceOnLogicAlarms =
(struct
let option_name = "-eva-reduce-on-logic-alarms"
let help = "Force reductions by a predicate to ignore logic alarms \
- emitted while the predicated is evaluated (experimental)"
+ emitted while the predicate is evaluated (experimental)"
end)
let () = add_correctness_dep ReduceOnLogicAlarms.parameter
let () = ReduceOnLogicAlarms.add_aliases ["-val-reduce-on-logic-alarms"]
@@ -619,7 +623,8 @@ module AllocatedContextValid =
False
(struct
let option_name = "-eva-context-valid-pointers"
- let help = "only allocate valid pointers until context-depth, and then use NULL (defaults to false)"
+ let help = "only allocate valid pointers until context-depth, \
+ and then use NULL (defaults to false)"
end)
let () = add_correctness_dep AllocatedContextValid.parameter
let () = AllocatedContextValid.add_aliases ["-context-valid-pointers"]
@@ -669,7 +674,7 @@ module HierarchicalConvergence =
(struct
let option_name = "-eva-hierarchical-convergence"
let help = "Experimental and unsound. Separate the convergence process \
- of each levels of nested loops. This implies that the convergence of \
+ of each level of nested loops. This implies that the convergence of \
inner loops will be completely recomputed when doing another iteration \
of the outer loops."
end)
@@ -711,7 +716,9 @@ module SemanticUnrollingLevel =
let option_name = "-eva-slevel"
let arg_name = "n"
let help =
- "superpose up to <n> states when unrolling control flow. The larger n, the more precise and expensive the analysis (defaults to 0)"
+ "superpose up to <n> states when unrolling control flow. \
+ The larger n, the more precise and expensive the analysis \
+ (defaults to 0)"
end)
let () = add_precision_dep SemanticUnrollingLevel.parameter
let () = SemanticUnrollingLevel.add_aliases ["-slevel"]
@@ -764,7 +771,7 @@ module MinLoopUnroll =
let help =
"unroll <n> loop iterations for each loop, regardless of the slevel \
settings and the number of states already propagated. \
- Can be overwritten on a case by case basis by loop unroll annotations."
+ Can be overwritten on a case-by-case basis by loop unroll annotations."
end)
let () = add_precision_dep MinLoopUnroll.parameter
let () = MinLoopUnroll.set_range 0 max_int
@@ -791,8 +798,8 @@ module DefaultLoopUnroll =
let arg_name = "n"
let default = 100
let help =
- "defines the default limit for loop unroll annotations that do\
- not explicitely provide a limit."
+ "defines the default limit for loop unroll annotations that do \
+ not explicitly provide a limit."
end)
let () = add_precision_dep DefaultLoopUnroll.parameter
let () = DefaultLoopUnroll.set_range 0 max_int
@@ -805,7 +812,7 @@ module HistoryPartitioning =
let arg_name = "n"
let default = 0
let help =
- "keep states distincts as long as the <n> last branching in their\
+ "keep states distinct as long as the <n> last branching in their \
traces are also distinct. (A value of 0 deactivates this feature)"
end)
let () = add_precision_dep HistoryPartitioning.parameter
@@ -868,7 +875,7 @@ module SplitReturn =
let arg_name = "mode"
let default = ""
let help = "when 'mode' is a number, or 'full', this is equivalent \
- to -val-split-return-function f:mode for all functions f. \
+ to -eva-split-return-function f:mode for all functions f. \
When mode is 'auto', automatically split states at the end \
of all functions, according to the function return code"
end)
@@ -1014,7 +1021,8 @@ module UsePrototype =
(struct
let option_name = "-eva-use-spec"
let arg_name = "f1,..,fn"
- let help = "use the ACSL specification of the functions instead of their definitions"
+ let help = "use the ACSL specification of the functions instead of \
+ their definitions"
end)
let () = add_precision_dep UsePrototype.parameter
let () = UsePrototype.add_aliases ["-val-use-spec"]
@@ -1036,7 +1044,8 @@ module RmAssert =
True
(struct
let option_name = "-eva-remove-redundant-alarms"
- let help = "after the analysis, try to remove redundant alarms, so that the user needs inspect fewer of them"
+ let help = "after the analysis, try to remove redundant alarms, \
+ so that the user needs to inspect fewer of them"
end)
let () = add_precision_dep RmAssert.parameter
let () = RmAssert.add_aliases ["-remove-redundant-alarms"]
@@ -1191,7 +1200,7 @@ module ValShowInitialState =
(* deprecated in Silicon *)
let help = "[deprecated] Show initial state before analysis starts. \
This option has been replaced by \
- -value-msg-key=[-]initial-state and has no effect anymore."
+ -eva-msg-key=[-]initial-state and has no effect anymore."
end)
let () =
ValShowInitialState.add_set_hook
@@ -1209,7 +1218,7 @@ module ValShowPerf =
False
(struct
let option_name = "-eva-show-perf"
- let help = "Compute and shows a summary of the time spent analyzing function calls"
+ let help = "Compute and show a summary of the time spent analyzing function calls"
end)
let () = ValShowPerf.add_aliases ["-val-show-perf"]