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