diff --git a/share/dune b/share/dune index bdd583e6b68b38004b122a7db94f97394417c184..4b6e152618066869404b4cfdd5cf715aa41b7191 100644 --- a/share/dune +++ b/share/dune @@ -23,297 +23,32 @@ (install (package frama-c) (section (site (frama-c share))) + (source_trees compliance emacs theme libc) (files -; Auto-Complete -(autocomplete_frama-c as autocomplete_frama-c) -(_frama-c as _frama-c) -; Emacs -(emacs/frama-c-init.el as emacs/frama-c-init.el) -(emacs/frama-c-dev.el as emacs/frama-c-dev.el) -(emacs/frama-c-recommended.el as emacs/frama-c-recommended.el) -(emacs/acsl.el as emacs/acsl.el) -; Useful Makefiles -(Makefile.common as Makefile.common) -(Makefile.headers as Makefile.headers) -(Makefile.linting as Makefile.linting) -(Makefile.installation as Makefile.installation) -(Makefile.testing as Makefile.testing) -; GUI Images -(frama-c.ico as frama-c.ico) -(frama-c.png as frama-c.png) -(unmark.png as unmark.png) -(switch-on.png as switch-on.png) -(switch-off.png as switch-off.png) -; Default theme -(theme/default/never_tried.png as theme/default/never_tried.png) -(theme/default/unknown.png as theme/default/unknown.png) -(theme/default/surely_valid.png as theme/default/surely_valid.png) -(theme/default/surely_invalid.png as theme/default/surely_invalid.png) -(theme/default/considered_valid.png as theme/default/considered_valid.png) -(theme/default/valid_under_hyp.png as theme/default/valid_under_hyp.png) -(theme/default/invalid_under_hyp.png as theme/default/invalid_under_hyp.png) -(theme/default/invalid_but_dead.png as theme/default/invalid_but_dead.png) -(theme/default/unknown_but_dead.png as theme/default/unknown_but_dead.png) -(theme/default/valid_but_dead.png as theme/default/valid_but_dead.png) -(theme/default/inconsistent.png as theme/default/inconsistent.png) -(theme/default/fold.png as theme/default/fold.png) -(theme/default/unfold.png as theme/default/unfold.png) -; Colorblind theme -(theme/colorblind/never_tried.png as theme/colorblind/never_tried.png) -(theme/colorblind/unknown.png as theme/colorblind/unknown.png) -(theme/colorblind/surely_valid.png as theme/colorblind/surely_valid.png) -(theme/colorblind/surely_invalid.png as theme/colorblind/surely_invalid.png) -(theme/colorblind/considered_valid.png as theme/colorblind/considered_valid.png) -(theme/colorblind/valid_under_hyp.png as theme/colorblind/valid_under_hyp.png) -(theme/colorblind/invalid_under_hyp.png as theme/colorblind/invalid_under_hyp.png) -(theme/colorblind/invalid_but_dead.png as theme/colorblind/invalid_but_dead.png) -(theme/colorblind/unknown_but_dead.png as theme/colorblind/unknown_but_dead.png) -(theme/colorblind/valid_but_dead.png as theme/colorblind/valid_but_dead.png) -(theme/colorblind/inconsistent.png as theme/colorblind/inconsistent.png) -(theme/colorblind/fold.png as theme/colorblind/fold.png) -(theme/colorblind/unfold.png as theme/colorblind/unfold.png) -; Flat theme -(theme/flat/never_tried.png as theme/flat/never_tried.png) -(theme/flat/unknown.png as theme/flat/unknown.png) -(theme/flat/surely_valid.png as theme/flat/surely_valid.png) -(theme/flat/surely_invalid.png as theme/flat/surely_invalid.png) -(theme/flat/considered_valid.png as theme/flat/considered_valid.png) -(theme/flat/valid_under_hyp.png as theme/flat/valid_under_hyp.png) -(theme/flat/invalid_under_hyp.png as theme/flat/invalid_under_hyp.png) -(theme/flat/invalid_but_dead.png as theme/flat/invalid_but_dead.png) -(theme/flat/unknown_but_dead.png as theme/flat/unknown_but_dead.png) -(theme/flat/valid_but_dead.png as theme/flat/valid_but_dead.png) -(theme/flat/inconsistent.png as theme/flat/inconsistent.png) -(theme/flat/fold.png as theme/flat/fold.png) -(theme/flat/unfold.png as theme/flat/unfold.png) -; Libc -(libc/__fc_alloc_axiomatic.h as libc/__fc_alloc_axiomatic.h) -(libc/__fc_builtin.c as libc/__fc_builtin.c) -(libc/__fc_builtin.h as libc/__fc_builtin.h) -(libc/__fc_define_blkcnt_t.h as libc/__fc_define_blkcnt_t.h) -(libc/__fc_define_blksize_t.h as libc/__fc_define_blksize_t.h) -(libc/__fc_define_clockid_t.h as libc/__fc_define_clockid_t.h) -(libc/__fc_define_dev_t.h as libc/__fc_define_dev_t.h) -(libc/__fc_define_eof.h as libc/__fc_define_eof.h) -(libc/__fc_define_fd_set_t.h as libc/__fc_define_fd_set_t.h) -(libc/__fc_define_fds.h as libc/__fc_define_fds.h) -(libc/__fc_define_file.h as libc/__fc_define_file.h) -(libc/__fc_define_fpos_t.h as libc/__fc_define_fpos_t.h) -(libc/__fc_define_fs_cnt.h as libc/__fc_define_fs_cnt.h) -(libc/__fc_define_id_t.h as libc/__fc_define_id_t.h) -(libc/__fc_define_ino_t.h as libc/__fc_define_ino_t.h) -(libc/__fc_define_intptr_t.h as libc/__fc_define_intptr_t.h) -(libc/__fc_define_iovec.h as libc/__fc_define_iovec.h) -(libc/__fc_define_key_t.h as libc/__fc_define_key_t.h) -(libc/__fc_define_locale_t.h as libc/__fc_define_locale_t.h) -(libc/__fc_define_max_open_files.h as libc/__fc_define_max_open_files.h) -(libc/__fc_define_mbstate_t.h as libc/__fc_define_mbstate_t.h) -(libc/__fc_define_mode_t.h as libc/__fc_define_mode_t.h) -(libc/__fc_define_nlink_t.h as libc/__fc_define_nlink_t.h) -(libc/__fc_define_null.h as libc/__fc_define_null.h) -(libc/__fc_define_off_t.h as libc/__fc_define_off_t.h) -(libc/__fc_define_pid_t.h as libc/__fc_define_pid_t.h) -(libc/__fc_define_pthread_types.h as libc/__fc_define_pthread_types.h) -(libc/__fc_define_sa_family_t.h as libc/__fc_define_sa_family_t.h) -(libc/__fc_define_seek_macros.h as libc/__fc_define_seek_macros.h) -(libc/__fc_define_sigset_t.h as libc/__fc_define_sigset_t.h) -(libc/__fc_define_size_t.h as libc/__fc_define_size_t.h) -(libc/__fc_define_sockaddr.h as libc/__fc_define_sockaddr.h) -(libc/__fc_define_ssize_t.h as libc/__fc_define_ssize_t.h) -(libc/__fc_define_stat.h as libc/__fc_define_stat.h) -(libc/__fc_define_suseconds_t.h as libc/__fc_define_suseconds_t.h) -(libc/__fc_define_time_t.h as libc/__fc_define_time_t.h) -(libc/__fc_define_timer_t.h as libc/__fc_define_timer_t.h) -(libc/__fc_define_timespec.h as libc/__fc_define_timespec.h) -(libc/__fc_define_timeval.h as libc/__fc_define_timeval.h) -(libc/__fc_define_uid_and_gid.h as libc/__fc_define_uid_and_gid.h) -(libc/__fc_define_useconds_t.h as libc/__fc_define_useconds_t.h) -(libc/__fc_define_wchar_t.h as libc/__fc_define_wchar_t.h) -(libc/__fc_define_wint_t.h as libc/__fc_define_wint_t.h) -(libc/__fc_gcc_builtins.h as libc/__fc_gcc_builtins.h) -(libc/__fc_inet.h as libc/__fc_inet.h) -(libc/__fc_integer.h as libc/__fc_integer.h) -(libc/__fc_libc.h as libc/__fc_libc.h) -(libc/__fc_runtime.c as libc/__fc_runtime.c) -(libc/__fc_select.h as libc/__fc_select.h) -(libc/__fc_string_axiomatic.h as libc/__fc_string_axiomatic.h) -(libc/__fc_utmp_constants.h as libc/__fc_utmp_constants.h) -(libc/aio.h as libc/aio.h) -(libc/alloca.h as libc/alloca.h) -(libc/argz.c as libc/argz.c) -(libc/argz.h as libc/argz.h) -(libc/arpa/inet.h as libc/arpa/inet.h) -(libc/assert.c as libc/assert.c) -(libc/assert.h as libc/assert.h) -(libc/byteswap.h as libc/byteswap.h) -(libc/complex.h as libc/complex.h) -(libc/cpio.h as libc/cpio.h) -(libc/ctype.c as libc/ctype.c) -(libc/ctype.h as libc/ctype.h) -(libc/dirent.h as libc/dirent.h) -(libc/dlfcn.h as libc/dlfcn.h) -(libc/endian.h as libc/endian.h) -(libc/err.h as libc/err.h) -(libc/errno.c as libc/errno.c) -(libc/errno.h as libc/errno.h) -(libc/error.c as libc/error.c) -(libc/error.h as libc/error.h) -(libc/fcntl.h as libc/fcntl.h) -(libc/features.h as libc/features.h) -(libc/fenv.c as libc/fenv.c) -(libc/fenv.h as libc/fenv.h) -(libc/float.h as libc/float.h) -(libc/fmtmsg.h as libc/fmtmsg.h) -(libc/fnmatch.h as libc/fnmatch.h) -(libc/ftw.h as libc/ftw.h) -(libc/getopt.h as libc/getopt.h) -(libc/glob.c as libc/glob.c) -(libc/glob.h as libc/glob.h) -(libc/grp.h as libc/grp.h) -(libc/iconv.h as libc/iconv.h) -(libc/ifaddrs.h as libc/ifaddrs.h) -(libc/inttypes.c as libc/inttypes.c) -(libc/inttypes.h as libc/inttypes.h) -(libc/iso646.h as libc/iso646.h) -(libc/langinfo.h as libc/langinfo.h) -(libc/libgen.h as libc/libgen.h) -(libc/limits.h as libc/limits.h) -(libc/locale.c as libc/locale.c) -(libc/locale.h as libc/locale.h) -(libc/malloc.h as libc/malloc.h) -(libc/math.c as libc/math.c) -(libc/math.h as libc/math.h) -(libc/memory.h as libc/memory.h) -(libc/monetary.h as libc/monetary.h) -(libc/mqueue.h as libc/mqueue.h) -(libc/ndbm.h as libc/ndbm.h) -(libc/net/if.h as libc/net/if.h) -(libc/netdb.c as libc/netdb.c) -(libc/netdb.h as libc/netdb.h) -(libc/netinet/in.c as libc/netinet/in.c) -(libc/netinet/in.h as libc/netinet/in.h) -(libc/netinet/ip.h as libc/netinet/ip.h) -(libc/netinet/tcp.h as libc/netinet/tcp.h) -(libc/nl_types.h as libc/nl_types.h) -(libc/poll.h as libc/poll.h) -(libc/pthread.h as libc/pthread.h) -(libc/pwd.c as libc/pwd.c) -(libc/pwd.h as libc/pwd.h) -(libc/regex.h as libc/regex.h) -(libc/resolv.h as libc/resolv.h) -(libc/sched.h as libc/sched.h) -(libc/search.h as libc/search.h) -(libc/semaphore.h as libc/semaphore.h) -(libc/setjmp.h as libc/setjmp.h) -(libc/signal.c as libc/signal.c) -(libc/signal.h as libc/signal.h) -(libc/spawn.h as libc/spawn.h) -(libc/stdalign.h as libc/stdalign.h) -(libc/stdarg.h as libc/stdarg.h) -(libc/stdatomic.c as libc/stdatomic.c) -(libc/stdatomic.h as libc/stdatomic.h) -(libc/stdbool.h as libc/stdbool.h) -(libc/stddef.h as libc/stddef.h) -(libc/stdint.h as libc/stdint.h) -(libc/stdio.c as libc/stdio.c) -(libc/stdio.h as libc/stdio.h) -(libc/stdlib.c as libc/stdlib.c) -(libc/stdlib.h as libc/stdlib.h) -(libc/stdnoreturn.h as libc/stdnoreturn.h) -(libc/string.c as libc/string.c) -(libc/string.h as libc/string.h) -(libc/strings.h as libc/strings.h) -(libc/stropts.h as libc/stropts.h) -(libc/sys/file.h as libc/sys/file.h) -(libc/sys/ioctl.h as libc/sys/ioctl.h) -(libc/sys/ipc.h as libc/sys/ipc.h) -(libc/sys/mman.h as libc/sys/mman.h) -(libc/sys/msg.h as libc/sys/msg.h) -(libc/sys/param.h as libc/sys/param.h) -(libc/sys/random.h as libc/sys/random.h) -(libc/sys/resource.h as libc/sys/resource.h) -(libc/sys/select.h as libc/sys/select.h) -(libc/sys/sem.h as libc/sys/sem.h) -(libc/sys/sendfile.h as libc/sys/sendfile.h) -(libc/sys/shm.h as libc/sys/shm.h) -(libc/sys/signal.h as libc/sys/signal.h) -(libc/sys/socket.c as libc/sys/socket.c) -(libc/sys/socket.h as libc/sys/socket.h) -(libc/sys/stat.h as libc/sys/stat.h) -(libc/sys/statvfs.h as libc/sys/statvfs.h) -(libc/sys/sysmacros.h as libc/sys/sysmacros.h) -(libc/sys/time.h as libc/sys/time.h) -(libc/sys/times.h as libc/sys/times.h) -(libc/sys/timex.h as libc/sys/timex.h) -(libc/sys/types.h as libc/sys/types.h) -(libc/sys/uio.h as libc/sys/uio.h) -(libc/sys/un.h as libc/sys/un.h) -(libc/sys/utsname.h as libc/sys/utsname.h) -(libc/sys/vfs.h as libc/sys/vfs.h) -(libc/sys/wait.h as libc/sys/wait.h) -(libc/syslog.h as libc/syslog.h) -(libc/tar.h as libc/tar.h) -(libc/termios.h as libc/termios.h) -(libc/tgmath.h as libc/tgmath.h) -(libc/time.c as libc/time.c) -(libc/time.h as libc/time.h) -(libc/trace.h as libc/trace.h) -(libc/uchar.h as libc/uchar.h) -(libc/ulimit.h as libc/ulimit.h) -(libc/unistd.c as libc/unistd.c) -(libc/unistd.h as libc/unistd.h) -(libc/utime.h as libc/utime.h) -(libc/utmp.h as libc/utmp.h) -(libc/utmpx.h as libc/utmpx.h) -(libc/wait.h as libc/wait.h) -(libc/wchar.c as libc/wchar.c) -(libc/wchar.h as libc/wchar.h) -(libc/wctype.h as libc/wctype.h) -(libc/wordexp.h as libc/wordexp.h) -; Compliance -(compliance/c11_functions.json as compliance/c11_functions.json) -(compliance/c11_headers.json as compliance/c11_headers.json) -(compliance/compiler_builtins.json as compliance/compiler_builtins.json) -(compliance/gcc_builtins.json as compliance/gcc_builtins.json) -(compliance/glibc_functions.json as compliance/glibc_functions.json) -(compliance/nonstandard_identifiers.json as compliance/nonstandard_identifiers.json) -(compliance/posix_identifiers.json as compliance/posix_identifiers.json) -)) + ; Auto-Complete + (autocomplete_frama-c as autocomplete_frama-c) + (_frama-c as _frama-c) + ; Useful Makefiles + (Makefile.common as Makefile.common) + (Makefile.headers as Makefile.headers) + (Makefile.linting as Makefile.linting) + (Makefile.installation as Makefile.installation) + (Makefile.testing as Makefile.testing) + ; GUI Images + (frama-c.ico as frama-c.ico) + (frama-c.png as frama-c.png) + (unmark.png as unmark.png) + (switch-on.png as switch-on.png) + (switch-off.png as switch-off.png))) ; Analysis scripts (executable files) (install (package frama-c) (section libexec) (files -(analysis-scripts/benchmark_database.py as lib/analysis-scripts/benchmark_database.py) -(analysis-scripts/bench-sqlite.sh as lib/analysis-scripts/bench-sqlite.sh) -(analysis-scripts/build_callgraph.py as lib/analysis-scripts/build_callgraph.py) -(analysis-scripts/build.py as lib/analysis-scripts/build.py) -(analysis-scripts/clone.sh as lib/analysis-scripts/clone.sh) -(analysis-scripts/cmd-dep.sh as lib/analysis-scripts/cmd-dep.sh) -(analysis-scripts/concat-csv.sh as lib/analysis-scripts/concat-csv.sh) -(analysis-scripts/creduce.sh as lib/analysis-scripts/creduce.sh) -(analysis-scripts/detect_recursion.py as lib/analysis-scripts/detect_recursion.py) -(analysis-scripts/estimate_difficulty.py as lib/analysis-scripts/estimate_difficulty.py) -(analysis-scripts/external_tool.py as lib/analysis-scripts/external_tool.py) -(analysis-scripts/fclog.py as lib/analysis-scripts/fclog.py) -(analysis-scripts/find_fun.py as lib/analysis-scripts/find_fun.py) -(analysis-scripts/flamegraph.pl as lib/analysis-scripts/flamegraph.pl) -(analysis-scripts/frama_c_results.py as lib/analysis-scripts/frama_c_results.py) -(analysis-scripts/function_finder.py as lib/analysis-scripts/function_finder.py) -(analysis-scripts/git_utils.py as lib/analysis-scripts/git_utils.py) -(analysis-scripts/heuristic_list_functions.py as lib/analysis-scripts/heuristic_list_functions.py) -(analysis-scripts/list_files.py as lib/analysis-scripts/list_files.py) -(analysis-scripts/make_wrapper.py as lib/analysis-scripts/make_wrapper.py) -(analysis-scripts/normalize_jcdb.py as lib/analysis-scripts/normalize_jcdb.py) -(analysis-scripts/parse-coverage.sh as lib/analysis-scripts/parse-coverage.sh) -(analysis-scripts/plot.sh as lib/analysis-scripts/plot.sh) -(analysis-scripts/print_callgraph.py as lib/analysis-scripts/print_callgraph.py) -(analysis-scripts/results_display.py as lib/analysis-scripts/results_display.py) -(analysis-scripts/script_for_creduce_fatal.sh as lib/analysis-scripts/script_for_creduce_fatal.sh) -(analysis-scripts/script_for_creduce_non_fatal.sh as lib/analysis-scripts/script_for_creduce_non_fatal.sh) -(analysis-scripts/source_filter.py as lib/analysis-scripts/source_filter.py) -(analysis-scripts/summary.py as lib/analysis-scripts/summary.py) + (glob_files (analysis-scripts/*.py with_prefix lib/analysis-scripts)) + (glob_files (analysis-scripts/*.sh with_prefix lib/analysis-scripts)) + (analysis-scripts/flamegraph.pl as lib/analysis-scripts/flamegraph.pl) )) ; Analysis scripts (non-executable files) @@ -321,16 +56,15 @@ (package frama-c) (section lib) (files -(analysis-scripts/analysis.mk as lib/analysis-scripts/analysis.mk) -(analysis-scripts/epilogue.mk as lib/analysis-scripts/epilogue.mk) -(analysis-scripts/fc_stubs.c as lib/analysis-scripts/fc_stubs.c) -(analysis-scripts/list_functions.ml as lib/analysis-scripts/list_functions.ml) -(analysis-scripts/prologue.mk as lib/analysis-scripts/prologue.mk) -(analysis-scripts/readme-graph.graphml as lib/analysis-scripts/readme-graph.graphml) -(analysis-scripts/readme-graph.svg as lib/analysis-scripts/readme-graph.svg) -(analysis-scripts/README.md as lib/analysis-scripts/README.md) -(analysis-scripts/template.mk as lib/analysis-scripts/template.mk) - + (analysis-scripts/analysis.mk as lib/analysis-scripts/analysis.mk) + (analysis-scripts/epilogue.mk as lib/analysis-scripts/epilogue.mk) + (analysis-scripts/fc_stubs.c as lib/analysis-scripts/fc_stubs.c) + (analysis-scripts/list_functions.ml as lib/analysis-scripts/list_functions.ml) + (analysis-scripts/prologue.mk as lib/analysis-scripts/prologue.mk) + (analysis-scripts/readme-graph.graphml as lib/analysis-scripts/readme-graph.graphml) + (analysis-scripts/readme-graph.svg as lib/analysis-scripts/readme-graph.svg) + (analysis-scripts/README.md as lib/analysis-scripts/README.md) + (analysis-scripts/template.mk as lib/analysis-scripts/template.mk) )) ; machdeps @@ -338,19 +72,8 @@ (package frama-c) (section share) (files - (machdeps/machdep_avr_8.yaml as share/machdeps/machdep_avr_8.yaml) - (machdeps/machdep_avr_16.yaml as share/machdeps/machdep_avr_16.yaml) - (machdeps/machdep_x86_16.yaml as share/machdeps/machdep_x86_16.yaml) - (machdeps/machdep_x86_32.yaml as share/machdeps/machdep_x86_32.yaml) - (machdeps/machdep_x86_64.yaml as share/machdeps/machdep_x86_64.yaml) - (machdeps/machdep_gcc_x86_16.yaml as share/machdeps/machdep_gcc_x86_16.yaml) - (machdeps/machdep_gcc_x86_32.yaml as share/machdeps/machdep_gcc_x86_32.yaml) - (machdeps/machdep_gcc_x86_64.yaml as share/machdeps/machdep_gcc_x86_64.yaml) - (machdeps/machdep_msvc_x86_64.yaml as share/machdeps/machdep_msvc_x86_64.yaml) - (machdeps/machdep_ppc_32.yaml as share/machdeps/machdep_ppc_32.yaml) - (machdeps/machdep-schema.yaml as share/machdeps/machdep-schema.yaml) - ) -) + (glob_files (machdeps/*.yaml with_prefix share/machdeps)) +)) ; machdep generation script (install @@ -365,56 +88,6 @@ (package frama-c) (section lib) (files - (machdeps/make_machdep/alignof_aligned.c as lib/make_machdep/alignof_aligned.c) - (machdeps/make_machdep/alignof_double.c as lib/make_machdep/alignof_double.c) - (machdeps/make_machdep/alignof_float.c as lib/make_machdep/alignof_float.c) - (machdeps/make_machdep/alignof_fun.c as lib/make_machdep/alignof_fun.c) - (machdeps/make_machdep/alignof_int.c as lib/make_machdep/alignof_int.c) - (machdeps/make_machdep/alignof_long.c as lib/make_machdep/alignof_long.c) - (machdeps/make_machdep/alignof_longdouble.c as lib/make_machdep/alignof_longdouble.c) - (machdeps/make_machdep/alignof_longlong.c as lib/make_machdep/alignof_longlong.c) - (machdeps/make_machdep/alignof_ptr.c as lib/make_machdep/alignof_ptr.c) - (machdeps/make_machdep/alignof_short.c as lib/make_machdep/alignof_short.c) - (machdeps/make_machdep/alignof_str.c as lib/make_machdep/alignof_str.c) - (machdeps/make_machdep/char_is_unsigned.c as lib/make_machdep/char_is_unsigned.c) - (machdeps/make_machdep/const_string_literals.c as lib/make_machdep/const_string_literals.c) - (machdeps/make_machdep/errno.c as lib/make_machdep/errno.c) - (machdeps/make_machdep/has__builtin_va_list.c as lib/make_machdep/has__builtin_va_list.c) - (machdeps/make_machdep/int_fast16_t.c as lib/make_machdep/int_fast16_t.c) - (machdeps/make_machdep/int_fast32_t.c as lib/make_machdep/int_fast32_t.c) - (machdeps/make_machdep/int_fast64_t.c as lib/make_machdep/int_fast64_t.c) - (machdeps/make_machdep/int_fast8_t.c as lib/make_machdep/int_fast8_t.c) - (machdeps/make_machdep/intptr_t.c as lib/make_machdep/intptr_t.c) - (machdeps/make_machdep/limits_macros.c as lib/make_machdep/limits_macros.c) - (machdeps/make_machdep/little_endian.c as lib/make_machdep/little_endian.c) + (glob_files (machdeps/make_machdep/*.c with_prefix lib/make_machdep)) (machdeps/make_machdep/make_machdep_common.h as lib/make_machdep/make_machdep_common.h) - (machdeps/make_machdep/nsig.c as lib/make_machdep/nsig.c) - (machdeps/make_machdep/posix_version.c as lib/make_machdep/posix_version.c) - (machdeps/make_machdep/ptrdiff_t.c as lib/make_machdep/ptrdiff_t.c) - (machdeps/make_machdep/sanity_check.c as lib/make_machdep/sanity_check.c) - (machdeps/make_machdep/sig_atomic_t.c as lib/make_machdep/sig_atomic_t.c) - (machdeps/make_machdep/sizeof_double.c as lib/make_machdep/sizeof_double.c) - (machdeps/make_machdep/sizeof_float.c as lib/make_machdep/sizeof_float.c) - (machdeps/make_machdep/sizeof_fun.c as lib/make_machdep/sizeof_fun.c) - (machdeps/make_machdep/sizeof_int.c as lib/make_machdep/sizeof_int.c) - (machdeps/make_machdep/sizeof_long.c as lib/make_machdep/sizeof_long.c) - (machdeps/make_machdep/sizeof_longdouble.c as lib/make_machdep/sizeof_longdouble.c) - (machdeps/make_machdep/sizeof_longlong.c as lib/make_machdep/sizeof_longlong.c) - (machdeps/make_machdep/sizeof_ptr.c as lib/make_machdep/sizeof_ptr.c) - (machdeps/make_machdep/sizeof_short.c as lib/make_machdep/sizeof_short.c) - (machdeps/make_machdep/sizeof_void.c as lib/make_machdep/sizeof_void.c) - (machdeps/make_machdep/size_t.c as lib/make_machdep/size_t.c) - (machdeps/make_machdep/ssize_t.c as lib/make_machdep/ssize_t.c) - (machdeps/make_machdep/stdio_macros.c as lib/make_machdep/stdio_macros.c) - (machdeps/make_machdep/stdlib_macros.c as lib/make_machdep/stdlib_macros.c) - (machdeps/make_machdep/time_t.c as lib/make_machdep/time_t.c) - (machdeps/make_machdep/uint_fast16_t.c as lib/make_machdep/uint_fast16_t.c) - (machdeps/make_machdep/uint_fast32_t.c as lib/make_machdep/uint_fast32_t.c) - (machdeps/make_machdep/uint_fast64_t.c as lib/make_machdep/uint_fast64_t.c) - (machdeps/make_machdep/uint_fast8_t.c as lib/make_machdep/uint_fast8_t.c) - (machdeps/make_machdep/uintptr_t.c as lib/make_machdep/uintptr_t.c) - (machdeps/make_machdep/wchar_t.c as lib/make_machdep/wchar_t.c) - (machdeps/make_machdep/weof.c as lib/make_machdep/weof.c) - (machdeps/make_machdep/wint_t.c as lib/make_machdep/wint_t.c) - (machdeps/make_machdep/wordsize.c as lib/make_machdep/wordsize.c) )) diff --git a/share/libc/__fc_machdep_linux_shared.h b/share/libc/__fc_machdep_linux_shared.h deleted file mode 100644 index 6f146ffb2baa1abd1b679b7d7b78d50b86cd7c70..0000000000000000000000000000000000000000 --- a/share/libc/__fc_machdep_linux_shared.h +++ /dev/null @@ -1,275 +0,0 @@ -/**************************************************************************/ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2024 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/**************************************************************************/ - -#ifndef __FC_FORCE_INCLUDE_MACHDEP__ -#error "Frama-C: This file shall not be directly included" -#endif -/* This file contains common machine specific values between - Linux x86 32-bit, AMD64 and x86 16-bit.*/ - -#ifndef __FC_MACHDEP_LINUX_SHARED -#define __FC_MACHDEP_LINUX_SHARED - -// These machdeps strive to conform themselves to POSIX.1-2008 -#define __FC_POSIX_VERSION 200809L - -/* Optional */ -#define __INT8_T signed char -#define __INT8_MIN __FC_SCHAR_MIN -#define __INT8_MAX __FC_SCHAR_MAX - -#define __UINT8_T unsigned char -#define __UINT8_MIN __FC_UCHAR_MAX - -#define __INT16_T signed short -#define __INT16_MIN __FC_SHRT_MIN -#define __INT16_MAX __FC_SHRT_MAX - -#define __UINT16_T unsigned short -#define __UINT16_MAX __FC_USHRT_MAX - -/* inttypes */ - -#define __PRI8_PREFIX "hh" -#define __PRI16_PREFIX "h" - -/* Required */ -#define __INT_LEAST8_T signed char -#define __INT_LEAST8_MIN __FC_SCHAR_MIN -#define __INT_LEAST8_MAX __FC_SCHAR_MAX - -#define __UINT_LEAST8_T unsigned char -#define __UINT_LEAST8_MAX __FC_UCHAR_MAX - -#define __INT_LEAST16_T signed short -#define __INT_LEAST16_MIN __FC_SHRT_MIN -#define __INT_LEAST16_MAX __FC_SHRT_MAX - -#define __UINT_LEAST16_T unsigned short -#define __UINT_LEAST16_MAX __FC_USHRT_MAX - -/* Required */ -#define __INT_FAST8_T signed char -#define __INT_FAST8_MIN __FC_SCHAR_MIN -#define __INT_FAST8_MAX __FC_SCHAR_MAX - -#define __UINT_FAST8_T unsigned char -#define __UINT_FAST8_MAX __FC_UCHAR_MAX - -#define __INT_FAST16_T signed int -#define __INT_FAST16_MIN __FC_INT_MIN -#define __INT_FAST16_MAX __FC_INT_MAX - -#define __UINT_FAST16_T unsigned int -#define __UINT_FAST16_MAX __FC_UINT_MAX -#define __PRIFAST16_PREFIX "" - -/* Required */ -#define __INT_MAX_T signed long long -#define __UINT_MAX_T unsigned long long - -#define __PRIMAX_PREFIX "ll" - -/* min and max values as specified in limits.h */ -#define __FC_SCHAR_MIN (-128) -#define __FC_SCHAR_MAX 127 -#define __FC_UCHAR_MAX 255 -#define __FC_SHRT_MIN (-32768) -#define __FC_SHRT_MAX 32767 -#define __FC_USHRT_MAX 65535 -#define __FC_LLONG_MIN (-9223372036854775807LL -1LL) -#define __FC_LLONG_MAX 9223372036854775807LL -#define __FC_ULLONG_MAX 18446744073709551615ULL -#define __FC_PATH_MAX 256 -// Note: POSIX requires HOST_NAME_MAX >= 255, but Linux uses 64 -#define __FC_HOST_NAME_MAX 64 -#define __FC_TTY_NAME_MAX 32 - -/* for stdarg.h */ -#define __FC_VA_LIST_T __builtin_va_list - -/* stdint.h */ -/* NB: in signal.h, sig_atomic_t is hardwired to int. */ -#define __FC_SIG_ATOMIC_MIN __FC_INT_MIN -#define __FC_SIG_ATOMIC_MAX __FC_INT_MAX -#define __FC_WCHAR_MIN __FC_INT_MIN -#define __FC_WCHAR_MAX __FC_INT_MAX -#define __FC_INTMAX_MIN (-9223372036854775807LL -1LL) -#define __FC_INTMAX_MAX 9223372036854775807LL -#define __FC_UINTMAX_MAX 18446744073709551615ULL - -/* stdio.h */ -#define __FC_BUFSIZ 8192 -#define __FC_EOF (-1) -#define __FC_FOPEN_MAX 16 -#define __FC_FILENAME_MAX 2048 -#define __FC_L_tmpnam 2048 -#define __FC_TMP_MAX 0xFFFFFFFF - -/* stdlib.h */ -#define __FC_RAND_MAX 32767 -#define __FC_MB_CUR_MAX ((size_t)16) - -/* errno.h */ -#define __FC_EPERM 1 -#define __FC_ENOENT 2 -#define __FC_ESRCH 3 -#define __FC_EINTR 4 -#define __FC_EIO 5 -#define __FC_ENXIO 6 -#define __FC_E2BIG 7 -#define __FC_ENOEXEC 8 -#define __FC_EBADF 9 -#define __FC_ECHILD 10 -#define __FC_EAGAIN 11 -#define __FC_ENOMEM 12 -#define __FC_EACCES 13 -#define __FC_EFAULT 14 -#define __FC_ENOTBLK 15 -#define __FC_EBUSY 16 -#define __FC_EEXIST 17 -#define __FC_EXDEV 18 -#define __FC_ENODEV 19 -#define __FC_ENOTDIR 20 -#define __FC_EISDIR 21 -#define __FC_EINVAL 22 -#define __FC_ENFILE 23 -#define __FC_EMFILE 24 -#define __FC_ENOTTY 25 -#define __FC_ETXTBSY 26 -#define __FC_EFBIG 27 -#define __FC_ENOSPC 28 -#define __FC_ESPIPE 29 -#define __FC_EROFS 30 -#define __FC_EMLINK 31 -#define __FC_EPIPE 32 -#define __FC_EDOM 33 -#define __FC_ERANGE 34 -#define __FC_EDEADLK 35 -#define __FC_ENAMETOOLONG 36 -#define __FC_ENOLCK 37 -#define __FC_ENOSYS 38 -#define __FC_ENOTEMPTY 39 -#define __FC_ELOOP 40 -#define __FC_EWOULDBLOCK EAGAIN -#define __FC_ENOMSG 42 -#define __FC_EIDRM 43 -#define __FC_ECHRNG 44 -#define __FC_EL2NSYNC 45 -#define __FC_EL3HLT 46 -#define __FC_EL3RST 47 -#define __FC_ELNRNG 48 -#define __FC_EUNATCH 49 -#define __FC_ENOCSI 50 -#define __FC_EL2HLT 51 -#define __FC_EBADE 52 -#define __FC_EBADR 53 -#define __FC_EXFULL 54 -#define __FC_ENOANO 55 -#define __FC_EBADRQC 56 -#define __FC_EBADSLT 57 -#define __FC_EDEADLOCK EDEADLK -#define __FC_EBFONT 59 -#define __FC_ENOSTR 60 -#define __FC_ENODATA 61 -#define __FC_ETIME 62 -#define __FC_ENOSR 63 -#define __FC_ENONET 64 -#define __FC_ENOPKG 65 -#define __FC_EREMOTE 66 -#define __FC_ENOLINK 67 -#define __FC_EADV 68 -#define __FC_ESRMNT 69 -#define __FC_ECOMM 70 -#define __FC_EPROTO 71 -#define __FC_EMULTIHOP 72 -#define __FC_EDOTDOT 73 -#define __FC_EBADMSG 74 -#define __FC_EOVERFLOW 75 -#define __FC_ENOTUNIQ 76 -#define __FC_EBADFD 77 -#define __FC_EREMCHG 78 -#define __FC_ELIBACC 79 -#define __FC_ELIBBAD 80 -#define __FC_ELIBSCN 81 -#define __FC_ELIBMAX 82 -#define __FC_ELIBEXEC 83 -#define __FC_EILSEQ 84 -#define __FC_ERESTART 85 -#define __FC_ESTRPIPE 86 -#define __FC_EUSERS 87 -#define __FC_ENOTSOCK 88 -#define __FC_EDESTADDRREQ 89 -#define __FC_EMSGSIZE 90 -#define __FC_EPROTOTYPE 91 -#define __FC_ENOPROTOOPT 92 -#define __FC_EPROTONOSUPPORT 93 -#define __FC_ESOCKTNOSUPPORT 94 -#define __FC_ENOTSUP 95 -#define __FC_EOPNOTSUPP 95 -#define __FC_EPFNOSUPPORT 96 -#define __FC_EAFNOSUPPORT 97 -#define __FC_EADDRINUSE 98 -#define __FC_EADDRNOTAVAIL 99 -#define __FC_ENETDOWN 100 -#define __FC_ENETUNREACH 101 -#define __FC_ENETRESET 102 -#define __FC_ECONNABORTED 103 -#define __FC_ECONNRESET 104 -#define __FC_ENOBUFS 105 -#define __FC_EISCONN 106 -#define __FC_ENOTCONN 107 -#define __FC_ESHUTDOWN 108 -#define __FC_ETOOMANYREFS 109 -#define __FC_ETIMEDOUT 110 -#define __FC_ECONNREFUSED 111 -#define __FC_EHOSTDOWN 112 -#define __FC_EHOSTUNREACH 113 -#define __FC_EALREADY 114 -#define __FC_EINPROGRESS 115 -#define __FC_ESTALE 116 -#define __FC_EUCLEAN 117 -#define __FC_ENOTNAM 118 -#define __FC_ENAVAIL 119 -#define __FC_EISNAM 120 -#define __FC_EREMOTEIO 121 -#define __FC_EDQUOT 122 -#define __FC_ENOMEDIUM 123 -#define __FC_EMEDIUMTYPE 124 -#define __FC_ECANCELED 125 -#define __FC_ENOKEY 126 -#define __FC_EKEYEXPIRED 127 -#define __FC_EKEYREVOKED 128 -#define __FC_EKEYREJECTED 129 -#define __FC_EOWNERDEAD 130 -#define __FC_ENOTRECOVERABLE 131 -#define __FC_ERFKILL 132 -#define __FC_EHWPOISON 133 - -/* time.h */ -#define __FC_TIME_T long - -/* signal.h */ -#define __FC_NSIG 65 -#define __FC__NSIG __FC_NSIG - -#endif diff --git a/share/libc/__fc_machdep_old.c b/share/libc/__fc_machdep_old.c deleted file mode 100644 index 46afd1d6fd3bffbadcc0797f2659d4b64bcde617..0000000000000000000000000000000000000000 --- a/share/libc/__fc_machdep_old.c +++ /dev/null @@ -1,796 +0,0 @@ -/**************************************************************************/ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2024 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/**************************************************************************/ - -#ifndef __FC_MACHDEP -#define __FC_MACHDEP - -#if defined(__FC_MACHDEP_X86_32) || defined(__FC_MACHDEP_GCC_X86_32) -#define __FC_FORCE_INCLUDE_MACHDEP__ -#include "__fc_machdep_linux_shared.h" -#undef __FC_FORCE_INCLUDE_MACHDEP__ -#define __FC_BYTE_ORDER __LITTLE_ENDIAN -/* Required */ -#undef __CHAR_UNSIGNED__ -#define __WORDSIZE 32 -#define __SIZEOF_SHORT 2 -#define __SIZEOF_INT 4 -#define __SIZEOF_LONG 4 -#define __SIZEOF_LONGLONG 8 -#define __CHAR_BIT 8 -#define __PTRDIFF_T int -#define __SIZE_T unsigned int -#define __WCHAR_T long -#define __FC_INT_MIN (-2147483647 - 1) -#define __FC_INT_MAX 2147483647 -#define __FC_UINT_MAX 4294967295U -#define __FC_LONG_MIN (-2147483647L - 1L) -#define __FC_LONG_MAX 2147483647L -#define __FC_ULONG_MAX 4294967295UL -#define __FC_SIZE_MAX __FC_UINT_MAX - -/* Optional */ -#define __INTPTR_T signed int -#define __FC_INTPTR_MIN __FC_INT_MIN -#define __FC_INTPTR_MAX __FC_INT_MAX - -#define __UINTPTR_T unsigned int -#define __FC_UINTPTR_MAX __FC_UINT_MAX - -#define __INT32_T signed int -#define __UINT32_T unsigned int -#define __INT64_T signed long long -#define __UINT64_T unsigned long long - -/* prefixes for inttypes */ -#define __PRI32_PREFIX "" -#define __PRI64_PREFIX "ll" -#define __PRIPTR_PREFIX "" - -/* Required */ -#define __INT_LEAST32_T signed int -#define __INT_LEAST32_MIN __FC_INT_MIN -#define __INT_LEAST32_MAX __FC_INT_MAX - -#define __UINT_LEAST32_T unsigned int -#define __UINT_LEAST32_MAX __FC_UINT_MAX - -#define __INT_LEAST64_T signed long long -#define __INT_LEAST64_MIN __FC_LLONG_MIN -#define __INT_LEAST64_MAX __FC_LLONG_MAX - -#define __UINT_LEAST64_T unsigned long long -#define __UINT_LEAST64_MAX __FC_ULLONG_MAX - -#define __INT_FAST32_T signed int -#define __INT_FAST32_MIN __FC_INT_MIN -#define __INT_FAST32_MAX __FC_INT_MAX - -#define __UINT_FAST32_T unsigned int -#define __UINT_FAST32_MAX __FC_UINT_MAX - -#define __INT_FAST64_T signed long long -#define __INT_FAST64_MIN __FC_LLONG_MIN -#define __INT_FAST64_MAX __FC_LLONG_MAX - -#define __UINT_FAST64_T unsigned long long -#define __UINT_FAST64_MAX __FC_ULLONG_MAX - -/* POSIX */ -#define __SSIZE_T int -#define __SSIZE_MAX __FC_INT_MAX -/* stdio.h */ -#ifndef __FC_L_tmpnam -#define __FC_L_tmpnam 1024 -#endif -/* stdint.h */ -#define __FC_PTRDIFF_MIN __FC_INT_MIN -#define __FC_PTRDIFF_MAX __FC_INT_MAX -/* wchar.h */ -#define __WINT_T unsigned int -#define __FC_WEOF (0xFFFFFFFFU) -#define __FC_WINT_MIN 0 -#define __FC_WINT_MAX __FC_UINT_MAX - -#ifdef __FC_MACHDEP_GCC_X86_32 -#include "__fc_gcc_builtins.h" -#endif - -// End of X86_32 || GCC_X86_32 -#else -#if defined(__FC_MACHDEP_X86_64) || defined(__FC_MACHDEP_GCC_X86_64) -#define __FC_FORCE_INCLUDE_MACHDEP__ -#include "__fc_machdep_linux_shared.h" -#undef __FC_FORCE_INCLUDE_MACHDEP__ -#define __FC_BYTE_ORDER __LITTLE_ENDIAN -/* Required */ -#undef __CHAR_UNSIGNED__ -#define __WORDSIZE 64 -#define __SIZEOF_SHORT 2 -#define __SIZEOF_INT 4 -#define __SIZEOF_LONG 8 -#define __SIZEOF_LONGLONG 8 -#define __CHAR_BIT 8 -#define __PTRDIFF_T long -#define __SIZE_T unsigned long -#define __WCHAR_T int -#define __FC_INT_MIN (-2147483647 - 1) -#define __FC_INT_MAX 2147483647 -#define __FC_UINT_MAX 4294967295U -#define __FC_LONG_MIN (-9223372036854775807L -1L) -#define __FC_LONG_MAX 9223372036854775807L -#define __FC_ULONG_MAX 18446744073709551615UL -#define __FC_SIZE_MAX __FC_ULONG_MAX - -/* Optional */ -#define __INTPTR_T signed long -#define __FC_INTPTR_MIN __FC_LONG_MIN -#define __FC_INTPTR_MAX __FC_LONG_MAX - -#define __UINTPTR_T unsigned long -#define __FC_UINTPTR_MAX __FC_ULONG_MAX - -#define __INT32_T signed int -#define __INT32_MIN __FC_INT_MIN -#define __INT32_MAX __FC_INT_MAX - -#define __UINT32_T unsigned int -#define __UINT32_MAX __FC_UINT_MAX - -#define __INT64_T signed long -#define __INT64_MIN __FC_LONG_MIN -#define __INT64_MAX __FC_LONG_MAX - -#define __UINT64_T unsigned long -#define __UINT64_MAX __FC_ULONG_MAX - -/* prefixes for inttypes */ -#define __PRI32_PREFIX "" -#define __PRI64_PREFIX "l" -#define __PRIPTR_PREFIX "l" - -/* Required */ -#define __INT_LEAST32_T signed int -#define __INT_LEAST32_MIN __FC_INT_MIN -#define __INT_LEAST32_MAX __FC_INT_MAX - -#define __UINT_LEAST32_T unsigned int -#define __UINT_LEAST32_MAX __FC_UINT_MAX - -#define __INT_LEAST64_T signed long -#define __INT_LEAST64_MIN __FC_LONG_MIN -#define __INT_LEAST64_MAX __FC_LONG_MAX - -#define __UINT_LEAST64_T unsigned long -#define __UINT_LEAST64_MAX __FC_ULONG_MAX - -#define __INT_FAST32_T signed int -#define __INT_FAST32_MIN __FC_INT_MIN -#define __INT_FAST32_MAX __FC_INT_MAX - -#define __UINT_FAST32_T unsigned int -#define __UINT_FAST32_MAX __FC_UINT_MAX - -#define __INT_FAST64_T signed long -#define __INT_FAST64_MIN __FC_LONG_MIN -#define __INT_FAST64_MAX __FC_LONG_MAX - -#define __UINT_FAST64_T unsigned long -#define __UINT_FAST64_MAX __FC_ULONG_MAX - -/* POSIX */ -#define __SSIZE_T signed long -#define __SSIZE_MAX __FC_LONG_MAX -/* stdio.h */ -#ifndef __FC_L_tmpnam -#define __FC_L_tmpnam 1024 -#endif -/* stdint.h */ -#define __FC_PTRDIFF_MIN __FC_LONG_MIN -#define __FC_PTRDIFF_MAX __FC_LONG_MAX -/* wchar.h */ -#define __WINT_T unsigned int -#define __FC_WEOF (0xFFFFFFFFU) -#define __FC_WINT_MIN 0 -#define __FC_WINT_MAX __FC_UINT_MAX - -#ifdef __FC_MACHDEP_GCC_X86_64 -#include "__fc_gcc_builtins.h" -#endif - -// End of X86_64 || GCC_X86_64 -#else -#if defined(__FC_MACHDEP_X86_16) || defined(__FC_MACHDEP_GCC_X86_16) -#define __FC_FORCE_INCLUDE_MACHDEP__ -#include "__fc_machdep_linux_shared.h" -#undef __FC_FORCE_INCLUDE_MACHDEP__ -#define __FC_BYTE_ORDER __LITTLE_ENDIAN -/* Required */ -#undef __CHAR_UNSIGNED__ -#define __WORDSIZE 16 -#define __SIZEOF_SHORT 2 -#define __SIZEOF_INT 2 -#define __SIZEOF_LONG 4 -#define __SIZEOF_LONGLONG 8 -#define __CHAR_BIT 8 -#define __PTRDIFF_T long -#define __SIZE_T unsigned int -#define __WCHAR_T int -#define __FC_INT_MIN (-32768) -#define __FC_INT_MAX 32767 -#define __FC_UINT_MAX 65535U -#define __FC_LONG_MIN (-2147483647L -1L) -#define __FC_LONG_MAX 2147483647L -#define __FC_ULONG_MAX 4294967295UL -#define __FC_SIZE_MAX 65535U - - -/* Optional */ -#define __INTPTR_T signed long -#define __FC_INTPTR_MIN __FC_LONG_MIN -#define __FC_INTPTR_MAX __FC_LONG_MAX - -#define __UINTPTR_T unsigned long -#define __FC_UINTPTR_MAX __FC_ULONG_MAX - -#define __INT32_T signed long -#define __INT32_MIN __FC_LONG_MIN -#define __INT32_MAX __FC_LONG_MAX - -#define __INT64_T signed long long -#define __INT64_MIN __FC_LLONG_MIN -#define __INT64_MAX __FC_LLONG_MAX - -#define __UINT32_T unsigned long -#define __UINT32_MAX __FC_ULONG_MAX - -#define __UINT64_T unsigned long long -#define __UINT64_MAX __FC_ULLONG_MAX - -/* inttypes */ - -#define __PRI32_PREFIX "l" -#define __PRI64_PREFIX "ll" -#define __PRIPTR_PREFIX "l" - -/* Required */ -#define __INT_LEAST32_T signed long -#define __INT_LEAST32_MIN __FC_LONG_MIN -#define __INT_LEAST32_MAX __FC_LONG_MAX - -#define __UINT_LEAST32_T unsigned long -#define __UINT_LEAST32_MAX __FC_ULONG_MAX - -#define __INT_LEAST64_T signed long long -#define __INT_LEAST64_MIN __FC_LLONG_MIN -#define __INT_LEAST64_MAX __FC_LLONG_MAX - -#define __UINT_LEAST64_T unsigned long long -#define __UINT_LEAST64_MAX __FC_ULLONG_MAX - -#define __INT_FAST32_T signed long -#define __INT_FAST32_MIN __FC_LONG_MIN -#define __INT_FAST32_MAX __FC_LONG_MAX - -#define __UINT_FAST32_T unsigned long -#define __UINT_FAST32_MAX __FC_ULONG_MAX - -#define __INT_FAST64_T signed long long -#define __INT_FAST64_MIN __FC_LLONG_MIN -#define __INT_FAST64_MAX __FC_LLONG_MAX - -#define __UINT_FAST64_T unsigned long long -#define __UINT_FAST64_MAX __FC_ULLONG_MAX - -/* POSIX */ -#define __SSIZE_T signed long -#define __SSIZE_MAX __FC_LONG_MAX -/* stdio.h */ -#ifndef __FC_L_tmpnam -#define __FC_L_tmpnam 1024 -#endif -/* stdint.h */ -#define __FC_PTRDIFF_MIN __FC_LONG_MIN -#define __FC_PTRDIFF_MAX __FC_LONG_MAX - -/* wchar.h */ -#define __WINT_T unsigned long -#define __FC_WEOF (0xFFFFFFFFUL) -#define __FC_WINT_MIN 0 -#define __FC_WINT_MAX __FC_ULONG_MAX - -#ifdef __FC_MACHDEP_GCC_X86_16 -#include "__fc_gcc_builtins.h" -#endif - -// End of X86_16 || GCC_X86_16 -#else -#ifdef __FC_MACHDEP_PPC_32 -#define __FC_FORCE_INCLUDE_MACHDEP__ -#include "__fc_machdep_linux_shared.h" -#undef __FC_FORCE_INCLUDE_MACHDEP__ -#define __FC_BYTE_ORDER __BIG_ENDIAN -/* Required */ -#undef __CHAR_UNSIGNED__ -#define __WORDSIZE 32 -#define __SIZEOF_SHORT 2 -#define __SIZEOF_INT 4 -#define __SIZEOF_LONG 4 -#define __SIZEOF_LONGLONG 8 -#define __CHAR_BIT 8 -#define __PTRDIFF_T int -#define __SIZE_T unsigned int -#define __WCHAR_T int -#define __FC_INT_MIN (-2147483647 - 1) -#define __FC_INT_MAX 2147483647 -#define __FC_UINT_MAX 4294967295U -#define __FC_LONG_MIN (-2147483647L -1L) -#define __FC_LONG_MAX 2147483647L -#define __FC_ULONG_MAX 4294967295UL -#define __FC_SIZE_MAX __FC_UINT_MAX - -/* Optional */ -#define __INTPTR_T signed int -#define __FC_INTPTR_MIN __FC_LONG_MIN -#define __FC_INTPTR_MAX __FC_LONG_MAX - -#define __UINTPTR_T unsigned int -#define __FC_UINTPTR_MAX __FC_ULONG_MAX - -#define __INT32_T signed int -#define __INT32_MIN __FC_INT_MIN -#define __INT32_MAX __FC_INT_MAX - -#define __UINT32_T unsigned int -#define __UINT32_MAX __FC_UINT_MAX - -#define __INT64_T signed long long -#define __INT64_MIN __FC_LLONG_MIN -#define __INT64_MAX __FC_LLONG_MAX - -#define __UINT64_T unsigned long long -#define __UINT64_MAX __FC_ULLONG_MAX - -/* inttypes */ - -#define __PRI32_PREFIX "" -#define __PRI64_PREFIX "ll" -#define __PRIPTR_PREFIX "" - -/* Required */ -#define __INT_LEAST32_T signed int -#define __INT_LEAST32_MIN __FC_INT_MIN -#define __INT_LEAST32_MAX __FC_INT_MAX - -#define __UINT_LEAST32_T unsigned int -#define __UINT_LEAST32_MAX __FC_UINT_MAX - -#define __INT_LEAST64_T signed long long -#define __INT_LEAST64_MIN __FC_LLONG_MIN -#define __INT_LEAST64_MAX __FC_LLONG_MAX - -#define __UINT_LEAST64_T unsigned long long -#define __UINT_LEAST64_MAX __FC_ULLONG_MAX - -#define __INT_FAST32_T signed int -#define __INT_FAST32_MIN __FC_INT_MIN -#define __INT_FAST32_MAX __FC_INT_MAX - -#define __UINT_FAST32_T unsigned int -#define __UINT_FAST32_MAX __FC_UINT_MAX - -#define __INT_FAST64_T signed long long -#define __INT_FAST64_MIN __FC_LLONG_MIN -#define __INT_FAST64_MAX __FC_LLONG_MAX - -#define __UINT_FAST64_T unsigned long long -#define __UINT_FAST64_MAX __FC_ULLONG_MAX - -/* POSIX */ -#define __SSIZE_T int -#define __SSIZE_MAX __FC_INT_MAX -/* stdio.h */ -#ifndef __FC_L_tmpnam -#define __FC_L_tmpnam 1024 -#endif -/* stdint.h */ -#define __FC_PTRDIFF_MIN __FC_INT_MIN -#define __FC_PTRDIFF_MAX __FC_INT_MAX -#define __FC_INTMAX_MIN (-9223372036854775807LL -1LL) -#define __FC_INTMAX_MAX 9223372036854775807LL -#define __FC_UINTMAX_MAX 18446744073709551615ULL -/* time.h */ -#define __FC_TIME_T long -/* wchar.h */ -#define __WINT_T unsigned int -#define __FC_WEOF (0xFFFFFFFFU) -#define __FC_WINT_MIN 0 -#define __FC_WINT_MAX __FC_UINT_MAX - -// End of PPC_32 -#else -#ifdef __FC_MACHDEP_MSVC_X86_64 -#define __FC_BYTE_ORDER __LITTLE_ENDIAN - -// This machdep does NOT conform itself to POSIX.1-2008 - -/* Required */ -#undef __CHAR_UNSIGNED__ -#define __WORDSIZE 64 -#define __SIZEOF_SHORT 2 -#define __SIZEOF_INT 4 -#define __SIZEOF_LONG 4 -#define __SIZEOF_LONGLONG 8 -#define __CHAR_BIT 8 -#define __PTRDIFF_T long long -#define __SIZE_T unsigned long long - -#define __FC_EOF (-1) -#define __FC_FOPEN_MAX 20 -#define __FC_RAND_MAX 32767 -#define __WCHAR_T unsigned short - -/* min and max values as specified in limits.h */ -#define __FC_SCHAR_MIN (-128) -#define __FC_SCHAR_MAX 127 -#define __FC_UCHAR_MAX 255 -#define __FC_SHRT_MIN (-32768) -#define __FC_SHRT_MAX 32767 -#define __FC_USHRT_MAX 65535 -#define __FC_INT_MIN (-2147483647 - 1) -#define __FC_INT_MAX 2147483647 -#define __FC_UINT_MAX 4294967295U -#define __FC_LONG_MIN (-2147483647L -1L) -#define __FC_LONG_MAX 2147483647L -#define __FC_ULONG_MAX 4294967295UL -#define __FC_LLONG_MIN (-9223372036854775807LL -1LL) -#define __FC_LLONG_MAX 9223372036854775807LL -#define __FC_ULLONG_MAX 18446744073709551615ULL -#define __FC_PATH_MAX 256 -#define __FC_SIZE_MAX __FC_ULLONG_MAX -// Note: SSIZE_T/SSIZE_MAX are not defined in this machdep! -/* Note: MSVC does not define this constant, but because it is used in an ACSL - specification, it is safer to define it anyway. */ -#define __FC_HOST_NAME_MAX 255 -#define __FC_TTY_NAME_MAX 32 - -/* Optional */ -#define __INT8_T signed char -#define __INT8_MIN __FC_SCHAR_MIN -#define __INT8_MAX __FC_SCHAR_MAX - -#define __UINT8_T unsigned char -#define __UINT8_MIN __FC_UCHAR_MAX - -#define __INT16_T signed short -#define __INT16_MIN __FC_SHRT_MIN -#define __INT16_MAX __FC_SHRT_MAX - -#define __UINT16_T unsigned short -#define __UINT16_MAX __FC_USHRT_MAX - -#define __INTPTR_T signed long long -#define __FC_INTPTR_MIN __FC_LLONG_MIN -#define __FC_INTPTR_MAX __FC_LLONG_MAX - -#define __UINTPTR_T unsigned long long -#define __FC_UINTPTR_MAX __FC_ULLONG_MAX - -#define __INT32_T signed int -#define __INT32_MIN __FC_INT_MIN -#define __INT32_MAX __FC_INT_MAX - -#define __UINT32_T unsigned int -#define __UINT32_MAX __FC_UINT_MAX - -#define __INT64_T signed long long -#define __INT64_MIN __FC_LLONG_MIN -#define __INT64_MAX __FC_LLONG_MAX - -#define __UINT64_T unsigned long long -#define __UINT64_MAX __FC_ULLONG_MAX - -/* inttypes */ - -#define __PRI8_PREFIX "hh" -#define __PRI16_PREFIX "h" -#define __PRIFAST16_PREFIX "" -#define __PRI32_PREFIX "" -#define __PRI64_PREFIX "ll" -#define __PRIPTR_PREFIX "ll" -#define __PRIMAX_PREFIX "ll" - -/* Required */ -#define __INT_LEAST8_T signed char -#define __INT_LEAST8_MIN __FC_SCHAR_MIN -#define __INT_LEAST8_MAX __FC_SCHAR_MAX - -#define __UINT_LEAST8_T unsigned char -#define __UINT_LEAST8_MAX __FC_UCHAR_MAX - -#define __INT_LEAST16_T signed short -#define __INT_LEAST16_MIN __FC_SHRT_MIN -#define __INT_LEAST16_MAX __FC_SHRT_MAX - -#define __UINT_LEAST16_T unsigned short -#define __UINT_LEAST16_MAX __FC_USHRT_MAX - -#define __INT_LEAST32_T signed int -#define __INT_LEAST32_MIN __FC_INT_MIN -#define __INT_LEAST32_MAX __FC_INT_MAX - -#define __UINT_LEAST32_T unsigned int -#define __UINT_LEAST32_MAX __FC_UINT_MAX - -#define __INT_LEAST64_T signed long long -#define __INT_LEAST64_MIN __FC_LLONG_MIN -#define __INT_LEAST64_MAX __FC_LLONG_MAX - -#define __UINT_LEAST64_T unsigned long long -#define __UINT_LEAST64_MAX __FC_ULLONG_MAX - -#define __INT_FAST8_T signed char -#define __INT_FAST8_MIN __FC_SCHAR_MIN -#define __INT_FAST8_MAX __FC_SCHAR_MAX - -#define __UINT_FAST8_T unsigned char -#define __UINT_FAST8_MAX __FC_UCHAR_MAX - -#define __INT_FAST16_T signed int -#define __INT_FAST16_MIN __FC_INT_MIN -#define __INT_FAST16_MAX __FC_INT_MAX - -#define __UINT_FAST16_T unsigned int -#define __UINT_FAST16_MAX __FC_UINT_MAX - -#define __INT_FAST32_T signed int -#define __INT_FAST32_MIN __FC_INT_MIN -#define __INT_FAST32_MAX __FC_INT_MAX - -#define __UINT_FAST32_T unsigned int -#define __UINT_FAST32_MAX __FC_UINT_MAX - -#define __INT_FAST64_T signed long long -#define __INT_FAST64_MIN __FC_LLONG_MIN -#define __INT_FAST64_MAX __FC_LLONG_MAX - -#define __UINT_FAST64_T unsigned long long -#define __UINT_FAST64_MAX __FC_ULLONG_MAX - -/* Required */ -#define __INT_MAX_T signed long long -#define __UINT_MAX_T unsigned long long - -/* POSIX */ -#define __SSIZE_T signed long long -/* stdio.h */ -#ifndef __FC_L_tmpnam -#define __FC_L_tmpnam 20 -#endif -/* stdint.h */ -#define __FC_WCHAR_MIN 0 -#define __FC_WCHAR_MAX __FC_USHRT_MAX -#define __FC_PTRDIFF_MIN __FC_LLONG_MIN -#define __FC_PTRDIFF_MAX __FC_LLONG_MAX -#define __FC_INTMAX_MIN (-9223372036854775807LL -1LL) -#define __FC_INTMAX_MAX 9223372036854775807LL -#define __FC_UINTMAX_MAX 18446744073709551615ULL -/* time.h */ -#define __FC_TIME_T __int64 - -/* for stdarg.h */ -#define __FC_VA_LIST_T char* - -/* wchar.h */ -// note: wint_t should contain all values of wchar_t plus WEOF; but this version -// of MSVC does not necessarily respect the standard -#define __WINT_T unsigned short -#define __FC_WEOF (0xFFFFU) -#define __FC_WINT_MIN 0 -#define __FC_WINT_MAX __FC_USHRT_MAX - -/* The following macros are defined to correspond to the version of MSVC used - during the definition of some MSVC-specific features: Visual Studio 2010. - They also help detecting, in some tests, whether we are in MSVC mode. */ -#define _MSC_FULL_VER 160040219 -#define _MSC_VER 1600 - -// MSVC-specific definitions; necessary when parsing MSVC libraries using -// non-MSVC preprocessors and compilers -#undef __ptr64 -#define __ptr64 -#undef __ptr32 -#define __ptr32 -#undef __unaligned -#define __unaligned -#undef __cdecl -#define __cdecl -#undef __possibly_notnullterminated -#define __possibly_notnullterminated -#ifndef errno_t -# define errno_t int -# define _ERRNO_T_DEFINED -#endif -#ifndef _WIN64 -# define _WIN64 1 -#endif -#ifndef _AMD64_ -# define _AMD64_ 1 -#endif -#ifndef _M_AMD64 -# define _M_AMD64 1 -#endif -#ifndef _M_X64 -# define _M_X64 1 -#endif - -/* errno.h */ -#define __FC_EPERM 1 -#define __FC_ENOENT 2 -#define __FC_ESRCH 3 -#define __FC_EINTR 4 -#define __FC_EIO 5 -#define __FC_ENXIO 6 -#define __FC_E2BIG 7 -#define __FC_ENOEXEC 8 -#define __FC_EBADF 9 -#define __FC_ECHILD 10 -#define __FC_EAGAIN 11 -#define __FC_ENOMEM 12 -#define __FC_EACCES 13 -#define __FC_EFAULT 14 -//NOT IN MSVC: #define __FC_ENOTBLK -#define __FC_EBUSY 16 -#define __FC_EEXIST 17 -#define __FC_EXDEV 18 -#define __FC_ENODEV 19 -#define __FC_ENOTDIR 20 -#define __FC_EISDIR 21 -#define __FC_EINVAL 22 -#define __FC_ENFILE 23 -#define __FC_EMFILE 24 -#define __FC_ENOTTY 25 -#define __FC_ETXTBSY 139 -#define __FC_EFBIG 27 -#define __FC_ENOSPC 28 -#define __FC_ESPIPE 29 -#define __FC_EROFS 30 -#define __FC_EMLINK 31 -#define __FC_EPIPE 32 -#define __FC_EDOM 33 -#define __FC_ERANGE 34 -#define __FC_EDEADLK 36 -#define __FC_ENAMETOOLONG 38 -#define __FC_ENOLCK 39 -#define __FC_ENOSYS 40 -#define __FC_ENOTEMPTY 41 -#define __FC_ELOOP 114 -#define __FC_EWOULDBLOCK 140 -#define __FC_ENOMSG 122 -#define __FC_EIDRM 111 -//NOT IN MSVC: #define __FC_ECHRNG -//NOT IN MSVC: #define __FC_EL2NSYNC -//NOT IN MSVC: #define __FC_EL3HLT -//NOT IN MSVC: #define __FC_EL3RST -//NOT IN MSVC: #define __FC_ELNRNG -//NOT IN MSVC: #define __FC_EUNATCH -//NOT IN MSVC: #define __FC_ENOCSI -//NOT IN MSVC: #define __FC_EL2HLT -//NOT IN MSVC: #define __FC_EBADE -//NOT IN MSVC: #define __FC_EBADR -//NOT IN MSVC: #define __FC_EXFULL -//NOT IN MSVC: #define __FC_ENOANO -//NOT IN MSVC: #define __FC_EBADRQC -//NOT IN MSVC: #define __FC_EBADSLT -#define __FC_EDEADLOCK 36 -//NOT IN MSVC: #define __FC_EBFONT -#define __FC_ENOSTR 125 -#define __FC_ENODATA 120 -#define __FC_ETIME 137 -#define __FC_ENOSR 124 -//NOT IN MSVC: #define __FC_ENONET -//NOT IN MSVC: #define __FC_ENOPKG -//NOT IN MSVC: #define __FC_EREMOTE -#define __FC_ENOLINK 121 -//NOT IN MSVC: #define __FC_EADV -//NOT IN MSVC: #define __FC_ESRMNT -//NOT IN MSVC: #define __FC_ECOMM -#define __FC_EPROTO 134 -//NOT IN MSVC: #define __FC_EMULTIHOP -//NOT IN MSVC: #define __FC_EDOTDOT -#define __FC_EBADMSG 104 -#define __FC_EOVERFLOW 132 -//NOT IN MSVC: #define __FC_ENOTUNIQ -//NOT IN MSVC: #define __FC_EBADFD -//NOT IN MSVC: #define __FC_EREMCHG -//NOT IN MSVC: #define __FC_ELIBACC -//NOT IN MSVC: #define __FC_ELIBBAD -//NOT IN MSVC: #define __FC_ELIBSCN -//NOT IN MSVC: #define __FC_ELIBMAX -//NOT IN MSVC: #define __FC_ELIBEXEC -#define __FC_EILSEQ 42 -//NOT IN MSVC: #define __FC_ERESTART -//NOT IN MSVC: #define __FC_ESTRPIPE -//NOT IN MSVC: #define __FC_EUSERS -#define __FC_ENOTSOCK 128 -#define __FC_EDESTADDRREQ 109 -#define __FC_EMSGSIZE 115 -#define __FC_EPROTOTYPE 136 -#define __FC_ENOPROTOOPT 123 -#define __FC_EPROTONOSUPPORT 135 -//NOT IN MSVC: #define __FC_ESOCKTNOSUPPORT -#define __FC_ENOTSUP 129 -#define __FC_EOPNOTSUPP 130 -//NOT IN MSVC: #define __FC_EPFNOSUPPORT -#define __FC_EAFNOSUPPORT 102 -#define __FC_EADDRINUSE 100 -#define __FC_EADDRNOTAVAIL 101 -#define __FC_ENETDOWN 116 -#define __FC_ENETUNREACH 118 -#define __FC_ENETRESET 117 -#define __FC_ECONNABORTED 106 -#define __FC_ECONNRESET 108 -#define __FC_ENOBUFS 119 -#define __FC_EISCONN 113 -#define __FC_ENOTCONN 126 -//NOT IN MSVC: #define __FC_ESHUTDOWN -//NOT IN MSVC: #define __FC_ETOOMANYREFS -#define __FC_ETIMEDOUT 138 -#define __FC_ECONNREFUSED 107 -//NOT IN MSVC: #define __FC_EHOSTDOWN -#define __FC_EHOSTUNREACH 110 -#define __FC_EALREADY 103 -#define __FC_EINPROGRESS 112 -//NOT IN MSVC: #define __FC_ESTALE -//NOT IN MSVC: #define __FC_EUCLEAN -//NOT IN MSVC: #define __FC_ENOTNAM -//NOT IN MSVC: #define __FC_ENAVAIL -//NOT IN MSVC: #define __FC_EISNAM -//NOT IN MSVC: #define __FC_EREMOTEIO -//NOT IN MSVC: #define __FC_EDQUOT -//NOT IN MSVC: #define __FC_ENOMEDIUM -//NOT IN MSVC: #define __FC_EMEDIUMTYPE -#define __FC_ECANCELED 105 -//NOT IN MSVC: #define __FC_ENOKEY -//NOT IN MSVC: #define __FC_EKEYEXPIRED -//NOT IN MSVC: #define __FC_EKEYREVOKED -//NOT IN MSVC: #define __FC_EKEYREJECTED -#define __FC_EOWNERDEAD 133 -#define __FC_ENOTRECOVERABLE 127 -//NOT IN MSVC: #define __FC_ERFKILL -//NOT IN MSVC: #define __FC_EHWPOISON - -/* signal.h */ -#define __FC_NSIG 23 - -// End of MSVC_X86_64 -#else -#error Must define __FC_MACHDEP_<M>, where <M> is one of the \ - following: X86_32, X86_64, X86_16, GCC_X86_32, GCC_X86_64, \ - GCC_X86_16, PPC_32, MSVC_X86_64. \ - If you are using a custom machdep, you must include your machdep \ - header file defining __FC_MACHDEP to avoid inclusion of this file. -#endif -#endif -#endif -#endif -#endif -#endif diff --git a/src/plugins/e-acsl/dune b/src/plugins/e-acsl/dune index 2a14f54f6fe256e473ef32b4beba8e7de85c4256..dc47a13216442a9a5e34169772c86ba5f28c005e 100644 --- a/src/plugins/e-acsl/dune +++ b/src/plugins/e-acsl/dune @@ -56,84 +56,7 @@ (files (scripts/e-acsl-gcc.sh as e-acsl-gcc.sh))) -; SHARE (install (package frama-c-e-acsl) (section (site (frama-c share))) - (files -; main header -(share/e-acsl/e_acsl.h as e-acsl/e_acsl.h) -; (numerical_model) -(share/e-acsl/numerical_model/e_acsl_floating_point.h as e-acsl/numerical_model/e_acsl_floating_point.h) -(share/e-acsl/numerical_model/e_acsl_floating_point.c as e-acsl/numerical_model/e_acsl_floating_point.c) -(share/e-acsl/numerical_model/e_acsl_gmp_api.h as e-acsl/numerical_model/e_acsl_gmp_api.h) -; (libc_replacements) -(share/e-acsl/libc_replacements/e_acsl_string.h as e-acsl/libc_replacements/e_acsl_string.h) -(share/e-acsl/libc_replacements/e_acsl_stdio.c as e-acsl/libc_replacements/e_acsl_stdio.c) -(share/e-acsl/libc_replacements/e_acsl_string.c as e-acsl/libc_replacements/e_acsl_string.c) -(share/e-acsl/libc_replacements/e_acsl_stdio.h as e-acsl/libc_replacements/e_acsl_stdio.h) -; (instrumentation_model) -(share/e-acsl/instrumentation_model/e_acsl_temporal.c as e-acsl/instrumentation_model/e_acsl_temporal.c) -(share/e-acsl/instrumentation_model/e_acsl_assert_data.h as e-acsl/instrumentation_model/e_acsl_assert_data.h) -(share/e-acsl/instrumentation_model/e_acsl_contract.h as e-acsl/instrumentation_model/e_acsl_contract.h) -(share/e-acsl/instrumentation_model/e_acsl_temporal.h as e-acsl/instrumentation_model/e_acsl_temporal.h) -(share/e-acsl/instrumentation_model/e_acsl_contract.c as e-acsl/instrumentation_model/e_acsl_contract.c) -(share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c as e-acsl/instrumentation_model/e_acsl_assert_data_api.c) -(share/e-acsl/instrumentation_model/e_acsl_assert.c as e-acsl/instrumentation_model/e_acsl_assert.c) -(share/e-acsl/instrumentation_model/e_acsl_assert.h as e-acsl/instrumentation_model/e_acsl_assert.h) -(share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h as e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h) -(share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h as e-acsl/instrumentation_model/e_acsl_assert_data_api.h) -; (observation_model) -(share/e-acsl/observation_model/e_acsl_observation_model.h as e-acsl/observation_model/e_acsl_observation_model.h) -(share/e-acsl/observation_model/e_acsl_heap.h as e-acsl/observation_model/e_acsl_heap.h) -; (observation_model/segment_model) -(share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c as e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c) -(share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h as e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h) -(share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c as e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c) -(share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h as e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h) -(share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c as e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c) -(share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h as e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h) -(share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c as e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c) -(share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c as e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c) -(share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c as e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c) -(share/e-acsl/observation_model/e_acsl_observation_model.c as e-acsl/observation_model/e_acsl_observation_model.c) -; (observation_model/bittree_model) -(share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c as e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c) -(share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c as e-acsl/observation_model/bittree_model/e_acsl_bittree.c) -(share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h as e-acsl/observation_model/bittree_model/e_acsl_bittree.h) -(share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c as e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c) -(share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c as e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c) -; (observation_model/internals) -(share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c as e-acsl/observation_model/internals/e_acsl_patricia_trie.c) -(share/e-acsl/observation_model/internals/e_acsl_safe_locations.h as e-acsl/observation_model/internals/e_acsl_safe_locations.h) -(share/e-acsl/observation_model/internals/e_acsl_safe_locations.c as e-acsl/observation_model/internals/e_acsl_safe_locations.c) -(share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h as e-acsl/observation_model/internals/e_acsl_patricia_trie.h) -(share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h as e-acsl/observation_model/internals/e_acsl_heap_tracking.h) -(share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h as e-acsl/observation_model/internals/e_acsl_omodel_debug.h) -(share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h as e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h) -(share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c as e-acsl/observation_model/internals/e_acsl_heap_tracking.c) -(share/e-acsl/observation_model/e_acsl_heap.c as e-acsl/observation_model/e_acsl_heap.c) -(share/e-acsl/e_acsl_rtl.c as e-acsl/e_acsl_rtl.c) -; (internals) -(share/e-acsl/internals/e_acsl_concurrency.h as e-acsl/internals/e_acsl_concurrency.h) -(share/e-acsl/internals/e_acsl_debug.c as e-acsl/internals/e_acsl_debug.c) -(share/e-acsl/internals/e_acsl_rtl_error.c as e-acsl/internals/e_acsl_rtl_error.c) -(share/e-acsl/internals/e_acsl_malloc.c as e-acsl/internals/e_acsl_malloc.c) -(share/e-acsl/internals/e_acsl_bits.c as e-acsl/internals/e_acsl_bits.c) -(share/e-acsl/internals/e_acsl_shexec.c as e-acsl/internals/e_acsl_shexec.c) -(share/e-acsl/internals/e_acsl_trace.c as e-acsl/internals/e_acsl_trace.c) -(share/e-acsl/internals/e_acsl_trace.h as e-acsl/internals/e_acsl_trace.h) -(share/e-acsl/internals/e_acsl_debug.h as e-acsl/internals/e_acsl_debug.h) -(share/e-acsl/internals/e_acsl_shexec.h as e-acsl/internals/e_acsl_shexec.h) -(share/e-acsl/internals/e_acsl_rtl_string.c as e-acsl/internals/e_acsl_rtl_string.c) -(share/e-acsl/internals/e_acsl_rtl_io.h as e-acsl/internals/e_acsl_rtl_io.h) -(share/e-acsl/internals/e_acsl_rtl_error.h as e-acsl/internals/e_acsl_rtl_error.h) -(share/e-acsl/internals/e_acsl_alias.h as e-acsl/internals/e_acsl_alias.h) -(share/e-acsl/internals/e_acsl_rtl_string.h as e-acsl/internals/e_acsl_rtl_string.h) -(share/e-acsl/internals/e_acsl_malloc.h as e-acsl/internals/e_acsl_malloc.h) -(share/e-acsl/internals/e_acsl_private_assert.c as e-acsl/internals/e_acsl_private_assert.c) -(share/e-acsl/internals/e_acsl_private_assert.h as e-acsl/internals/e_acsl_private_assert.h) -(share/e-acsl/internals/e_acsl_bits.h as e-acsl/internals/e_acsl_bits.h) -(share/e-acsl/internals/e_acsl_rtl_io.c as e-acsl/internals/e_acsl_rtl_io.c) -(share/e-acsl/internals/e_acsl_config.h as e-acsl/internals/e_acsl_config.h) -)) + (source_trees (share/e-acsl as e-acsl))) diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune index a83f14990653d6de97debb2017cf8caa8f9863bd..b46cbeb373eb6214a4aa1d096431328d18678263 100644 --- a/src/plugins/wp/dune +++ b/src/plugins/wp/dune @@ -55,17 +55,5 @@ (install (package frama-c-wp) (section (site (frama-c share))) - (files - (share/Makefile.resources as wp/Makefile.resources) - (share/why3/frama_c_wp/vlist.mlw as wp/why3/frama_c_wp/vlist.mlw) - (share/why3/frama_c_wp/cbits.mlw as wp/why3/frama_c_wp/cbits.mlw) - (share/why3/frama_c_wp/cint.mlw as wp/why3/frama_c_wp/cint.mlw) - (share/why3/frama_c_wp/qed.mlw as wp/why3/frama_c_wp/qed.mlw) - (share/why3/frama_c_wp/vset.mlw as wp/why3/frama_c_wp/vset.mlw) - (share/why3/frama_c_wp/memaddr.mlw as wp/why3/frama_c_wp/memaddr.mlw) - (share/why3/frama_c_wp/memory.mlw as wp/why3/frama_c_wp/memory.mlw) - (share/why3/frama_c_wp/membytes.mlw as wp/why3/frama_c_wp/membytes.mlw) - (share/why3/frama_c_wp/cmath.mlw as wp/why3/frama_c_wp/cmath.mlw) - (share/why3/frama_c_wp/cfloat.mlw as wp/why3/frama_c_wp/cfloat.mlw) - (share/why3/frama_c_wp/sequence.mlw as wp/why3/frama_c_wp/sequence.mlw) - (share/wp.driver as wp/wp.driver))) + (files (share/wp.driver as wp/wp.driver)) + (source_trees (share/why3 as wp/why3))) diff --git a/src/plugins/wp/share/Makefile.resources b/src/plugins/wp/share/Makefile.resources deleted file mode 100644 index 57e5a3c260f48bf4419cc704870756d339a765d8..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/Makefile.resources +++ /dev/null @@ -1,60 +0,0 @@ -########################################################################## -# # -# This file is part of WP plug-in of Frama-C. # -# # -# Copyright (C) 2007-2024 # -# CEA (Commissariat a l'energie atomique et aux energies # -# alternatives) # -# # -# you can redistribute it and/or modify it under the terms of the GNU # -# Lesser General Public License as published by the Free Software # -# Foundation, version 2.1. # -# # -# It is distributed in the hope that it will be useful, # -# but WITHOUT ANY WARRANTY; without even the implied warranty of # -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # -# GNU Lesser General Public License for more details. # -# # -# See the GNU Lesser General Public License version 2.1 # -# for more details (enclosed in the file licenses/LGPLv2.1). # -# # -########################################################################## - -# -------------------------------------------------------------------------- -# --- Why-3 Libraries -# -------------------------------------------------------------------------- - -## Used in share/why3 - -WHY3_LIBS_CEA:= \ - cbits.mlw \ - cint.mlw \ - cfloat.mlw \ - cmath.mlw \ - memory.mlw \ - qed.mlw \ - vset.mlw \ - vlist.mlw - -## Used in share/why3 -WHY3_API_LIBS_CEA:= WHY3_LIBS_CEA - -# -------------------------------------------------------------------------- -# --- LICENSES -# -------------------------------------------------------------------------- - -# Resource classes for license header files -# These files are relatives to this directory -WP_SHARE_SRC_CEA_RESOURCES:= \ - wp.driver \ - why3/coq.drv \ - $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA)) - -ALL_CEA_RESOURCES+= \ - Makefile.resources \ - $(WP_SHARE_SRC_CEA_RESOURCES) - -########################################################################## -# Local Variables: -# mode: makefile -# End: diff --git a/tests/libc/check_parsing_individual_headers.ml b/tests/libc/check_parsing_individual_headers.ml index 21969ad8745198a0bd7e76a325806cafab756894..1ff8543f6d081888f499ac6dff1146ecbb6116ec 100644 --- a/tests/libc/check_parsing_individual_headers.ml +++ b/tests/libc/check_parsing_individual_headers.ml @@ -8,9 +8,7 @@ let is_header f = Str.string_match header_re f 0 (* Files which are *not* supposed to be parsed *) let blacklist libc_dir = - List.map (fun f -> - Datatype.Filepath.concat libc_dir f) - ["tgmath.h"; "complex.h"; "__fc_machdep_linux_shared.h"] + List.map (Datatype.Filepath.concat libc_dir) ["tgmath.h"; "complex.h"] (* only goes down one level, which is enough for the libc *) let collect_headers () = diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c index 30692f59a93a94b308478a97d4b13136bc4308fd..8d9887b9f2af32909c6058fcdb0e9cba188c9640 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -93,7 +93,6 @@ #include "__fc_integer.h" //#include "__fc_libc.h" //keep this; used by check_full_libc.sh #include "__fc_machdep.h" -//#include "__fc_machdep_linux_shared.h" //keep this; used by check_full_libc.sh #include "fcntl.h" #include "__fc_select.h" #include "__fc_string_axiomatic.h" diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle index bec42d8aa6bcecb2bd7c64989c5ebf0903092274..8a1386fbba1a8ac05da0d116266046bc33924eee 100644 --- a/tests/libc/oracle/fc_libc.0.res.oracle +++ b/tests/libc/oracle/fc_libc.0.res.oracle @@ -5,10 +5,10 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization +[eva] fc_libc.c:209: assertion got status valid. [eva] fc_libc.c:210: assertion got status valid. [eva] fc_libc.c:211: assertion got status valid. [eva] fc_libc.c:212: assertion got status valid. -[eva] fc_libc.c:213: assertion got status valid. [eva] Recording results for main [eva] Done for function main [eva] ====== VALUES COMPUTED ======