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

[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