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] Precondition for user call (newbye question)

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.