Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] E-ACSL v0.3
  • From: Pierre-Loic.Garoche at onera.fr (Pierre-Loïc Garoche)
  • Date: Wed, 12 Mar 2014 19:24:47 +0100
  • In-reply-to: <524082A7.8080202@cea.fr>
  • References: <524082A7.8080202@cea.fr>
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>