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
}