[rte] trivial annotations includes validation from syntaxical rules

doc/rte/rte.tex

@@ -875,8 +875,7 @@ left-values access \\
 \lstinline |-rte-float-to-int| & boolean (true) & Generate annotations for
 casts from floating-point to integer \\
 \hline
-\lstinline |-rte-trivial-annotations| & boolean (true) & Generate status for
-annotation through constant folding \\
+\lstinline |-rte-trivial-annotations| & boolean (true) & Generate all annotations even when they trivially hold \\
 \hline
 \lstinline |-rte-warn| & boolean (true) & Emit warning on broken annotations \\
 \hline

src/plugins/rte/options.ml

@@ -90,14 +90,16 @@ module DoPointerCall =
     end)
 
 (* uses results of basic constant propagation in order to check
-   validity / invalidity of generated assertions, emitting a status if possible
+   validity / invalidity of generated assertions, emitting a status if possible.
+   Notice that annotations that can be considered valid from syntaxical rules
+   are also considered as trivial.
 *)
 module Trivial =
   False
     (struct
       let option_name = "-rte-trivial-annotations"
-      let help = "generate annotations for constant expressions, even when \
-                  they trivially hold"
+      let help = "generate all annotations even when they trivially hold \
+                  (from evaluation of constant expressions, syntactical rules...)"
       (* if on, evaluates constants in order to check if assertions
          are trivially true / false *)
     end)