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

[Frama-c-discuss] string functions and how to use jessie_prolog.h ?



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