--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on December 2013 ---
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>