--- layout: fc_discuss_archives title: Message 6 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



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