--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with \strlen and \offset constructs



Hi all,
  As I specify loop invariant and variant for string compare function taken from C library,
  The \offset construct make jessie fail:
  szos_strcmp.c:79:[jessie] failure: logic offset
[jessie] user error: Unsupported feature(s).

  I tried \strlen for loop invariant:
 \forall integer k: 0<=k<\strlen(s1) ==> s1[k]==s2[k];
  
[kernel] user error: unbound function \strlen in annotation.

   Any idea on how to use these build-in construct correctly?

cheers

xiao-lei

-------------------------------------------------------------------------------------
INT szos_strcmp
    (
    const schar * s1,   /* string to compare */
    const schar * s2    /* string to compare <s1> to */
    )
    { 

      if ((NULL==s1)&&(NULL==s2))
        {
           return (0);
        }
        if (NULL==s1)
        {
           return ((INT)(0 - *s2 ));
        }
        if (NULL==s2)
        {
           return ((INT)(*s1 - 0 ));
        }

        //@   loop invariant \offset(s1) == \offset(s2);
        //@   loop variant \block_length(s2)-\offset(s2);
       while (*s1++ == *s2++)
        {
                if ((*(s1-1))== ((schar)EOS))
                {
                    return (0);
                }
        }
       //@assert !(*s1 == *s2);
       ;     
         return ((INT)(*(s1 -1) -*(s2 -1)));
    }


 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131202/c09a33c4/attachment.html>