--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



Hello Pascal,
I think I will follow your advice and will use the annotated
libraries. I understand that whenever I am going to use standard
libraries I should replace these with the annotated ones.

In my example, I will probably not use standard libraries because my
example is from a safety domain and standard libraries are considered
with concern.

In the embedded domain, we are using sometimes specific compilers that
come with specific libraries. In that case, do I have to annotate them
myself in order to make analysis work?

Frank


On Fri, 18 Apr 2014, Pascal Cuoq wrote:

> 
> 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?
> 
>