--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on July 2019 ---
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