--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2014 ---
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>