Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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