--- layout: fc_discuss_archives title: Message 16 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 14/06/2019 14:48, Yannick Moy wrote:
> Similar to what you were used to in old SPARK.

Nope.. in SPARK2005, every executable function got an implicitly 
declared "proof function" (i.e. a "log function") for free... so it just 
worked...

  - Rod


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190614/95b1bdbf/attachment.html>