--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Frama-C version: Fluorine



I'm very excited in finally having a new version of frama-c.

Installation went smooth, and the first thing I did was checking POs of the
project I'm currently am working on.

The new memory model seems powerfull, sadly I cannot prove a simple
function using alt-ergo (previously i could), and also cannot use why3 as
it returns an error related to unbound variables:

File "/Users/xxxxx/.frama-c-wp/typed/Axiomatic.why", line 16, characters
8-11: unused variable x_0

http://pastebin.com/JZHEskC5


Error while reading file '../typed/strlen_Why3_ide.why': File
"/Users/xxxxx/.frama-c-wp/project.session/../typed/strlen_Why3_ide.why",
line 36, characters 4-11: Unbound symbol 'addr_le'

http://pastebin.com/hxzBu0xw


function: http://pastebin.com/ahvWeYXh


-- 
Regards,
Cristiano Sousa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/3b2b5b7e/attachment.html>