Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Error on using pp-annot

On Mon, Apr 7, 2014 at 9:31 PM, Frank Dordowsky <frank at dordowsky.de> wrote:

> I have tried clang and it seems to work. I also could reduce the
> number of options of the command. This is my command now:
>
>  frama-c -cpp-command 'clang -C -E -I.' -wp -wp-rte -pp-annot constant.c
>
>
You should still use -cpp-extra-args=-nostdinc -cpp-extra-args=-I`frama-c
-print-share-path`/libc .

Just because it happens to work on the simple example you initially set out
to parse does not mean that using the compiler-provided headers is a good
idea.

In other words:

The headers on the left are designed to work with another compiler and if
they were ever shown a formal annotation, they weren't looking. The headers
on the right contain ACSL specifications for a large number of standard
library functions. Which ones do you want to use for your analyses?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140418/a2fce29d/attachment.html>