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

[Frama-c-discuss] [PROVENANCE INTERNET] Re: multiple ACSL contracts/declarations for onefunction definition



 I have some sympathy with the use case. However it seems not difficult to have one specification that is used for verifying the implementation of a function and a different specification that is used for invocations of a function, leading to untrustworthy overall result. 

- David
________________________________________
From: Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] on behalf of BAUDIN Patrick
Sent: Friday, March 01, 2019 11:44 AM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: [PROVENANCE  INTERNET] Re: [Frama-c-discuss] multiple ACSL contracts/declarations for onefunction definition

Le 27/02/2019 à 15:16, COK David a écrit :
> The ACSL manual says
> "A C function can be defined only once but declared several times. It
> is allowed to annotate each of these functions with contracts. These
> contracts are seen as a single contract with the union of the requires
> clauses and behaviors."
Yes, that could be usefull in some industrial context (fi.e. in order to
complete frama-c stblib).
> This seems problematic. Different contracts might be used in different
> places. If the same contract is present multiple times, at minimum
> ones gets repetition of identical clauses, and one is faced with
> combining lists of behaviors, some of which might have identical
> names. This can arise if a declaration in a .h has a contract and the
> .h is included multiple times.
In such cases, theses preprocessing directives are welcome
#ifndef CONTRACT_INCLUDED
/*@ contract */
#define CONTRACT_INCLUDED
#endif


-- Patrick Baudin

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss