--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on June 2009 ---
Hello Paolo, On Fri, Jun 5, 2009 at 11:33, Paolo Bashir Argenton<bashir1961 at gmail.com> wrote: > In the following code I got a warning with jessie-analysis in the > statement len=strlen(s). [...] > /*@ assigns \nothing; > ?@ requires valid_string(s); You should put "requires" *before* "assigns". Always keep order given in Frama-C manuals. Here is the code that does not produce any warning for me. Apparently, some goals are not proven but I haven't looked at them to understand why. You don't need to include "frama/include/jessie_prolog.h", use "-jessie-std-stubs" command line option instead. I'm using following command line: frama-c -jessie-analysis -jessie-atp alt-ergo -jessie-gui -jessie-std-stubs paolo-issue.c --start-- //#include "bool.h" #define TRUE 1 #define FALSE 0 #define BOOL int //#include "isspace.h" //#include "frama/include/jessie_prolog.h" #include "string.h" BOOL isnotspace(char c) { return c != ' '; } /*@ @ requires valid_string(s); assigns \nothing; @ behavior nullo: @ assumes strlen(s) == 0; @ ensures \result == \true; @ behavior not_blank: @ assumes strlen(s) > 0 && \exists int i ; 0 <= i < strlen(s) && ( (s[i]!=' ') && (s[i]!='\t') ); @ ensures \result == \false; @ behavior blank: @ assumes strlen(s) > 0 && \forall int i ; 0 <= i < strlen(s) && ( (s[i]==' ') || (s[i]!='\t') ); @ ensures \result == \true; */ BOOL st_isblank( const char *s ) { BOOL retval = TRUE; unsigned int i = 0; unsigned char ch; unsigned int len = 0; len = strlen(s); if( 0 == len ) return retval; /* true */ for ( i=0; i<len; i++) { /*@ assert i<=len; */ /*@ assert \valid(s+i); */ ch = (unsigned char) s[i]; if ( isnotspace( ch ) ) { /* se almeno 1 char e' != blank torna false */ retval = FALSE; return retval; } } return retval; } --end-- Yours, d.