Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002369Frama-CPlug-in > E-ACSLpublic2018-02-23 10:402018-02-23 17:37
Reporterjens 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002369: e-acsl-gcc failes on macOS
DescriptionWhen trying to process the example 'true.i' from http://frama-c.com/eacsl.html the `e-acsl-gcc.sh` script fails and reports e-acsl-gcc: fatal error: unexpected output of system getopt
Additional InformationThis problem does not occur on my Linux installation.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006532)
jens (reporter)
2018-02-23 10:42

The particular problem disappers after installing 'gnu-get-opt' via $ brew install gnu-getopt and $ brew link --force gnu-getopt However, then I receive the following error message e-acsl-gcc.sh -c true.i ++ frama-c -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 true.i -e-acsl -e-acsl-share=/Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c [kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl_gmp_api.h (with preprocessing) [kernel] syntax error at /usr/include/stdlib.h:147:28-37, before or at token: __compar 145 #endif /* !__DARWIN_NO_LONG_LONG */ 146 void *bsearch(const void *__key, const void *__base, size_t __nel, 147 size_t __width, int (* _Nonnull __compar)(const void *, const void *)); ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 148 void *calloc(size_t __count, size_t __size) __result_use_check __alloc_size(1,2); 149 div_t div(int, int) __pure2; [kernel] Frama-C aborted: invalid user input. e-acsl-gcc: fatal error: aborted by Frama-C
(0006533)
signoles (manager)
2018-02-23 11:18

It is indeed hard to make E-ACSL work fine under Mac OS and it should be better documented. The issue is that E-ACSL relies on the system libc, while the Mac OS libc contains several non-standard extensions that are not supported by the Frama-C kernel. A possible workaround is to rely on the Frama-C libc through option --frama-c-stdlib of e-acsl-gcc.sh.
(0006534)
jens (reporter)
2018-02-23 11:34

Thanks for pointing out this option to me. However, now there seems to be a problems further down the line (I understand that macOS is not a major platform for Frama-C ...) $ e-acsl-gcc.sh -c --frama-c-stdlib true.i ++ frama-c -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -frama-c-stdlib true.i -e-acsl -e-acsl-share=/Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.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 true.i (no preprocessing) [e-acsl] beginning translation. [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 true.i -o a.out clang: warning: optimization flag '-fno-merge-constants' is not supported [-Wignored-optimization-argument] warning: unknown warning option '-Wno-unused-but-set-variable'; did you mean '-Wno-unused-const-variable'? [-Wunknown-warning-option] 1 warning generated. ++ gcc -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -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/Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl/ -o a.out.e-acsl-segment a.out.frama.c /Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl//e_acsl_rtl.c /Users/jens/.opam/4.05.0/bin/../lib/libeacsl-dlmalloc.a /Users/jens/.opam/4.05.0/bin/../lib/libeacsl-gmp.a -lm clang: warning: optimization flag '-fno-merge-constants' is not supported [-Wignored-optimization-argument] clang: warning: optimization flag '-fno-merge-constants' is not supported [-Wignored-optimization-argument] warning: unknown warning option '-Wno-unused-but-set-variable'; did you mean '-Wno-unused-const-variable'? [-Wunknown-warning-option] 1 warning generated. warning: unknown warning option '-Wno-unused-but-set-variable'; did you mean '-Wno-unused-const-variable'? [-Wunknown-warning-option] In file included from /Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl//e_acsl_rtl.c:105: In file included from /Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl/segment_model/e_acsl_segment_mmodel.c:31: /Users/jens/.opam/4.05.0/bin/../share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:50:7: error: conflicting types for 'sbrk' void *sbrk(intptr_t increment); ^ /usr/include/unistd.h:587:7: note: previous declaration is here void *sbrk(int); ^ 1 warning and 1 error generated. e-acsl-gcc: fatal error: fail to compile/link instrumented code
(0006535)
jens (reporter)
2018-02-23 11:35

I guess that part of the problem is that under macOS, clang is the default compiler.
(0006536)
signoles (manager)
2018-02-23 11:49

It is true that E-ACSL has been almost not tested under Mac OS. I don't think that the issue comes from clang: under Ubuntu, using clang works fine (even if the compilation raises many warnings). The issue is the system's libc. For instance, the signature of sbrk is expected to be: void *sbrk(intptr_t); while, under Mac OS, it seems to be (from your error message): void *sbrk(int); Note that the sbrk's wikipedia page (https://en.wikipedia.org/wiki/Sbrk) indicates that this system call is only emulated under Mac OS... Conclusion: additional work is certainly required to be able to execute the code generated by E-ACSL under Mac OS.
(0006537)
virgile (developer)
2018-02-23 12:00

I don't think that /usr/include/unistd.h is installed by clang. You might be able to get it working by removing the offending prototype in e_acsl_shadow_layout.h, and replacing it by #include (it's already used in other e-acsl headers, so you won't introduce a new dependency here).
(0006538)
jens (reporter)
2018-02-23 13:03

Thanks for the advice. However, now there is a linking problem ... ... Undefined symbols for architecture x86_64: "___executable_start", referenced from: ___e_acsl_memory_init in e_acsl_rtl-08970e.o "_end", referenced from: ___e_acsl_memory_init in e_acsl_rtl-08970e.o ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) e-acsl-gcc: fatal error: fail to compile/link instrumented code
(0006539)
signoles (manager)
2018-02-23 17:37

It looks like that the undefined symbols are indeed Linux-specific. Hard to debug forward without the right OS...

- Issue History
Date Modified Username Field Change
2018-02-23 10:40 jens New Issue
2018-02-23 10:40 jens Status new => assigned
2018-02-23 10:40 jens Assigned To => signoles
2018-02-23 10:42 jens Note Added: 0006532
2018-02-23 11:18 signoles Note Added: 0006533
2018-02-23 11:19 signoles Status assigned => acknowledged
2018-02-23 11:34 jens Note Added: 0006534
2018-02-23 11:35 jens Note Added: 0006535
2018-02-23 11:49 signoles Note Added: 0006536
2018-02-23 12:00 virgile Note Added: 0006537
2018-02-23 13:03 jens Note Added: 0006538
2018-02-23 17:37 signoles Note Added: 0006539


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker