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



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?
>
>  Thanks,
>
>   Rod
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190722/2f54c133/attachment-0001.html>