diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml index 5d7801695966c21eddbaee91d44e0038a33ea650..fb4af071484d6bbe03bdc79e8e543ffbfdda0d5f 100644 --- a/src/plugins/rte/options.ml +++ b/src/plugins/rte/options.ml @@ -98,7 +98,7 @@ module Trivial = False (struct let option_name = "-rte-trivial-annotations" - let help = "generate all annotations even when they trivially hold \ + let help = "generate all annotations even if they trivially hold \ (from evaluation of constant expressions, syntactical rules...)" (* if on, evaluates constants in order to check if assertions are trivially true / false *) diff --git a/tests/rte/bool.i b/tests/rte/bool.i index 070a9fbcaf83ae4e600e7128a0cdf52760e9c47e..4c0f20d8595943bbabac9f0bbc3823d3cf308e39 100644 --- a/tests/rte/bool.i +++ b/tests/rte/bool.i @@ -2,7 +2,7 @@ OPT: -warn-invalid-bool -rte -print -then -rte-trivial-annotations -rte -print */ -/* The test asks for two execution of RTE plug-in: +/* The test asks for two executions of RTE plug-in: - a first one without trivial annotations (default behavior) - a second one with trivial annotations (-rte-trivial-annotations) */