--- layout: fc_discuss_archives title: Message 14 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 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