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] problem with \strlen and \offset constructs

  • Subject: [Frama-c-discuss] problem with \strlen and \offset constructs
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Mon, 2 Dec 2013 23:12:11 -0500
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>