--- layout: fc_discuss_archives title: Message 14 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



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>