Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
  • From: Paolo.Argenton at elsagdatamat.com (Argenton Paolo)
  • Date: Wed, 3 Jun 2009 13:43:07 +0200
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;
}