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] Why does a string literal not satisfy valid_read_string?

Hello,

Le lun. 22 juil. 2019 à 16:12, Roderick Chapman <rod at proteancode.com> a
écrit :

> I have also just tried (having RTFM) the -wp-literals options and this
> seems to have no affect.
>
> Can anyone explain what I am doing wrong please?
>  Thanks,
>   Rod
>
>
> On 22/07/2019 11:04, Roderick Chapman wrote:
>
> On 18/07/2019 09:00, Roderick Chapman wrote:
>
>  I possibly silly question. The the code below - I get an unproved VC for
> the precondition of the call to "d2".  So.. why is a string literal not
> considered to satisfy "valid_read_string"?? I am using Frama-C 19...
>
> With a bit more experimenting, I find that a string literal satisifies
> "valid_read" but not "valid_read_string".  Can anyone please explain this?
>
>
>
>
Indeed, -wp-literals should have worked. It seems that automated provers
are missing a trigger or two, though: the following code result in a
timeout with frama-c -wp -wp-literals file.c

#include "string.h"

void f(void) {
  const char* const foo = "foo";
    /*@ assert foo: valid_read_string(foo); */
}

while adding /*@ assert content3: foo[3] == 0; */ just before assert foo
results in both proof obligations discharged in no time. This suggests that
the file given to Alt-Ergo in the original case doesn't give enough hints
to the prover that it would be a good idea to check the content of the
array when dealing with valid_read_string. Finding the appropriate set of
such hints is largely empirical and not trivial.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190722/d23c6a3d/attachment.html>