GitLab

ID0002472: This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002472	Frama-C	Plug-in > E-ACSL	public	2019-08-19	2019-08-22

Reporter	evdenis	Assigned To	signoles	Resolution	no change required
Priority	normal	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C 19-Potassium	Target Version	-	Fixed in Version	-

Description :

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;
}

Additional Information :

$ 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; }

Steps To Reproduce :

$ e-acsl-gcc.sh -c ./strlen.c $ ./a.out.e-acsl [1] 26340 segmentation fault (core dumped) ./a.out.e-acsl

Attachments

• strlen.c