GitLab

I followed the user's manual, but the following result does not come out and 'Segmentation fault (core dumped)' occurs. I don't know what is the problem. (URL: https://frama-c.com/fc-plugins/e-acsl.html)

• expected result

• my result

jaeyoung@jaeyoung-VirtualBox:~/Documents$ e-acsl-gcc.sh -c -omonitored_first.i first.i
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib first.i -e-acsl -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode monitored_first.i
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:92: Warning: 
  unnamed fields are a C11 extension (use -c11 to avoid this warning)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body first.i -o a.out
+ gcc -DE_ACSL_SEGMENT_MMODEL -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/jaeyoung/.opam/default/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
jaeyoung@jaeyoung-VirtualBox:~/Documents$ ls
a.out         first.i          monitored_first.c  monitored_first.o  pow.i
a.out.e-acsl  format-string.c  monitored_first.i  no_main.i
jaeyoung@jaeyoung-VirtualBox:~/Documents$ ./a.out.e-acsl 
Segmentation fault (core dumped)

I checked it through gdb, can you tell me how to solve it?

jaeyoung@jaeyoung-VirtualBox:~/Documents$ gdb -q ./a.out.e-acsl 
Reading symbols from ./a.out.e-acsl...
(gdb) run
Starting program: /home/jaeyoung/Documents/a.out.e-acsl 

Program received signal SIGSEGV, Segmentation fault.
0x000055555555bf0a in shadow_alloca (ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, 
    size=size@entry=216)
    at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
302	      sec_shadow[j++] = size;
(gdb) info locals
i = 0
j = 1
k = 0
boundary = 216
prim_shadow = <optimized out>
prim_shadow_alt = 0x0
sec_shadow = 0x0
i = <optimized out>
j = 0
k = 0
(gdb)