Frama-C Bug Tracking System - Frama-C
View Issue Details
0002472Frama-CPlug-in > E-ACSLpublic2019-08-19 14:382019-08-22 08:58
evdenis 
signoles 
normalcrashalways
closedno change required 
Frama-C 19-Potassium 
 
0002472: E-ACSL: segmentation fault on a simple strlen function
E-ACSL successfully generates executable for this example and fails at runtime with segmentation fault error in shadow_alloca function at initialization stage.
#include 
#include 
#include 

/*@ requires \exists size_t i; s[i] == '\0' && \valid_read(s+(0..i));
    assigns \nothing;
    ensures s[\result] == '\0';
    ensures \forall size_t j; 0 <= j < \result ==> s[j] != '\0';
 */
size_t strlen(char *s)
{
	size_t len;

	/*@ loop invariant \forall size_t i; i < len ==> s[i] != '\0';
	    loop assigns len;
	    loop variant SIZE_MAX - len;
	 */
	for(len = 0; s[len] != '\0'; ++len);

	return len;
}

int main(int argc, char *argv[])
{
	for(int i = 0; i < argc; ++i) {
		printf("%s: %d\n", argv[i], strlen(argv[i]));
	}
	return 0;
}
$ e-acsl-gcc.sh -c ./strlen.c $ ./a.out.e-acsl [1] 26340 segmentation fault (core dumped) ./a.out.e-acsl
$ gdb ./a.out.e-acsl Temporary breakpoint 1, main (argc=1, argv=0x7fffffffd3e8) at a.out.frama.c:278 278 __e_acsl_memory_init(& argc,& argv,8UL); Program received signal SIGSEGV, Segmentation fault. shadow_alloca (ptr=ptr@entry=0x7fffffffd298, size=size@entry=8) at /home/work/.opam/framac/bin/../share/frama-c/e-acsl//segment_model/e_acsl_segment_tracking.h:562 562 prim_shadow[i] = (code << 2); main function could be simple. For example, fails also in this case: int main(void) { char *str = "0123456789"; printf("%s: %d\n", str, strlen(str)); return 0; }
No tags attached.
c strlen.c (606) 2019-08-19 14:38
https://bts.frama-c.com/file_download.php?file_id=1323&type=bug
Issue History
2019-08-19 14:38evdenisNew Issue
2019-08-19 14:38evdenisStatusnew => assigned
2019-08-19 14:38evdenisAssigned To => signoles
2019-08-19 14:38evdenisFile Added: strlen.c
2019-08-19 17:31signolesNote Added: 0006843
2019-08-22 08:58signolesStatusassigned => closed
2019-08-22 08:58signolesResolutionopen => no change required

Notes
(0006843)
signoles   
2019-08-19 17:31   
Redefining strlen is undefined behavior as explained in Section 7.1.3 (Reserved Identifiers) of the C standard. In this particular case, it may (or may not) lead to a crash depending on your system. On my laptop, it crashes if the E-ACSL-generated program is compiled with gcc 7.4 and -O2 (but it does not crash if compiled with the same compiler and -O1 or -Os). If you rename your function, your program should run as expected.