--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on June 2009 ---
Hello everybody, hope I don't bother you with "newbye" questions; In the following code I got a warning with jessie-analysis in the statement len=strlen(s). Shouldn't it be already assumed ok by the precondition requires valid_string(s) ? Am I missing something ? thanks again Paolo Bashir Argenton #include "bool.h" #include "isspace.h" #include "framainclude/jessie_prolog.h" #include "framainclude/string.h" /*@ assigns \nothing; @ requires valid_string(s); @ 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; }