--- layout: fc_discuss_archives title: Message 19 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?



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>