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