--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2015 ---
Hello David, 2015-06-03 16:06 GMT+02:00 David MENTRE <dmentre at linux-france.org>: > Hello, > > I have attached C code, including <string.h> and calling strcpy(). I would > like to prove this kind of code using WP. > > I use the following command line: > frama-c -frama-c-stdlib -wp -wp-rte string_use.c > > However, I get following warnings: > """ > [wp] warning: No definition for 'memchr' interpreted as reads nothing > [wp] warning: No definition for 'strlen' interpreted as reads nothing > [wp] warning: No definition for 'memset' interpreted as reads nothing > [wp] warning: No definition for 'strchr' interpreted as reads nothing > [wp] warning: No definition for 'strcmp' interpreted as reads nothing > [wp] warning: No definition for 'strncmp' interpreted as reads nothing > [wp] warning: No definition for 'wcscmp' interpreted as reads nothing > [wp] warning: No definition for 'wcslen' interpreted as reads nothing > [wp] warning: No definition for 'wcsncmp' interpreted as reads nothing > """ > > How should I call Frama-C Sodium to avoid those warnings? > > From my understanding of §5.1 of User manual, -frama-c-stdlib should be > enough. In FRAMAC_SHARE/libc/string.h (including __fc_string_axiomatic.h), > all the needed function contracts are defined (e.g. memchr()). > In fact, you don't need -frama-c-stdlib, as it is the default for Sodium (you have to use the negated option -no-frama-c-stdlib if you want to use another stdlib, e.g. the one installed on your system). However, it looks like we overlook something in the distribution: contrary to jessie, wp does not try to infer the memory locations a predicate defined axiomatically depends upon (jessie does that by inspecting the axioms that are declared in the same axiomatic block as the predicate). When wp encounters a predicate/logic function which is only declared, and does not have a reads clause, it emits this warning and considers that the predicate is pure (i.e. its truth value is independent from any C memory state). Fortunately, in the case of __fc_string_axiomatic.h, the reads clause are present, but commented out. If you uncomment them (and remove the semi-column before them), you should be able to get WP correctly interpret these predicates. Best regards, -- E tutto per oggi, a la prossima volta Virgile