From 95ec3228313fe308543131b8b8bfc101605b9588 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 15 Jan 2019 13:50:02 +0100
Subject: [PATCH] [rte] trivial annotations includes validation from syntaxical
rules
---
doc/rte/rte.tex | 3 +--
src/plugins/rte/options.ml | 8 +++++---
2 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex
index 65daa15731b..bea711914f6 100644
--- a/doc/rte/rte.tex
+++ b/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
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 0b629f7f994..5d780169596 100644
--- a/src/plugins/rte/options.ml
+++ b/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)
--
GitLab