Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002422Frama-CPlug-in > E-ACSLpublic2019-01-22 14:552019-01-23 10:35
Reporterrmalak 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusconfirmedResolutionopen 
Platformx86_64OSLinux 4.19 Ocaml 4.07.0OS VersionDebian Sid
Product VersionFrama-C 18-Argon 
Target VersionFrama-C 19-PotassiumFixed in Version 
Summary0002422: Can't use e-acsl on a dynamic library containing all the instrumentations
DescriptionHi !

main.c contains the entry point : the main function and is not instrumented by frama-c

it calls instrumented func.c (e-acsl.func.c containing the __e_acsl_memory_init call) compiled as a dynamic library libe-acsl.func.so

then the e-acsl code segfault at

e_acsl_segment_tracking.h:815
Steps To Reproduce$ make
rm -vf *.*o ./loader ./main *e-acsl*
frama-c -main func -variadic-no-translation -machdep gcc_x86_64 -c11 -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64" -no-frama-c-stdlib func.c -e-acsl-prepare -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-full-mmodel -then-last -print -ocode e-acsl.func.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing func.c (with preprocessing)
[rte] annotating function __bswap_16
[rte] annotating function __bswap_32
[rte] annotating function __bswap_64
[rte] annotating function __uint16_identity
[rte] annotating function __uint32_identity
[rte] annotating function __uint64_identity
[rte] annotating function func
[e-acsl] beginning translation.
[kernel:annot:missing-spec] :0: Warning:
  Neither code nor specification for function __builtin_bswap16, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
  Neither code nor specification for function __builtin_bswap32, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
  Neither code nor specification for function __builtin_bswap64, generating default assigns from the prototype
[kernel:annot:missing-spec] /usr/include/stdio.h:332: Warning:
  Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
gcc -shared -fPIC -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -std=c99 -m64 -O0 -g -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/jean/local-frama-c/share/frama-c/e-acsl/ -o libe-acsl.func.so e-acsl.func.c /home/jean/local-frama-c/share/frama-c/e-acsl/e_acsl_rtl.c /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-dlmalloc.a /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-gmp.a -lm
gcc -o main main.c -L. -le-acsl.func

LD_LIBRARY_PATH=:./ ./main
Segmentation fault
make: *** [Makefile:11: e-acsl-main-shared] Error 139
Additional InformationWhy the hell am I doing this ? :)

Contiki-NG is an IoT OS. It can be build as a firmware for several IoT devices, as a ELF for Linux x86/x86_64, and as a shared library loaded by the Java Cooja network simulator (with some JNI).

Before experimenting with dlopen in C and JNI in Java, which is going to fail because of the __executable_start symbol at ./share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:47

(this will the subject of another future post)

I would like to be able, as a first step, to use a e-acsl instrumented dynamic library used by a non-instrumented program (containing main or not).

I am open to a solution that eventually needs some change inside the C E-ACSL code.
TagsNo tags attached.
Attached Filestar file icon e-acsl-is-fun.tar [^] (10,240 bytes) 2019-01-22 14:55

- Relationships

-  Notes
(0006734)
rmalak (reporter)
2019-01-22 15:01

Be careful with the Makefile as the main target (all) will call the clean target which performs a :

rm -vf *.*o ./loader ./main *e-acsl*

so try the Makefile in a dedicated directory !
(0006736)
signoles (manager)
2019-01-23 10:35

See Section 3.3.1 ("Programs without Main") of the E-ACSL user manual. Actually this section could be improved: that is why I do not close this issue.

To sum up, you must call __e_acsl_memory_init at the beginning of the main and __e_acsl_memory_clean at the end.

Typically (for a 64-bit architecture):

====
int main() {
  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
  [...]
  __e_acsl_memory_clean();
  return 0;
}

=====

- Issue History
Date Modified Username Field Change
2019-01-22 14:55 rmalak New Issue
2019-01-22 14:55 rmalak Status new => assigned
2019-01-22 14:55 rmalak Assigned To => signoles
2019-01-22 14:55 rmalak File Added: e-acsl-is-fun.tar
2019-01-22 15:01 rmalak Note Added: 0006734
2019-01-23 10:35 signoles Note Added: 0006736
2019-01-23 10:35 signoles Status assigned => confirmed
2019-01-23 10:35 signoles Target Version => Frama-C 19-Potassium


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker