--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2009 ---
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 !