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