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
- Subject: [Frama-c-discuss] Problem with strlen
- From: iblissard at grammatech.com (Ian Blissard)
- Date: Tue, 10 Feb 2015 15:12:10 -0500
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 }
- Follow-Ups:
- [Frama-c-discuss] Problem with strlen
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Problem with strlen
- Prev by Date: [Frama-c-discuss] Frama-C related postdoc positions at CEA LIST
- Next by Date: [Frama-c-discuss] polymorphic logic types and the use of type parameters?
- Previous by thread: [Frama-c-discuss] Frama-C related postdoc positions at CEA LIST
- Next by thread: [Frama-c-discuss] Problem with strlen
- Index(es):