--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on June 2009 ---
Hello, Le mer. 03 juin 2009 13:43:07 CEST, "Argenton Paolo" <Paolo.Argenton at elsagdatamat.com> a ?crit : > > What is the correct way to be able to use the valid_string predicate ? > (and of course strlen?) > > Should I modify the source code in order to include "Jessie_prolog" ? > What about the other headers ? don't they collide with standard headers > (eg. String.h) ? yes, you have to include the jessie/string.h file in order to use the valid_string predicate since it is defined here. The C prototypes declared there should conforming to the C standard, i.e. there should not be any clash. Generally speaking, including headers from the standard library is not really advised (except for the macros), since Frama-C won't know anything about the function declared there, and thus won't be able to tell something meaningful about code which uses them. Besides the jessie/*.h headers, other functions are available in the share directory of Frama-C (frama-c -print-path will give the exact location), usually under the form of a prototype with its specification and a reference implementation (which is better suited for the value analysis plugin). We have some plans to extend that to a sizable portion of the C standard library, feel free to suggest the functions that you are missing as candidates for a full specification. > > Second question (loosely related to the first one): > It seems to me that frama-c is more reliable in the Linux version rather > the windows one, do you suggest to use a Linux box ? > Frama-C is mainly developed under various unix-like environments (Mac OS X, Linux, BSD), but it should run on windows. What issues are you experiencing? Best regards, -- E tutto per oggi, a la prossima volta. Virgile