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