Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002472Frama-CPlug-in > E-ACSLpublic2019-08-19 14:382019-08-22 08:58
Reporterevdenis 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C 19-Potassium 
Target VersionFixed in Version 
Summary0002472: E-ACSL: segmentation fault on a simple strlen function
DescriptionE-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;
}
Steps To Reproduce$ e-acsl-gcc.sh -c ./strlen.c $ ./a.out.e-acsl [1] 26340 segmentation fault (core dumped) ./a.out.e-acsl
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; }
TagsNo tags attached.
Attached Filesc file icon strlen.c [^] (606 bytes) 2019-08-19 14:38 [Show Content]

- Relationships

-  Notes
(0006843)
signoles (manager)
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.

- Issue History
Date Modified Username Field Change
2019-08-19 14:38 evdenis New Issue
2019-08-19 14:38 evdenis Status new => assigned
2019-08-19 14:38 evdenis Assigned To => signoles
2019-08-19 14:38 evdenis File Added: strlen.c
2019-08-19 17:31 signoles Note Added: 0006843
2019-08-22 08:58 signoles Status assigned => closed
2019-08-22 08:58 signoles Resolution open => no change required


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker