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