E-ACSL: segmentation fault on a simple strlen function
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.
<pre>
#include <stddef.h>
#include <stdint.h>
#include <stdio.h>
/*@ 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;
}
</pre>
### 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](/uploads/8cc47a4d07786ef1a83cc2d83a9ef725/strlen.c)
issue