--- layout: fc_discuss_archives title: Message 9 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 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 !