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: Julien.Signoles at cea.fr (Julien Signoles)
- Date: Thu, 13 Mar 2014 15:55:19 +0100
- In-reply-to: <20140312182447.GH20864@damazan>
- References: <524082A7.8080202@cea.fr> <20140312182447.GH20864@damazan>
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
- Follow-Ups:
- [Frama-c-discuss] WP Question/Bug?
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] WP Question/Bug?
- References:
- [Frama-c-discuss] E-ACSL v0.3
- From: Pierre-Loic.Garoche at onera.fr (Pierre-Loïc Garoche)
- [Frama-c-discuss] E-ACSL v0.3
- Prev by Date: [Frama-c-discuss] E-ACSL v0.3
- Next by Date: [Frama-c-discuss] WP: Pointer issue?
- Previous by thread: [Frama-c-discuss] E-ACSL v0.3
- Next by thread: [Frama-c-discuss] WP Question/Bug?
- Index(es):