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