--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on February 2015 ---
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 }