--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on August 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] preprocessing a file for E-ACSL



Did you try using "-ocode find_main.i"? It's the usual option to save 
the normalized source code produced by Frama-C, without having other 
messages redirected to the file. "-print" tells Frama-C to print the 
output, and "-ocode" tells Frama-C where to print it (stdout, by default).

On 24/08/2020 11:31, Gerlach, Jens wrote:
> Hello,
>
> I am using the following command line to preprocess/prepare an annotated C file for E-ACSL.
>
> 	frama-c -cpp-command 'gcc -C -E -I../.. -I../../Logic -I. ' -cpp-frama-c-compliant -pp-annot -no-unicode find_main.c -print > find_main.i
>
> In general, I am happy with the generated output, except that the first line reads
>
> 	[kernel] Parsing find_main.c (with preprocessing)
>
> How can I avoid that this line appears in the output?
> (I can of course filter it out with 'grep‘ but I assume that I am not using the Frama-C options quite correctly.)
>
> Thanks in advance.
>
> Jens
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/List
Software Reliability and Security Laboratory