Skip to content
Snippets Groups Projects
Commit abb088ab authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/blanchard/install/dirs' into 'master' 

Use Dune 3.11 install source tree

See merge request frama-c/frama-c!4299
parents b5420b14 679db718
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 36 additions and 1586 deletions
share/dune
+ 31
− 358
View file @ abb088ab
...@@ -23,297 +23,32 @@ ...@@ -23,297 +23,32 @@
(install (install
(package frama-c) (package frama-c)
(section (site (frama-c share))) (section (site (frama-c share)))
(source_trees compliance emacs theme libc)
(files (files
; Auto-Complete ; Auto-Complete
(autocomplete_frama-c as autocomplete_frama-c) (autocomplete_frama-c as autocomplete_frama-c)
(_frama-c as _frama-c) (_frama-c as _frama-c)
; Emacs ; Useful Makefiles
(emacs/frama-c-init.el as emacs/frama-c-init.el) (Makefile.common as Makefile.common)
(emacs/frama-c-dev.el as emacs/frama-c-dev.el) (Makefile.headers as Makefile.headers)
(emacs/frama-c-recommended.el as emacs/frama-c-recommended.el) (Makefile.linting as Makefile.linting)
(emacs/acsl.el as emacs/acsl.el) (Makefile.installation as Makefile.installation)
; Useful Makefiles (Makefile.testing as Makefile.testing)
(Makefile.common as Makefile.common) ; GUI Images
(Makefile.headers as Makefile.headers) (frama-c.ico as frama-c.ico)
(Makefile.linting as Makefile.linting) (frama-c.png as frama-c.png)
(Makefile.installation as Makefile.installation) (unmark.png as unmark.png)
(Makefile.testing as Makefile.testing) (switch-on.png as switch-on.png)
; GUI Images (switch-off.png as switch-off.png)))
(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)
))
; Analysis scripts (executable files) ; Analysis scripts (executable files)
(install (install
(package frama-c) (package frama-c)
(section libexec) (section libexec)
(files (files
(analysis-scripts/benchmark_database.py as lib/analysis-scripts/benchmark_database.py) (glob_files (analysis-scripts/*.py with_prefix lib/analysis-scripts))
(analysis-scripts/bench-sqlite.sh as lib/analysis-scripts/bench-sqlite.sh) (glob_files (analysis-scripts/*.sh with_prefix lib/analysis-scripts))
(analysis-scripts/build_callgraph.py as lib/analysis-scripts/build_callgraph.py) (analysis-scripts/flamegraph.pl as lib/analysis-scripts/flamegraph.pl)
(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)
)) ))
; Analysis scripts (non-executable files) ; Analysis scripts (non-executable files)
...@@ -321,16 +56,15 @@ ...@@ -321,16 +56,15 @@
(package frama-c) (package frama-c)
(section lib) (section lib)
(files (files
(analysis-scripts/analysis.mk as lib/analysis-scripts/analysis.mk) (analysis-scripts/analysis.mk as lib/analysis-scripts/analysis.mk)
(analysis-scripts/epilogue.mk as lib/analysis-scripts/epilogue.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/fc_stubs.c as lib/analysis-scripts/fc_stubs.c)
(analysis-scripts/list_functions.ml as lib/analysis-scripts/list_functions.ml) (analysis-scripts/list_functions.ml as lib/analysis-scripts/list_functions.ml)
(analysis-scripts/prologue.mk as lib/analysis-scripts/prologue.mk) (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.graphml as lib/analysis-scripts/readme-graph.graphml)
(analysis-scripts/readme-graph.svg as lib/analysis-scripts/readme-graph.svg) (analysis-scripts/readme-graph.svg as lib/analysis-scripts/readme-graph.svg)
(analysis-scripts/README.md as lib/analysis-scripts/README.md) (analysis-scripts/README.md as lib/analysis-scripts/README.md)
(analysis-scripts/template.mk as lib/analysis-scripts/template.mk) (analysis-scripts/template.mk as lib/analysis-scripts/template.mk)
)) ))
; machdeps ; machdeps
...@@ -338,19 +72,8 @@ ...@@ -338,19 +72,8 @@
(package frama-c) (package frama-c)
(section share) (section share)
(files (files
(machdeps/machdep_avr_8.yaml as share/machdeps/machdep_avr_8.yaml) (glob_files (machdeps/*.yaml with_prefix share/machdeps))
(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)
)
)
; machdep generation script ; machdep generation script
(install (install
...@@ -365,56 +88,6 @@ ...@@ -365,56 +88,6 @@
(package frama-c) (package frama-c)
(section lib) (section lib)
(files (files
(machdeps/make_machdep/alignof_aligned.c as lib/make_machdep/alignof_aligned.c) (glob_files (machdeps/make_machdep/*.c with_prefix lib/make_machdep))
(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)
(machdeps/make_machdep/make_machdep_common.h as lib/make_machdep/make_machdep_common.h) (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)
)) ))
share/libc/__fc_machdep_linux_shared.h deleted 100644 → 0
+ 0
− 275
View file @ b5420b14
/**************************************************************************/
/* */
/* 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
share/libc/__fc_machdep_old.c deleted 100644 → 0
+ 0
− 796
View file @ b5420b14
This diff is collapsed.
src/plugins/e-acsl/dune
+ 1
− 78
View file @ abb088ab
...@@ -56,84 +56,7 @@ ...@@ -56,84 +56,7 @@
(files (files
(scripts/e-acsl-gcc.sh as e-acsl-gcc.sh))) (scripts/e-acsl-gcc.sh as e-acsl-gcc.sh)))
; SHARE
(install (install
(package frama-c-e-acsl) (package frama-c-e-acsl)
(section (site (frama-c share))) (section (site (frama-c share)))
(files (source_trees (share/e-acsl as e-acsl)))
; 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)
))
src/plugins/wp/dune
+ 2
− 14
View file @ abb088ab
...@@ -55,17 +55,5 @@ ...@@ -55,17 +55,5 @@
(install (install
(package frama-c-wp) (package frama-c-wp)
(section (site (frama-c share))) (section (site (frama-c share)))
(files (files (share/wp.driver as wp/wp.driver))
(share/Makefile.resources as wp/Makefile.resources) (source_trees (share/why3 as wp/why3)))
(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)))
src/plugins/wp/share/Makefile.resources deleted 100644 → 0
+ 0
− 60
View file @ b5420b14
##########################################################################
# #
# 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:
tests/libc/check_parsing_individual_headers.ml
+ 1
− 3
View file @ abb088ab
...@@ -8,9 +8,7 @@ let is_header f = Str.string_match header_re f 0 ...@@ -8,9 +8,7 @@ let is_header f = Str.string_match header_re f 0
(* Files which are *not* supposed to be parsed *) (* Files which are *not* supposed to be parsed *)
let blacklist libc_dir = let blacklist libc_dir =
List.map (fun f -> List.map (Datatype.Filepath.concat libc_dir) ["tgmath.h"; "complex.h"]
Datatype.Filepath.concat libc_dir f)
["tgmath.h"; "complex.h"; "__fc_machdep_linux_shared.h"]
(* only goes down one level, which is enough for the libc *) (* only goes down one level, which is enough for the libc *)
let collect_headers () = let collect_headers () =
......
tests/libc/fc_libc.c
+ 0
− 1
View file @ abb088ab
...@@ -93,7 +93,6 @@ ...@@ -93,7 +93,6 @@
#include "__fc_integer.h" #include "__fc_integer.h"
//#include "__fc_libc.h" //keep this; used by check_full_libc.sh //#include "__fc_libc.h" //keep this; used by check_full_libc.sh
#include "__fc_machdep.h" #include "__fc_machdep.h"
//#include "__fc_machdep_linux_shared.h" //keep this; used by check_full_libc.sh
#include "fcntl.h" #include "fcntl.h"
#include "__fc_select.h" #include "__fc_select.h"
#include "__fc_string_axiomatic.h" #include "__fc_string_axiomatic.h"
......
tests/libc/oracle/fc_libc.0.res.oracle
+ 1
− 1
View file @ abb088ab
...@@ -5,10 +5,10 @@ ...@@ -5,10 +5,10 @@
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [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:210: assertion got status valid.
[eva] fc_libc.c:211: 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:212: assertion got status valid.
[eva] fc_libc.c:213: assertion got status valid.
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment