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] 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