--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to include standard header (e.g. string.h) in Frama-C Sodium?



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