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



On 15/06/2019 11:15, Gerlach, Jens wrote:
> The code of the examples and the various logic functions and predicates can be found under
>
> 	https://github.com/fraunhoferfokus/acsl-by-example

OK..got it... you define a predicate called "Empty" and use that in the 
"ensures" clause of the "stack_empty" function... which can then be used 
in the preconditions of other functions...

>  From time to time I hear the Frama-C developers talk about the idea of allowing “pure” C functions
> (no side effects etc) in contracts. However, this hasn’t materialized yet.
>
Ah...of course...in SPARK, functions are always pure, so using them 
directly in contracts is always OK...

  Thanks for the help,

  Rod