--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] string functions and how to use jessie_prolog.h ?



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