--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on June 2009 ---
Hi to everybody listening on this list, First of all, thanks for your amazing work! I'm just learning frama-c / Jessie / why and all their friends and I decided to start with a little example: The (trivial) function should return TRUE if the string passed is composed only by blank chars, FALSE otherwise. So I started to think how to annotate it and wanted to use valid_string, but I did not find the way out, I did read some post and ref.manual about library functions but -sorry- I still don't get it. 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) ? 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 ? Thanks again and best regards Paolo Bashir Argenton #include <string.h> #include <stdio.h> etc.etc. /*@ requires valid_string(s); @ assigns \nothing; */ BOOL st_isblank( INP char * s ) { BOOL retval = TRUE; unsigned int i; for ( i=0; i<strlen(s); i++) { if ( NOT isspace( (unsigned char) s[i] ) ) { /* if at least 1 char is != blank ret false */ retval = FALSE; break; } } /* retval is TRUE if every char is isspace */ } return retval; }