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 ?
- Subject: [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Wed, 3 Jun 2009 17:12:27 +0200
- In-reply-to: <67BE2A6FF7A6A842B489D513FC93962875776D@GRPGEPWMX0012.grptop.net>
- References: <67BE2A6FF7A6A842B489D513FC93962875776D@GRPGEPWMX0012.grptop.net>
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
- Follow-Ups:
- [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- From: Paolo.Argenton at elsagdatamat.com (Argenton Paolo)
- [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- References:
- [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- From: Paolo.Argenton at elsagdatamat.com (Argenton Paolo)
- [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- Prev by Date: [Frama-c-discuss] Jessie sort specification
- Next by Date: [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- Previous by thread: [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- Next by thread: [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
- Index(es):