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] [PROVENANCE INTERNET] Re: multiple ACSL contracts/declarations for onefunction definition

  • Subject: [Frama-c-discuss] [PROVENANCE INTERNET] Re: multiple ACSL contracts/declarations for onefunction definition
  • From: David.COK at cea.fr (COK David)
  • Date: Fri, 1 Mar 2019 11:59:25 +0000
  • In-reply-to: <24587_1551437087_5C790D1F_24587_5269_1_76124e8f-05fc-9960-f62d-727fb7f00a6e@cea.fr>
  • References: <7875_1551276998_5C769BC5_7875_19700_1_1DB23E1C78E0A3418D38356B91D1E7410B6E07F9@EXDAG0-A1.intra.cea.fr>, <24587_1551437087_5C790D1F_24587_5269_1_76124e8f-05fc-9960-f62d-727fb7f00a6e@cea.fr>
 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