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 </usr/include/unistd.h> (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 - 2018 MantisBT Team
Powered by Mantis Bugtracker