--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2019 ---
[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>