--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2015 ---
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