--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2019 ---
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