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: Paolo.Argenton at elsagdatamat.com (Argenton Paolo)
  • Date: Wed, 3 Jun 2009 17:44:40 +0200
  • In-reply-to: <20090603171227.74bb9b32@is005115>
  • References: <67BE2A6FF7A6A842B489D513FC93962875776D@GRPGEPWMX0012.grptop.net> <20090603171227.74bb9b32@is005115>
Hello Virgile,
Thanks for your answer;

>Generally speaking, including headers from the standard library is not
>really advised (except for the macros),

What I'm trying to do is to take some existing code, and starting to
write contract specifications for some functions, beginning from the
simplest ones, in order to learn something from this process.
In this scenario, of course, existing code is filled up with standard
header includes.

Maybe this is not the best approach to use in order to learn the
framework (frama-c, Jessie, provers etc.), I would like some hint about
that, since I have some expertise in C programming but I'm an absolute
beginner (and self taught) in formal methods and verification tools.

So my next step is to extract some simple function from working code
(which obviously I prefer not to mess up) and starting annotation
experiments in a separate environment.

I'll let you know, thanks again for your good work !