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

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



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."

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.

It seems better to follow the spirit of the ODR: If multiple declarations each have ACSL contracts, those contracts must be token-identical. Tools can pick one to use; as in the ODR, tools may not be obligated to report violations of this rule.

Comments?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190227/5dc6a88c/attachment.html>