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] Problem with strlen

Hello,

2015-02-10 21:12 GMT+01:00 Ian Blissard <iblissard at grammatech.com>:
> Hello Everyone,
>
> I have been trying to use the definitions provided by frama-c?s libc
> headers, and have encountered an issue with strlen (defined in
> __fc_string_axiomatic.h). I am using frama-c-Neon-20140301.

> [wp] warning: No definition for 'strlen' interpreted as reads nothing

> Deriving false is obviously problematic. Can someone help me figure out what
> I am doing incorrectly? Or is it possible there is some inconsistency in the
> definition of strlen?

The issue is in the warning emitted by WP. As a matter of fact,
specifications of __fc_string_axiomatic.h have been written mainly for
the Jessie plugin. On the contrary to Jessie, which IIRC is able to
infer (an overapproximation of) the memory locations a logic function
depends on by looking at the axioms defining it, WP just considers
strlen as a 'pure' logic function, that does not depend on the memory
state of the program. Hence strlen(str) is supposed to stay the same
throughout the execution of truncate. In order to fix this issue, you
can add 'reads s[0..]' at the end of the declaration of strlen in
__fc_string_axiomatic.h. unchanged will then become unprovable.

NB: vacuous is still proved: in this proof obligation, changed and
unchanged are taken as hypotheses, and obviously only one can be true

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile