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

[Frama-c-discuss] Problem with strlen



Hello Everyone,

I have been trying to use the definitions provided by frama-c?s libc 
headers, and have encountered an issue with strlen (defined in 
__fc_string_axiomatic.h). I am using frama-c-Neon-20140301.

In the function below (also attached), everything is validated, which 
concludes false.
The first assertion is included to show the axiom strlen_pos_or_null 
applies, therefore strlen is 2.
I would expect that the assertion ?unchanged? does not validate, but 
this is not the case.

#include <string.h>

/*@
     requires valid_string(str);
     requires strlen(str) >= 5;
     assigns *(str+(0..strlen(str)));
*/
void truncate(char *str) {
    str[2] = '\0';
    //@ assert \forall integer j; 0<=j<2 ==> str[j] != '\0';
    //@ assert changed:      strlen{Here}(str) == 2;
    //@ assert unchanged:    strlen{Here}(str) >= 5;
    //@ assert vacuous:      \false;
}

The command I am using is:

frama-c -cpp-extra-args="-I${FRAMA_C_LIBC}" -wp -wp-rte strlen_contradict.c

where $FRAMA_C_LIBC is set to the frama-c-Neon-20140301/share/libc 
directory.

Output is:

[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function truncate
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'strlen' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'strncmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_truncate_assert_unchanged : Valid (25ms) (7)
[wp] [Alt-Ergo] Goal typed_truncate_assert_changed : Valid (41ms) (36)
[wp] [Alt-Ergo] Goal typed_truncate_assert : Valid (34ms) (20)
[wp] [Alt-Ergo] Goal typed_truncate_assert_rte_mem_access : Valid (31ms) 
(34)
[wp] [Qed] Goal typed_truncate_assert_vacuous : Valid
[wp] [Alt-Ergo] Goal typed_truncate_assign : Valid (Qed:1ms) (33ms) (42)
[wp] Proved goals:    6 / 6
      Qed:             1  (0ms-1ms)
      Alt-Ergo:        5  (25ms-41ms) (42)

Deriving false is obviously problematic. Can someone help me figure out 
what I am doing incorrectly? Or is it possible there is some 
inconsistency in the definition of strlen?

Thanks,
Ian

-------------- next part --------------
#include <string.h>

/*@
    requires valid_string(str);
    requires strlen(str) >= 5;
    assigns *(str+(0..strlen(str)));
*/
void truncate(char *str) {
   str[2] = '\0';
   //@ assert \forall integer j; 0<=j<2 ==> str[j] != '\0'; // True Valid
   //@ assert changed:      strlen{Here}(str) == 2;         // True Valid
   //@ assert unchanged:    strlen{Here}(str) >= 5;         // False Valid
   //@ assert vacuous:      \false;                         // False Valid
}