--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RTE plugin: Standalone or File Output



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>