--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] E-ACSL v0.3



Dear frama-c-ists,

I tried to play with e-acsl. However I have some issues with memories. And the manual is not consistent with the libraries. 

For example, in page 24, section 3.2.1, you mention the need to call __e_acsl_memory_init and __e_acsl_memory_clean.
While the latter is in e-acsl/e_acsl_mmodel.h, the former does not appear anywhere.

I compiled separately a set of functions, instrumented with ACSL contracts and a main containing calls to scanf, printf, etc ...

When I run the binary, I have a set of warning "function initialize called with null pointers".
For some examples, even if the original source code seems to behave properly, the instrumented version fails:
mem_access: \valid_read(&__e_acsl_at_5->....)

If I tried to apply e-acsl plugin on the whole function (including the main with printf), I am not able to compile the code:
gcc complains: undefined reference to '__fc_stdout'

Last, I found difficult to understand e-acsl plugin error locations. For example, during the call to frama-c to preprocess the file, I have a warning "file.c:629:[e-acsl]: E-ACSL construct 'logic function application' is not yet supported". But I don't have any logic definitions and the line 629 is in the middle of a C function without annotations.

I hope my remarks/comments were helpful. I am interested by any feedback on them :)

Best regards,

pl

-- 
Pierre-Lo?c Garoche
Research Scientist @ ONERA
pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu
http://www.onera.fr/staff/pierre-loic-garoche/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140312/a6280a0c/attachment.pgp>