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

[Frama-c-discuss] Help with using user-declared functions in preconditions



>  Perhaps you can help please? In languages like Eiffel, Ada or SPARK, I am used to being able to use user-defined functions in subsequent contracts. Like a Stack ADT, declaring an executable Boolean-valued function called "Empty", then saying "not Empty" in the precondition of my "Pop" function.
> 
> If I try to do that in ACSL, it fails... the simplest example I can come up with is:

Hi Rod,
You have to declare capacity as a logic function inside annotations. Similar to what you were used to in old SPARK.
Even if you already have a program function called capacity.

--
Yannick Moy, Senior Software Engineer, AdaCore



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190614/66ae8967/attachment.html>