--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on June 2019 ---
Dear ACSL experts, Â 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: int capacity(int x); /*@ requires capacity(x) > 0; Â */ void do_something (const int x); Frama-C (18) says "unbound function capacity" on line 3. This seems like such a common pattern... why doesn't this work? Many thanks, Â Rod Chapman -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190614/de4c7e30/attachment.html>