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