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 Virgile,

Le 03/06/2015 17:47, Virgile Prevosto a écrit :
> In fact, you don't need -frama-c-stdlib, as it is the default for
> Sodium

Yes I knew it, but just in case... :-) BTW, the default to Frama-C 
stdlib is a very good idea in my humble opinion.

> 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).

OK.

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

Thanks for the tip. After editing the __fc_string_axiomatic.h, it works.

Thanks for the quick response!
Best regards,
david