---
layout: fc_discuss_archives
title: Message 4 from Frama-C-discuss on May 2014
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Error on using pp-annot
- Subject: [Frama-c-discuss] Error on using pp-annot
- From: dmentre at linux-france.org (David MENTRE)
- Date: Mon, 12 May 2014 11:15:34 +0200
- In-reply-to: <alpine.LNX.2.03.1404282100020.600@dordowsky.de>
- References: <alpine.LNX.2.03.1403300940120.3220@strato.de> <CAOH62JhJErP1S-T80t6TTWDj4DB+89aGb3BHSNM3=vAKEJMz-Q@mail.gmail.com> <CAOH62JiriPFVqKf1-ynK_5BurCv8WR0kNDUECH-tG_4gSnvbBA@mail.gmail.com> <alpine.LNX.2.03.1403301438460.3899@dordowsky.de> <CAOH62JiHCiHPUJRidjsvkv_1USR_qsStz1CYgOPak+HM6MCnMw@mail.gmail.com> <alpine.LNX.2.03.1404012134240.617@dordowsky.de> <CAOH62JizN7SNKizysEWehbjhVY81sgsfnaO=LxnuPZ8cYc8Htw@mail.gmail.com> <alpine.LNX.2.03.1404072130160.567@dordowsky.de> <CAOH62JhQbCdgy9WDQ=aEUK6_EtkHj7q8Y5H=X1EwqdXgNu65og@mail.gmail.com> <alpine.LNX.2.03.1404282100020.600@dordowsky.de>
Le 28/04/2014 21:02, Frank Dordowsky a ?crit :
> 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?
Yes. You need to write down assumptions on which the analysis can work.
Please notice that Pascal's advice of using the Frama-C standard library
is there to avoid you to write part of those annotations (of course only
if your target system libraries have the same semantics).
Best regards,
david