--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2014 ---
Hello Pierre-Lo?c, On 03/12/2014 07:24 PM, Pierre-Lo?c Garoche wrote: > 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. __e_acsl_memory_clean is in e-acsl/e_acsl_mmodel.h, while __e_acsl_memory_init is generated by E-ACSL and is not part of the memory library. In the case described in Section 3.2.1, you need to call both manually. I see no inconsistency here, but arguably I could clarify the doc. > 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". Look like a bug. Could you provide a reproducible (small) example and submit a bug report on the BTS? > 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->....) Idem. > 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' I tried to reproduce this issue with E-ACSL 0.4 on the following small example, but it works as expected. ===== #include "stdio.h" int main(void) { int x = 2; printf("x = %d\n", x); return 0; } ===== So, could you also provide a reproducible example that has not the expected behavior? > 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. That's right. The localisations of warnings in case of unsupported constructs are wrong. You can monitor this BTS entry related to this issue that I have just created : https://bts.frama-c.com/view.php?id=1692. > I hope my remarks/comments were helpful. I am interested by any feedback on them :) Thanks for your feedback. E-ACSL is still a young experimental plug-in: even if I do my best, it may still contain bugs/issues. Do not hesitate to report each of them. Thanks, Julien -- Researcher-engineer CEA LIST, Software Safety Labs tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr