e-acsl-gcc.sh segmentation fault
Whenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
#include <stdio.h>
int main(void) {
printf ("is %d really an int?", "foo");
return 0;
}
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings print.c
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib print.c -e-acsl -e-acsl-validate-format-strings -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode a.out.frama.c
[kernel] Parsing print.c (with 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 print.c -o printf
+ gcc -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_VALIDATE_FORMAT_STRINGS -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 printf.e-acsl a.out.frama.c /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:~/Downloads/frama$ ./printf.e-acsl
Segmentation fault (core dumped)
The error in the printf.c file cannot be detected because a 'segmentation fault' has occurred.
The result of running gdb of ./printf.e-acsl is as follows.
(gdb) run
Starting program: /home/jaeyoung/Downloads/frama/printf.e-acsl
Program received signal SIGSEGV, Segmentation fault.
0x000055555555c1fa 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) bt
#0 0x000055555555c1fa 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
#1 0x000055555555e9bf in register_safe_locations (
thread_only=thread_only@entry=0)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c:720
#2 0x000055555555ea88 in do_eacsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:324
#3 0x000055555555ebd9 in __e_acsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:331
#4 0x0000555555557856 in main () at a.out.frama.c:243