--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on June 2015 ---
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