--- layout: fc_discuss_archives title: Message 21 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 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.