Skip to content
Snippets Groups Projects
Commit 9fa55db4 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/rte/update-help-msg' into 'master'

[rte] Remove call site preconds from help msg

See merge request frama-c/frama-c!2620
parents 6c233a74 acee44d3
No related branches found
No related tags found
No related merge requests found
...@@ -20,8 +20,7 @@ ...@@ -20,8 +20,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
let help_msg = "generates annotations for runtime error checking and \ let help_msg = "generates annotations for runtime error checking"
preconditions at call sites"
include Plugin.Register include Plugin.Register
(struct (struct
......
...@@ -112,8 +112,7 @@ let _ = ...@@ -112,8 +112,7 @@ let _ =
~journalize:false ~journalize:false
Generator.emitter Generator.emitter
(* retrieve list of generated rte annotations (not precond) for (* retrieve list of generated rte annotations for a given stmt *)
a given stmt *)
let _ignore = let _ignore =
Dynamic.register Dynamic.register
~comment:"Get the list of annotations previously emitted by RTE for the \ ~comment:"Get the list of annotations previously emitted by RTE for the \
...@@ -149,8 +148,7 @@ let _ignore = ...@@ -149,8 +148,7 @@ let _ignore =
Visit.get_annotations_exp Visit.get_annotations_exp
let main () = let main () =
(* reset "rte generated"/"called precond generated" properties for all (* reset "rte generated" properties for all functions *)
functions *)
if Options.Enabled.get () then begin if Options.Enabled.get () then begin
Options.feedback ~level:2 "generating annotations"; Options.feedback ~level:2 "generating annotations";
!Db.RteGen.compute (); !Db.RteGen.compute ();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment