--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Precondition for user call (newbye question)



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;
}