diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml index d46193ae8e0cac9c12209bd96f17bd456a06d528..e5ad90472cfc4dd5a71691dbb0acc58a811c234d 100644 --- a/src/plugins/rte/options.ml +++ b/src/plugins/rte/options.ml @@ -20,8 +20,7 @@ (* *) (**************************************************************************) -let help_msg = "generates annotations for runtime error checking and \ - preconditions at call sites" +let help_msg = "generates annotations for runtime error checking" include Plugin.Register (struct diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml index a3f3df56f048d270e2bdb4ede38ae8cac65c1646..cb4f763b97e52d084b722c3e6422f778ad03e0e7 100644 --- a/src/plugins/rte/register.ml +++ b/src/plugins/rte/register.ml @@ -112,8 +112,7 @@ let _ = ~journalize:false Generator.emitter -(* retrieve list of generated rte annotations (not precond) for - a given stmt *) +(* retrieve list of generated rte annotations for a given stmt *) let _ignore = Dynamic.register ~comment:"Get the list of annotations previously emitted by RTE for the \ @@ -149,8 +148,7 @@ let _ignore = Visit.get_annotations_exp let main () = - (* reset "rte generated"/"called precond generated" properties for all - functions *) + (* reset "rte generated" properties for all functions *) if Options.Enabled.get () then begin Options.feedback ~level:2 "generating annotations"; !Db.RteGen.compute ();