[build] install share using source_trees

share/dune

@@ -23,262 +23,23 @@
 (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

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)))

src/plugins/wp/dune

@@ -57,15 +57,5 @@
   (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)))
+    (share/wp.driver as wp/wp.driver))
+  (source_trees (share/why3 as wp/why3)))