--- layout: fc_discuss_archives title: Message 23 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 22/07/2019 15:31, Virgile Prevosto wrote:
> while adding /*@ assert content3: foo[3] == 0; */ just before assert 
> foo results in both proof obligations discharged in no time.

Hmm... most of my string literals are used exactly once as an actual 
parameter in a function call, so I really don't want to have to declare 
them all separately as named constants...

> 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.

That's odd.. I would think that such a common use case (i.e. "pass a 
string literal to (const char *)  formal parameter") would be very 
trivial indeed.  I note that valid_read_string(s) requires
   strlen(s) >= 0
but I would hope that a something like
   strlen("hello") >= 0
would be blown away without any user-supplied hints.

  - Rod