--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2019 ---
Hello, You can try frama-c -rte files.c -print -ocode annotated_file.i Hope this helps, Benjamin Monate TrustInSoft Founder&CTO Le 6 mars 2019 à 20:28, Rafael Bachmann <rafael.bachmann.93 at gmail.com<mailto:rafael.bachmann.93 at gmail.com>> a écrit : Hello, I was wondering whether the RTE plugin can be used on its own. What I am looking for is something like: frama-c -rte file.c -output annotated_file.c which would write the generated assertions to annotated_file.c. The manual<https://frama-c.com/download/frama-c-rte-manual.pdf> does not mention any flag for that purpose. As it stands, the annotations have to be copy-pasted from frama-c-gui. Is there something I am overlooking here? I know that this is not at all the primary purpose of RTE, but I think this would be useful as a standalone tool. Thanks a lot, Rafael Bachmann _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190306/b23a093f/attachment.html>