View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0002369 | Frama-C | Plug-in > E-ACSL | public | 2018-02-23 10:40 | 2018-02-23 17:37 | ||||||||
Reporter | jens | ||||||||||||
Assigned To | signoles | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | acknowledged | Resolution | open | ||||||||||
Product Version | Frama-C 16-Sulfur | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002369: e-acsl-gcc failes on macOS | ||||||||||||
Description | When 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 Information | This problem does not occur on my Linux installation. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
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 |
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. |
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 |
jens (reporter) 2018-02-23 11:35 |
I guess that part of the problem is that under macOS, clang is the default compiler. |
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. |
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 </usr/include/unistd.h> (it's already used in other e-acsl headers, so you won't introduce a new dependency here). |
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 |
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... |
![]() |
|||
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 |