Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] multiple ACSL contracts/declarations for onefunction definition

  • Subject: [Frama-c-discuss] multiple ACSL contracts/declarations for onefunction definition
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Fri, 1 Mar 2019 11:44:36 +0100
  • In-reply-to: <7875_1551276998_5C769BC5_7875_19700_1_1DB23E1C78E0A3418D38356B91D1E7410B6E07F9@EXDAG0-A1.intra.cea.fr>
  • References: <7875_1551276998_5C769BC5_7875_19700_1_1DB23E1C78E0A3418D38356B91D1E7410B6E07F9@EXDAG0-A1.intra.cea.fr>
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