--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2019 ---
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?  Thanks,  Rod -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190722/d989fd69/attachment.html>