diff --git a/headers/header_spec.txt b/headers/header_spec.txt
deleted file mode 100644
index dc4e4537811af57290bad456a08eb235c871ad0a..0000000000000000000000000000000000000000
--- a/headers/header_spec.txt
+++ /dev/null
@@ -1,1960 +0,0 @@
-.force-reconfigure: .ignore
-.gitattributes: .ignore
-.gitignore: .ignore
-.gitlab-ci.yml: .ignore
-.mailmap: .ignore
-.make-clean: .ignore
-.make-clean-stamp: .ignore
-ALL_VERSIONS: .ignore
-Changelog: .ignore
-Changelog_detailed.md: .ignore
-INSTALL.md: .ignore
-Makefile: CEA_LGPL
-Makefile.generating: CEA_LGPL
-README.md: .ignore
-VERSION: .ignore
-VERSION_CODENAME: .ignore
-bin/.gitignore: .ignore
-bin/build-src-distrib.sh: CEA_LGPL
-bin/frama-c: CEA_LGPL
-bin/frama-c-config: CEA_LGPL
-bin/frama-c-script: CEA_LGPL
-bin/frama-c-gui: CEA_LGPL
-bin/frama-c-gui.byte: CEA_LGPL
-bin/frama-c.byte: CEA_LGPL
-bin/frama-c.debug: CEA_LGPL
-bin/frama-c.top: CEA_LGPL
-bin/local_export.sh: CEA_LGPL
-bin/migration_scripts/aluminium2silicon.sh: CEA_LGPL
-bin/migration_scripts/boron2carbon.sh: CEA_LGPL
-bin/migration_scripts/calcium2scandium.sh: CEA_LGPL
-bin/migration_scripts/carbon2nitrogen.sh: CEA_LGPL
-bin/migration_scripts/chlorine2argon.sh: CEA_LGPL
-bin/migration_scripts/chromium2manganese.sh: CEA_LGPL
-bin/migration_scripts/fluorine2neon.sh: CEA_LGPL
-bin/migration_scripts/lithium2beryllium.sh: CEA_LGPL
-bin/migration_scripts/magnesium2aluminium.sh: CEA_LGPL
-bin/migration_scripts/neon2sodium.sh: CEA_LGPL
-bin/migration_scripts/nitrogen2oxygen.sh: CEA_LGPL
-bin/migration_scripts/oxygen2fluorine.sh: CEA_LGPL
-bin/migration_scripts/phosphorus2sulfur.sh: CEA_LGPL
-bin/migration_scripts/potassium2calcium.sh: CEA_LGPL
-bin/migration_scripts/silicon2phosphorus.sh: CEA_LGPL
-bin/migration_scripts/sodium2magnesium.sh: CEA_LGPL
-bin/migration_scripts/sulfur2chlorine.sh: CEA_LGPL
-bin/migration_scripts/titanium2vanadium.sh: CEA_LGPL
-bin/migration_scripts/vanadium2chromium.sh: CEA_LGPL
-bin/sed_get_binutils_version: .ignore
-bin/sed_get_make_major: .ignore
-bin/sed_get_make_minor: .ignore
-config.h.in: CEA_LGPL
-configure.in: CEA_INRIA_LGPL
-devel_tools/size.ml: .ignore
-devel_tools/size.mli: .ignore
-doc/Makefile: CEA_LGPL
-doc/README: .ignore
-doc/code/docgen.ml: CEA_LGPL
-doc/code/intro_kernel_plugin.txt: CEA_LGPL
-doc/code/intro_occurrence.txt: CEA_LGPL
-doc/code/intro_pdg.txt: CEA_LGPL
-doc/code/intro_plugin.txt: CEA_LGPL
-doc/code/intro_plugin_D_and_S.txt: CEA_LGPL
-doc/code/intro_plugin_default.txt: CEA_LGPL
-doc/code/intro_scope.txt: CEA_LGPL
-doc/code/intro_slicing.txt: CEA_LGPL
-doc/code/intro_sparecode.txt: CEA_LGPL
-doc/code/style.css: CEA_LGPL
-doc/code/toc_head.htm: CEA_LGPL
-doc/code/toc_tail.htm: CEA_LGPL
-headers/close-source/AORAI_LGPL: .ignore
-headers/close-source/CEA_INRIA_LGPL: .ignore
-headers/close-source/CEA_LGPL: .ignore
-headers/close-source/CEA_LGPL_OR_PROPRIETARY: .ignore
-headers/close-source/CEA_PROPRIETARY: .ignore
-headers/close-source/CEA_PR_LGPL: .ignore
-headers/close-source/CEA_WP: .ignore
-headers/close-source/CIL: .ignore
-headers/close-source/INRIA_BSD: .ignore
-headers/close-source/INRIA_LGPL: .ignore
-headers/close-source/INSA_INRIA_LGPL: .ignore
-headers/close-source/MODIFIED_MENHIR: .ignore
-headers/close-source/MODIFIED_OCAMLGRAPH: .ignore
-headers/close-source/MODIFIED_WHY3: .ignore
-headers/close-source/OCAML_STDLIB: .ignore
-headers/close-source/UNMODIFIED_WHY3: .ignore
-headers/headache_config.txt: CEA_LGPL
-headers/header_spec.txt: .ignore
-headers/open-source/AORAI_LGPL: .ignore
-headers/open-source/CEA_INRIA_LGPL: .ignore
-headers/open-source/CEA_LGPL: .ignore
-headers/open-source/CEA_LGPL_OR_PROPRIETARY: .ignore
-headers/open-source/CEA_PROPRIETARY: .ignore
-headers/open-source/CEA_PR_LGPL: .ignore
-headers/open-source/CEA_WP: .ignore
-headers/open-source/CIL: .ignore
-headers/open-source/INRIA_BSD: .ignore
-headers/open-source/INRIA_LGPL: .ignore
-headers/open-source/INSA_INRIA_LGPL: .ignore
-headers/open-source/MODIFIED_MENHIR: .ignore
-headers/open-source/MODIFIED_OCAMLGRAPH: .ignore
-headers/open-source/MODIFIED_WHY3: .ignore
-headers/open-source/OCAML_STDLIB: .ignore
-headers/open-source/UNMODIFIED_WHY3: .ignore
-lib/plugins/PLUGINS.README: .ignore
-licenses/CDDL-1.0: .ignore
-licenses/LGPLv2: .ignore
-licenses/LGPLv2.1: .ignore
-licenses/Q_MODIFIED_LICENSE: .ignore
-man/frama-c.1: .ignore
-opam/opam: .ignore
-ptests/.gitignore: .ignore
-ptests/.merlin: .ignore
-ptests/ptests.ml: CEA_LGPL
-share/_frama-c: CEA_LGPL
-share/analysis-scripts/analysis.mk: CEA_LGPL
-share/analysis-scripts/benchmark_database.py: CEA_LGPL
-share/analysis-scripts/build.py: CEA_LGPL
-share/analysis-scripts/build_callgraph.py: CEA_LGPL
-share/analysis-scripts/clone.sh: CEA_LGPL
-share/analysis-scripts/creduce.sh: CEA_LGPL
-share/analysis-scripts/detect_recursion.py: CEA_LGPL
-share/analysis-scripts/epilogue.mk: CEA_LGPL
-share/analysis-scripts/estimate_difficulty.py: CEA_LGPL
-share/analysis-scripts/fc_stubs.c: CEA_LGPL
-share/analysis-scripts/frama_c_results.py: CEA_LGPL
-share/analysis-scripts/cmd-dep.sh: CEA_LGPL
-share/analysis-scripts/concat-csv.sh: CEA_LGPL
-share/analysis-scripts/find_fun.py: CEA_LGPL
-share/analysis-scripts/flamegraph.pl: CDDL
-share/analysis-scripts/function_finder.py: CEA_LGPL
-share/analysis-scripts/git_utils.py: CEA_LGPL
-share/analysis-scripts/heuristic_list_functions.py: CEA_LGPL
-share/analysis-scripts/list_files.py: CEA_LGPL
-share/analysis-scripts/list_functions.ml: CEA_LGPL
-share/analysis-scripts/make_wrapper.py: CEA_LGPL
-share/analysis-scripts/normalize_jcdb.py: CEA_LGPL
-share/analysis-scripts/parse-coverage.sh: CEA_LGPL
-share/analysis-scripts/print_callgraph.py: CEA_LGPL
-share/analysis-scripts/prologue.mk: CEA_LGPL
-share/analysis-scripts/pyproject.toml: .ignore
-share/analysis-scripts/README.md: .ignore
-share/analysis-scripts/results_display.py: CEA_LGPL
-share/analysis-scripts/script_for_creduce_fatal.sh: CEA_LGPL
-share/analysis-scripts/script_for_creduce_non_fatal.sh: CEA_LGPL
-share/analysis-scripts/source_filter.py: CEA_LGPL
-share/analysis-scripts/summary.py: CEA_LGPL
-share/analysis-scripts/template.mk: CEA_LGPL
-share/compliance/c11_functions.json: .ignore
-share/compliance/c11_headers.json: .ignore
-share/compliance/compiler_builtins.json: .ignore
-share/compliance/gcc_builtins.json: .ignore
-share/compliance/glibc_functions.json: .ignore
-share/compliance/nonstandard_identifiers.json: .ignore
-share/compliance/posix_identifiers.json: .ignore
-share/autocomplete_frama-c: CEA_LGPL
-share/Makefile.clean: CEA_LGPL
-share/Makefile.common: CEA_LGPL
-share/Makefile.config.in: CEA_LGPL
-share/Makefile.dynamic: CEA_LGPL
-share/Makefile.dynamic_config.external: CEA_LGPL
-share/Makefile.dynamic_config.internal: CEA_LGPL
-share/Makefile.generic: CEA_LGPL
-share/Makefile.plugin.template: CEA_LGPL
-share/META.frama-c: .ignore
-share/configure.ac: CEA_LGPL
-share/emacs/acsl.el: CEA_PR_LGPL
-share/emacs/frama-c-dev.el: CEA_LGPL
-share/emacs/frama-c-init.el: CEA_LGPL
-share/emacs/frama-c-recommended.el: CEA_LGPL
-share/frama-c-icon.svg: .ignore
-share/frama-c.Unix.rc: CEA_LGPL
-share/frama-c.WIN32.rc: CEA_LGPL
-share/frama-c.ico: .ignore
-share/frama-c.png: .ignore
-share/framac.vim: .ignore
-share/libc.c: CEA_LGPL
-share/libc/__fc_alloc_axiomatic.h: CEA_LGPL
-share/libc/__fc_builtin.c: CEA_LGPL
-share/libc/__fc_builtin.h: CEA_LGPL
-share/libc/__fc_define_blkcnt_t.h: CEA_LGPL
-share/libc/__fc_define_blksize_t.h: CEA_LGPL
-share/libc/__fc_define_clockid_t.h: CEA_LGPL
-share/libc/__fc_define_dev_t.h: CEA_LGPL
-share/libc/__fc_define_eof.h: CEA_LGPL
-share/libc/__fc_define_fd_set_t.h: CEA_LGPL
-share/libc/__fc_define_fds.h: CEA_LGPL
-share/libc/__fc_define_file.h: CEA_LGPL
-share/libc/__fc_define_fpos_t.h: CEA_LGPL
-share/libc/__fc_define_fs_cnt.h: CEA_LGPL
-share/libc/__fc_define_id_t.h: CEA_LGPL
-share/libc/__fc_define_ino_t.h: CEA_LGPL
-share/libc/__fc_define_intptr_t.h: CEA_LGPL
-share/libc/__fc_define_iovec.h: CEA_LGPL
-share/libc/__fc_define_key_t.h: CEA_LGPL
-share/libc/__fc_define_locale_t.h: CEA_LGPL
-share/libc/__fc_define_max_open_files.h: CEA_LGPL
-share/libc/__fc_define_mode_t.h: CEA_LGPL
-share/libc/__fc_define_nlink_t.h: CEA_LGPL
-share/libc/__fc_define_null.h: CEA_LGPL
-share/libc/__fc_define_off_t.h: CEA_LGPL
-share/libc/__fc_define_pid_t.h: CEA_LGPL
-share/libc/__fc_define_pthread_types.h: CEA_LGPL
-share/libc/__fc_define_sa_family_t.h: CEA_LGPL
-share/libc/__fc_define_seek_macros.h: CEA_LGPL
-share/libc/__fc_define_sigset_t.h: CEA_LGPL
-share/libc/__fc_define_size_t.h: CEA_LGPL
-share/libc/__fc_define_sockaddr.h: CEA_LGPL
-share/libc/__fc_define_ssize_t.h: CEA_LGPL
-share/libc/__fc_define_stat.h: CEA_LGPL
-share/libc/__fc_define_suseconds_t.h: CEA_LGPL
-share/libc/__fc_define_time_t.h: CEA_LGPL
-share/libc/__fc_define_timer_t.h: CEA_LGPL
-share/libc/__fc_define_timespec.h: CEA_LGPL
-share/libc/__fc_define_timeval.h: CEA_LGPL
-share/libc/__fc_define_uid_and_gid.h: CEA_LGPL
-share/libc/__fc_define_useconds_t.h: CEA_LGPL
-share/libc/__fc_define_wchar_t.h: CEA_LGPL
-share/libc/__fc_define_wint_t.h: CEA_LGPL
-share/libc/__fc_gcc_builtins.h: CEA_LGPL
-share/libc/__fc_inet.h: CEA_LGPL
-share/libc/__fc_integer.h: CEA_LGPL
-share/libc/__fc_libc.h: CEA_LGPL
-share/libc/__fc_machdep.h: CEA_LGPL
-share/libc/__fc_machdep_linux_shared.h: CEA_LGPL
-share/libc/__fc_runtime.c: CEA_LGPL
-share/libc/__fc_select.h: CEA_LGPL
-share/libc/__fc_string_axiomatic.h: CEA_LGPL
-share/libc/aio.h: CEA_LGPL
-share/libc/alloca.h: CEA_LGPL
-share/libc/argz.c: CEA_FSF_LGPL
-share/libc/argz.h: CEA_FSF_LGPL
-share/libc/arpa/inet.h: CEA_LGPL
-share/libc/assert.c: CEA_LGPL
-share/libc/assert.h: CEA_LGPL
-share/libc/byteswap.h: CEA_LGPL
-share/libc/complex.h: CEA_LGPL
-share/libc/cpio.h: CEA_LGPL
-share/libc/ctype.c: CEA_LGPL
-share/libc/ctype.h: CEA_LGPL
-share/libc/dirent.h: CEA_LGPL
-share/libc/dlfcn.h: CEA_LGPL
-share/libc/endian.h: CEA_LGPL
-share/libc/err.h: CEA_LGPL
-share/libc/errno.c: CEA_LGPL
-share/libc/errno.h: CEA_LGPL
-share/libc/fcntl.h: CEA_LGPL
-share/libc/features.h: CEA_LGPL
-share/libc/fenv.h: CEA_LGPL
-share/libc/fenv.c: CEA_LGPL
-share/libc/float.h: CEA_LGPL
-share/libc/fmtmsg.h: CEA_LGPL
-share/libc/fnmatch.h: CEA_LGPL
-share/libc/ftw.h: CEA_LGPL
-share/libc/getopt.c: CEA_LGPL
-share/libc/getopt.h: CEA_LGPL
-share/libc/glob.c: CEA_LGPL
-share/libc/glob.h: CEA_LGPL
-share/libc/grp.h: CEA_LGPL
-share/libc/iconv.h: CEA_LGPL
-share/libc/ifaddrs.h: CEA_LGPL
-share/libc/inttypes.c: CEA_LGPL
-share/libc/inttypes.h: CEA_LGPL
-share/libc/iso646.h: CEA_LGPL
-share/libc/langinfo.h: CEA_LGPL
-share/libc/libgen.h: CEA_LGPL
-share/libc/limits.h: CEA_LGPL
-share/libc/locale.c: CEA_LGPL
-share/libc/locale.h: CEA_LGPL
-share/libc/malloc.h: CEA_LGPL
-share/libc/math.c: CEA_LGPL
-share/libc/math.h: CEA_LGPL
-share/libc/memory.h: CEA_LGPL
-share/libc/monetary.h: CEA_LGPL
-share/libc/mqueue.h: CEA_LGPL
-share/libc/n1336.pdf: .ignore
-share/libc/n1362.pdf: .ignore
-share/libc/ndbm.h: CEA_LGPL
-share/libc/net/if.h: CEA_LGPL
-share/libc/netdb.c: CEA_LGPL
-share/libc/netdb.h: CEA_LGPL
-share/libc/netinet/in.c: CEA_LGPL
-share/libc/netinet/in.h: CEA_LGPL
-share/libc/netinet/ip.h: CEA_LGPL
-share/libc/netinet/tcp.h: CEA_LGPL
-share/libc/nl_types.h: CEA_LGPL
-share/libc/poll.h: CEA_LGPL
-share/libc/pthread.h: CEA_LGPL
-share/libc/pwd.c: CEA_LGPL
-share/libc/pwd.h: CEA_LGPL
-share/libc/regex.h: CEA_LGPL
-share/libc/resolv.h: CEA_LGPL
-share/libc/sched.h: CEA_LGPL
-share/libc/search.h: CEA_LGPL
-share/libc/semaphore.h: CEA_LGPL
-share/libc/setjmp.h: CEA_LGPL
-share/libc/signal.c: CEA_LGPL
-share/libc/signal.h: CEA_LGPL
-share/libc/spawn.h: CEA_LGPL
-share/libc/stdalign.h: CEA_LGPL
-share/libc/stdarg.h: CEA_LGPL
-share/libc/stdatomic.c: CEA_LGPL
-share/libc/stdatomic.h: CEA_LGPL
-share/libc/stdbool.h: CEA_LGPL
-share/libc/stddef.h: CEA_LGPL
-share/libc/stdint.h: CEA_LGPL
-share/libc/stdio.c: CEA_LGPL
-share/libc/stdio.h: CEA_LGPL
-share/libc/stdlib.c: CEA_LGPL
-share/libc/stdlib.h: CEA_LGPL
-share/libc/stdnoreturn.h: CEA_LGPL
-share/libc/string.c: CEA_LGPL
-share/libc/string.h: CEA_LGPL
-share/libc/strings.h: CEA_LGPL
-share/libc/stropts.h: CEA_LGPL
-share/libc/sys/file.h: CEA_LGPL
-share/libc/sys/ioctl.h: CEA_LGPL
-share/libc/sys/ipc.h: CEA_LGPL
-share/libc/sys/mman.h: CEA_LGPL
-share/libc/sys/msg.h: CEA_LGPL
-share/libc/sys/param.h: CEA_LGPL
-share/libc/sys/random.h: CEA_LGPL
-share/libc/sys/resource.h: CEA_LGPL
-share/libc/sys/select.h: CEA_LGPL
-share/libc/sys/sendfile.h: CEA_LGPL
-share/libc/sys/sem.h: CEA_LGPL
-share/libc/sys/shm.h: CEA_LGPL
-share/libc/sys/signal.h: CEA_LGPL
-share/libc/sys/socket.h: CEA_LGPL
-share/libc/sys/stat.h: CEA_LGPL
-share/libc/sys/statvfs.h: CEA_LGPL
-share/libc/sys/time.h: CEA_LGPL
-share/libc/sys/times.h: CEA_LGPL
-share/libc/sys/timex.h: CEA_LGPL
-share/libc/sys/types.h: CEA_LGPL
-share/libc/sys/uio.h: CEA_LGPL
-share/libc/sys/un.h: CEA_LGPL
-share/libc/sys/utsname.h: CEA_LGPL
-share/libc/sys/vfs.h: CEA_LGPL
-share/libc/sys/wait.h: CEA_LGPL
-share/libc/syslog.h: CEA_LGPL
-share/libc/tar.h: CEA_LGPL
-share/libc/termios.h: CEA_LGPL
-share/libc/tgmath.h: CEA_LGPL
-share/libc/time.c: CEA_LGPL
-share/libc/time.h: CEA_LGPL
-share/libc/trace.h: CEA_LGPL
-share/libc/ulimit.h: CEA_LGPL
-share/libc/unistd.c: CEA_LGPL
-share/libc/unistd.h: CEA_LGPL
-share/libc/utime.h: CEA_LGPL
-share/libc/utmp.h: CEA_LGPL
-share/libc/utmpx.h: CEA_LGPL
-share/libc/wait.h: CEA_LGPL
-share/libc/wchar.c: CEA_LGPL
-share/libc/wchar.h: CEA_LGPL
-share/libc/wctype.h: CEA_LGPL
-share/libc/wordexp.h: CEA_LGPL
-share/machdep.c: CIL
-share/switch-off.png: .ignore
-share/switch-on.png: .ignore
-share/theme/colorblind/considered_valid.png: .ignore
-share/theme/colorblind/inconsistent.png: .ignore
-share/theme/colorblind/invalid_but_dead.png: .ignore
-share/theme/colorblind/invalid_under_hyp.png: .ignore
-share/theme/colorblind/never_tried.png: .ignore
-share/theme/colorblind/surely_invalid.png: .ignore
-share/theme/colorblind/surely_valid.png: .ignore
-share/theme/colorblind/unknown.png: .ignore
-share/theme/colorblind/unknown_but_dead.png: .ignore
-share/theme/colorblind/valid_but_dead.png: .ignore
-share/theme/colorblind/valid_under_hyp.png: .ignore
-share/theme/colorblind/fold.png: .ignore
-share/theme/colorblind/unfold.png: .ignore
-share/theme/default/considered_valid.png: .ignore
-share/theme/default/inconsistent.png: .ignore
-share/theme/default/invalid_but_dead.png: .ignore
-share/theme/default/invalid_under_hyp.png: .ignore
-share/theme/default/never_tried.png: .ignore
-share/theme/default/surely_invalid.png: .ignore
-share/theme/default/surely_valid.png: .ignore
-share/theme/default/unknown.png: .ignore
-share/theme/default/unknown_but_dead.png: .ignore
-share/theme/default/valid_but_dead.png: .ignore
-share/theme/default/valid_under_hyp.png: .ignore
-share/theme/default/fold.png: .ignore
-share/theme/default/unfold.png: .ignore
-share/theme/flat/considered_valid.png: .ignore
-share/theme/flat/inconsistent.png: .ignore
-share/theme/flat/invalid_but_dead.png: .ignore
-share/theme/flat/invalid_under_hyp.png: .ignore
-share/theme/flat/never_tried.png: .ignore
-share/theme/flat/surely_invalid.png: .ignore
-share/theme/flat/surely_valid.png: .ignore
-share/theme/flat/unknown.png: .ignore
-share/theme/flat/unknown_but_dead.png: .ignore
-share/theme/flat/valid_but_dead.png: .ignore
-share/theme/flat/valid_under_hyp.png: .ignore
-share/theme/flat/fold.png: .ignore
-share/theme/flat/unfold.png: .ignore
-share/unmark.png: .ignore
-share/win32_installer.iss: .ignore
-share/win32_manual_installation_step.txt: .ignore
-src/kernel_internals/README.md: .ignore
-src/kernel_internals/parsing/README.md: .ignore
-src/kernel_internals/parsing/check_logic_parser.ml: CEA_LGPL
-src/kernel_internals/parsing/clexer.mli: CIL
-src/kernel_internals/parsing/clexer.mll: CIL
-src/kernel_internals/parsing/cparser.mly: CIL
-src/kernel_internals/parsing/errorloc.ml: CIL
-src/kernel_internals/parsing/errorloc.mli: CIL
-src/kernel_internals/parsing/lexerhack.ml: CIL
-src/kernel_internals/parsing/lexerhack.mli: CIL
-src/kernel_internals/parsing/logic_lexer.mli: CEA_INRIA_LGPL
-src/kernel_internals/parsing/logic_lexer.mll: CEA_INRIA_LGPL
-src/kernel_internals/parsing/logic_parser.mly: CEA_INRIA_LGPL
-src/kernel_internals/parsing/logic_preprocess.mli: CEA_INRIA_LGPL
-src/kernel_internals/parsing/logic_preprocess.mll: CEA_INRIA_LGPL
-src/kernel_internals/parsing/parse_env.ml: CEA_LGPL
-src/kernel_internals/parsing/parse_env.mli: CEA_LGPL
-src/kernel_internals/runtime/README.md: .ignore
-src/kernel_internals/runtime/boot.ml: CEA_LGPL
-src/kernel_internals/runtime/boot.mli: CEA_LGPL
-src/kernel_internals/runtime/dump_config.ml: CEA_LGPL
-src/kernel_internals/runtime/dump_config.mli: CEA_LGPL
-src/kernel_internals/runtime/fc_config.ml.in: CEA_LGPL
-src/kernel_internals/runtime/fc_config.mli: CEA_LGPL
-src/kernel_internals/runtime/frama_c_init.ml: CEA_LGPL
-src/kernel_internals/runtime/frama_c_init.mli: CEA_LGPL
-src/kernel_internals/runtime/gui_init.ml: CEA_LGPL
-src/kernel_internals/runtime/gui_init.mli: CEA_LGPL
-src/kernel_internals/runtime/machdeps.ml: CIL
-src/kernel_internals/runtime/machdeps.mli: CIL
-src/kernel_internals/runtime/messages.ml: CEA_LGPL
-src/kernel_internals/runtime/messages.mli: CEA_LGPL
-src/kernel_internals/runtime/special_hooks.ml: CEA_LGPL
-src/kernel_internals/runtime/special_hooks.mli: CEA_LGPL
-src/kernel_internals/runtime/toplevel_config.ml: CEA_LGPL
-src/kernel_internals/typing/README.md: .ignore
-src/kernel_internals/typing/allocates.ml: CEA_LGPL
-src/kernel_internals/typing/allocates.mli: CEA_LGPL
-src/kernel_internals/typing/alpha.ml: CIL
-src/kernel_internals/typing/alpha.mli: CIL
-src/kernel_internals/typing/asm_contracts.ml: CEA_LGPL
-src/kernel_internals/typing/asm_contracts.mli: CEA_LGPL
-src/kernel_internals/typing/cabs2cil.ml: CIL
-src/kernel_internals/typing/cabs2cil.mli: CIL
-src/kernel_internals/typing/cfg.ml: CIL
-src/kernel_internals/typing/cfg.mli: CIL
-src/kernel_internals/typing/frontc.ml: CIL
-src/kernel_internals/typing/frontc.mli: CIL
-src/kernel_internals/typing/ghost_accesses.ml: CEA_LGPL
-src/kernel_internals/typing/ghost_accesses.mli: CEA_LGPL
-src/kernel_internals/typing/ghost_cfg.ml: CEA_LGPL
-src/kernel_internals/typing/ghost_cfg.mli: CEA_LGPL
-src/kernel_internals/typing/infer_annotations.ml: CEA_LGPL
-src/kernel_internals/typing/infer_annotations.mli: CEA_LGPL
-src/kernel_internals/typing/logic_builtin.ml: CEA_INRIA_LGPL
-src/kernel_internals/typing/logic_builtin.mli: CEA_INRIA_LGPL
-src/kernel_internals/typing/mergecil.ml: CIL
-src/kernel_internals/typing/mergecil.mli: CIL
-src/kernel_internals/typing/oneret.ml: CIL
-src/kernel_internals/typing/oneret.mli: CIL
-src/kernel_internals/typing/rmtmps.ml: CIL
-src/kernel_internals/typing/rmtmps.mli: CIL
-src/kernel_internals/typing/translate_lightweight.ml: CEA_INRIA_LGPL
-src/kernel_internals/typing/translate_lightweight.mli: CEA_INRIA_LGPL
-src/kernel_internals/typing/unroll_loops.ml: CEA_LGPL
-src/kernel_internals/typing/unroll_loops.mli: CEA_LGPL
-src/kernel_internals/typing/substitute_const_globals.ml: CEA_LGPL
-src/kernel_internals/typing/substitute_const_globals.mli: CEA_LGPL
-src/kernel_services/README.md: .ignore
-src/kernel_services/abstract_interp/README.md: .ignore
-src/kernel_services/abstract_interp/abstract_interp.ml: CEA_LGPL
-src/kernel_services/abstract_interp/abstract_interp.mli: CEA_LGPL
-src/kernel_services/abstract_interp/base.ml: CEA_LGPL
-src/kernel_services/abstract_interp/base.mli: CEA_LGPL
-src/kernel_services/abstract_interp/eva_lattice_type.mli: CEA_LGPL
-src/kernel_services/abstract_interp/fc_float.ml: CEA_LGPL
-src/kernel_services/abstract_interp/fc_float.mli: CEA_LGPL
-src/kernel_services/abstract_interp/float_sig.mli: CEA_LGPL
-src/kernel_services/abstract_interp/float_interval.ml: CEA_LGPL
-src/kernel_services/abstract_interp/float_interval.mli: CEA_LGPL
-src/kernel_services/abstract_interp/float_interval_sig.mli: CEA_LGPL
-src/kernel_services/abstract_interp/fval.ml: CEA_LGPL
-src/kernel_services/abstract_interp/fval.mli: CEA_LGPL
-src/kernel_services/abstract_interp/int_Base.ml: CEA_LGPL
-src/kernel_services/abstract_interp/int_Base.mli: CEA_LGPL
-src/kernel_services/abstract_interp/int_Intervals.ml: CEA_LGPL
-src/kernel_services/abstract_interp/int_Intervals.mli: CEA_LGPL
-src/kernel_services/abstract_interp/int_Intervals_sig.mli: CEA_LGPL
-src/kernel_services/abstract_interp/int_interval.ml: CEA_LGPL
-src/kernel_services/abstract_interp/int_interval.mli: CEA_LGPL
-src/kernel_services/abstract_interp/int_set.ml: CEA_LGPL
-src/kernel_services/abstract_interp/int_set.mli: CEA_LGPL
-src/kernel_services/abstract_interp/int_val.ml: CEA_LGPL
-src/kernel_services/abstract_interp/int_val.mli: CEA_LGPL
-src/kernel_services/abstract_interp/ival.ml: CEA_LGPL
-src/kernel_services/abstract_interp/ival.mli: CEA_LGPL
-src/kernel_services/abstract_interp/lattice_bounds.ml: CEA_LGPL
-src/kernel_services/abstract_interp/lattice_bounds.mli: CEA_LGPL
-src/kernel_services/abstract_interp/lattice_messages.ml: CEA_LGPL
-src/kernel_services/abstract_interp/lattice_messages.mli: CEA_LGPL
-src/kernel_services/abstract_interp/lattice_type.mli: CEA_LGPL
-src/kernel_services/abstract_interp/lmap.ml: CEA_LGPL
-src/kernel_services/abstract_interp/lmap.mli: CEA_LGPL
-src/kernel_services/abstract_interp/lmap_bitwise.ml: CEA_LGPL
-src/kernel_services/abstract_interp/lmap_bitwise.mli: CEA_LGPL
-src/kernel_services/abstract_interp/lmap_sig.mli: CEA_LGPL
-src/kernel_services/abstract_interp/locations.ml: CEA_LGPL
-src/kernel_services/abstract_interp/locations.mli: CEA_LGPL
-src/kernel_services/abstract_interp/map_lattice.ml: CEA_LGPL
-src/kernel_services/abstract_interp/map_lattice.mli: CEA_LGPL
-src/kernel_services/abstract_interp/offsetmap.ml: CEA_LGPL
-src/kernel_services/abstract_interp/offsetmap.mli: CEA_LGPL
-src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli: CEA_LGPL
-src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli: CEA_LGPL
-src/kernel_services/abstract_interp/offsetmap_sig.mli: CEA_LGPL
-src/kernel_services/abstract_interp/origin.ml: CEA_LGPL
-src/kernel_services/abstract_interp/origin.mli: CEA_LGPL
-src/kernel_services/abstract_interp/tr_offset.ml: CEA_LGPL
-src/kernel_services/abstract_interp/tr_offset.mli: CEA_LGPL
-src/kernel_services/analysis/README.md: .ignore
-src/kernel_services/analysis/bit_utils.ml: CEA_LGPL
-src/kernel_services/analysis/bit_utils.mli: CEA_LGPL
-src/kernel_services/analysis/dataflow2.ml: CEA_LGPL
-src/kernel_services/analysis/dataflow2.mli: CEA_LGPL
-src/kernel_services/analysis/dataflows.ml: CIL
-src/kernel_services/analysis/dataflows.mli: CIL
-src/kernel_services/analysis/destructors.ml: CEA_LGPL
-src/kernel_services/analysis/destructors.mli: CEA_LGPL
-src/kernel_services/analysis/dominators.ml: CEA_LGPL
-src/kernel_services/analysis/dominators.mli: CEA_LGPL
-src/kernel_services/analysis/exn_flow.ml: CEA_LGPL
-src/kernel_services/analysis/exn_flow.mli: CEA_LGPL
-src/kernel_services/analysis/interpreted_automata.ml: CEA_LGPL
-src/kernel_services/analysis/interpreted_automata.mli: CEA_LGPL
-src/kernel_services/analysis/logic_interp.ml: CEA_LGPL
-src/kernel_services/analysis/logic_interp.mli: CEA_LGPL
-src/kernel_services/analysis/loop.ml: CEA_LGPL
-src/kernel_services/analysis/loop.mli: CEA_LGPL
-src/kernel_services/analysis/ordered_stmt.ml: CEA_LGPL
-src/kernel_services/analysis/ordered_stmt.mli: CEA_LGPL
-src/kernel_services/analysis/service_graph.ml: CEA_LGPL
-src/kernel_services/analysis/service_graph.mli: CEA_LGPL
-src/kernel_services/analysis/stmts_graph.ml: CEA_LGPL
-src/kernel_services/analysis/stmts_graph.mli: CEA_LGPL
-src/kernel_services/analysis/undefined_sequence.ml: CEA_LGPL
-src/kernel_services/analysis/undefined_sequence.mli: CEA_LGPL
-src/kernel_services/analysis/wto_statement.ml: CEA_LGPL
-src/kernel_services/analysis/wto_statement.mli: CEA_LGPL
-src/kernel_services/ast_building/cil_builder.ml: CEA_LGPL
-src/kernel_services/ast_building/cil_builder.mli: CEA_LGPL
-src/kernel_services/ast_data/README.md: .ignore
-src/kernel_services/ast_data/alarms.ml: CEA_LGPL
-src/kernel_services/ast_data/alarms.mli: CEA_LGPL
-src/kernel_services/ast_data/annotations.ml: CEA_LGPL
-src/kernel_services/ast_data/annotations.mli: CEA_LGPL
-src/kernel_services/ast_data/ast.ml: CEA_LGPL
-src/kernel_services/ast_data/ast.mli: CEA_LGPL
-src/kernel_services/ast_data/cil_types.mli: CIL
-src/kernel_services/ast_printing/cil_types_debug.ml: CEA_LGPL
-src/kernel_services/ast_printing/cil_types_debug.mli: CEA_LGPL
-src/kernel_services/ast_data/globals.ml: CEA_LGPL
-src/kernel_services/ast_data/globals.mli: CEA_LGPL
-src/kernel_services/ast_data/kernel_function.ml: CEA_LGPL
-src/kernel_services/ast_data/kernel_function.mli: CEA_LGPL
-src/kernel_services/ast_data/property.ml: CEA_LGPL
-src/kernel_services/ast_data/property.mli: CEA_LGPL
-src/kernel_services/ast_data/property_status.ml: CEA_LGPL
-src/kernel_services/ast_data/property_status.mli: CEA_LGPL
-src/kernel_services/ast_data/statuses_by_call.ml: CEA_LGPL
-src/kernel_services/ast_data/statuses_by_call.mli: CEA_LGPL
-src/kernel_services/ast_printing/cabs_debug.ml: CEA_LGPL
-src/kernel_services/ast_printing/cabs_debug.mli: CEA_LGPL
-src/kernel_services/ast_printing/cil_descriptive_printer.ml: CEA_LGPL
-src/kernel_services/ast_printing/cil_descriptive_printer.mli: CEA_LGPL
-src/kernel_services/ast_printing/cil_printer.ml: CEA_LGPL
-src/kernel_services/ast_printing/cil_printer.mli: CEA_LGPL
-src/kernel_services/ast_printing/cprint.ml: CIL
-src/kernel_services/ast_printing/cprint.mli: CIL
-src/kernel_services/ast_printing/description.ml: CEA_LGPL
-src/kernel_services/ast_printing/description.mli: CEA_LGPL
-src/kernel_services/ast_printing/logic_print.ml: CEA_INRIA_LGPL
-src/kernel_services/ast_printing/logic_print.mli: CEA_INRIA_LGPL
-src/kernel_services/ast_printing/printer.ml: CEA_LGPL
-src/kernel_services/ast_printing/printer.mli: CEA_LGPL
-src/kernel_services/ast_printing/printer_api.mli: CEA_LGPL
-src/kernel_services/ast_printing/printer_builder.ml: CEA_LGPL
-src/kernel_services/ast_printing/printer_builder.mli: CEA_LGPL
-src/kernel_services/ast_printing/printer_tag.ml: CEA_LGPL
-src/kernel_services/ast_printing/printer_tag.mli: CEA_LGPL
-src/kernel_services/ast_queries/README.md: .ignore
-src/kernel_services/ast_queries/acsl_extension.ml: CEA_LGPL
-src/kernel_services/ast_queries/acsl_extension.mli: CEA_LGPL
-src/kernel_services/ast_queries/ast_diff.ml: CEA_LGPL
-src/kernel_services/ast_queries/ast_diff.mli: CEA_LGPL
-src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL
-src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL
-src/kernel_services/ast_queries/cil.ml: CIL
-src/kernel_services/ast_queries/cil.mli: CIL
-src/kernel_services/ast_queries/cil_builtins.ml: CIL
-src/kernel_services/ast_queries/cil_builtins.mli: CIL
-src/kernel_services/ast_queries/cil_const.ml: CIL
-src/kernel_services/ast_queries/cil_const.mli: CIL
-src/kernel_services/ast_queries/cil_datatype.ml: CEA_LGPL
-src/kernel_services/ast_queries/cil_datatype.mli: CEA_LGPL
-src/kernel_services/ast_queries/cil_state_builder.ml: CEA_LGPL
-src/kernel_services/ast_queries/cil_state_builder.mli: CEA_LGPL
-src/kernel_services/ast_queries/file.ml: CEA_LGPL
-src/kernel_services/ast_queries/file.mli: CEA_LGPL
-src/kernel_services/ast_queries/filecheck.ml: CEA_LGPL
-src/kernel_services/ast_queries/filecheck.mli: CEA_LGPL
-src/kernel_services/ast_queries/json_compilation_database.ml: CEA_LGPL
-src/kernel_services/ast_queries/json_compilation_database.mli: CEA_LGPL
-src/kernel_services/ast_queries/logic_const.ml: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_const.mli: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_env.ml: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_env.mli: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_typing.ml: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_typing.mli: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_utils.ml: CEA_INRIA_LGPL
-src/kernel_services/ast_queries/logic_utils.mli: CEA_INRIA_LGPL
-src/kernel_services/ast_transformations/README.md: .ignore
-src/kernel_services/ast_transformations/contract_special_float.ml: CEA_LGPL
-src/kernel_services/ast_transformations/contract_special_float.mli: CEA_LGPL
-src/kernel_services/ast_transformations/clone.ml: CEA_LGPL
-src/kernel_services/ast_transformations/clone.mli: CEA_LGPL
-src/kernel_services/ast_transformations/filter.ml: CEA_LGPL
-src/kernel_services/ast_transformations/filter.mli: CEA_LGPL
-src/kernel_services/ast_transformations/inline.ml: CEA_LGPL
-src/kernel_services/ast_transformations/inline.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/README.md: .ignore
-src/kernel_services/cmdline_parameters/cmdline.ml: CEA_LGPL
-src/kernel_services/cmdline_parameters/cmdline.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_builder.ml: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_builder.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_category.ml: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_category.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_customize.ml: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_customize.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_sig.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_state.ml: CEA_LGPL
-src/kernel_services/cmdline_parameters/parameter_state.mli: CEA_LGPL
-src/kernel_services/cmdline_parameters/typed_parameter.ml: CEA_LGPL
-src/kernel_services/cmdline_parameters/typed_parameter.mli: CEA_LGPL
-src/kernel_services/parsetree/README.md: .ignore
-src/kernel_services/parsetree/cabs.mli: CIL
-src/kernel_services/parsetree/cabshelper.ml: CIL
-src/kernel_services/parsetree/cabshelper.mli: CIL
-src/kernel_services/parsetree/logic_ptree.mli: CEA_INRIA_LGPL
-src/kernel_services/plugin_entry_points/README.md: .ignore
-src/kernel_services/plugin_entry_points/db.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/db.mli: CEA_LGPL
-src/kernel_services/plugin_entry_points/dynamic.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/dynamic.mli: CEA_LGPL
-src/kernel_services/plugin_entry_points/emitter.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/emitter.mli: CEA_LGPL
-src/kernel_services/plugin_entry_points/kernel.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/kernel.mli: CEA_LGPL
-src/kernel_services/plugin_entry_points/log.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/log.mli: CEA_LGPL
-src/kernel_services/plugin_entry_points/plugin.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/plugin.mli: CEA_LGPL
-src/kernel_services/visitors/README.md: .ignore
-src/kernel_services/visitors/cabsvisit.ml: CIL
-src/kernel_services/visitors/cabsvisit.mli: CIL
-src/kernel_services/visitors/visitor.ml: CEA_LGPL
-src/kernel_services/visitors/visitor.mli: CEA_LGPL
-src/kernel_services/visitors/visitor_behavior.ml: CEA_INRIA_LGPL
-src/kernel_services/visitors/visitor_behavior.mli: CEA_INRIA_LGPL
-src/libraries/README.md: .ignore
-src/libraries/datatype/README.md: .ignore
-src/libraries/datatype/datatype.ml: CEA_LGPL
-src/libraries/datatype/datatype.mli: CEA_LGPL
-src/libraries/datatype/descr.ml: CEA_LGPL
-src/libraries/datatype/descr.mli: CEA_LGPL
-src/libraries/datatype/structural_descr.ml: CEA_LGPL
-src/libraries/datatype/structural_descr.mli: CEA_LGPL
-src/libraries/datatype/type.ml: CEA_LGPL
-src/libraries/datatype/type.mli: CEA_LGPL
-src/libraries/datatype/unmarshal.ml: INRIA_BSD
-src/libraries/datatype/unmarshal.mli: INRIA_BSD
-src/libraries/datatype/unmarshal_hashtbl_test.ml: INRIA_BSD
-src/libraries/datatype/unmarshal_test.ml: INRIA_BSD
-src/libraries/datatype/unmarshal_z.ml: CEA_LGPL
-src/libraries/datatype/unmarshal_z.mli: CEA_LGPL
-src/libraries/project/README.md: .ignore
-src/libraries/project/project.ml: CEA_LGPL
-src/libraries/project/project.mli: CEA_LGPL
-src/libraries/project/project_skeleton.ml: CEA_LGPL
-src/libraries/project/project_skeleton.mli: CEA_LGPL
-src/libraries/project/state.ml: CEA_LGPL
-src/libraries/project/state.mli: CEA_LGPL
-src/libraries/project/state_builder.ml: CEA_LGPL
-src/libraries/project/state_builder.mli: CEA_LGPL
-src/libraries/project/state_dependency_graph.ml: CEA_LGPL
-src/libraries/project/state_dependency_graph.mli: CEA_LGPL
-src/libraries/project/state_selection.ml: CEA_LGPL
-src/libraries/project/state_selection.mli: CEA_LGPL
-src/libraries/project/state_topological.ml: MODIFIED_OCAMLGRAPH
-src/libraries/project/state_topological.mli: MODIFIED_OCAMLGRAPH
-src/libraries/stdlib/FCHashtbl.ml: CEA_LGPL
-src/libraries/stdlib/FCHashtbl.mli: CEA_LGPL
-src/libraries/stdlib/README.md: .ignore
-src/libraries/stdlib/extlib.ml: CEA_LGPL
-src/libraries/stdlib/extlib.mli: CEA_LGPL
-src/libraries/stdlib/integer.ml: CEA_LGPL
-src/libraries/stdlib/integer.mli: CEA_LGPL
-src/libraries/stdlib/transitioning.ml.in: CEA_LGPL
-src/libraries/stdlib/transitioning.mli: CEA_LGPL
-src/libraries/utils/README.md: .ignore
-src/libraries/utils/bag.ml: CEA_LGPL
-src/libraries/utils/bag.mli: CEA_LGPL
-src/libraries/utils/json.mll: CEA_LGPL
-src/libraries/utils/json.mli: CEA_LGPL
-src/libraries/utils/binary_cache.ml: CEA_LGPL
-src/libraries/utils/binary_cache.mli: CEA_LGPL
-src/libraries/utils/bitvector.ml: CEA_LGPL
-src/libraries/utils/bitvector.mli: CEA_LGPL
-src/libraries/utils/c_bindings.c: CEA_LGPL
-src/libraries/utils/cilconfig.ml: CIL
-src/libraries/utils/cilconfig.mli: CIL
-src/libraries/utils/command.ml: CEA_LGPL
-src/libraries/utils/command.mli: CEA_LGPL
-src/libraries/utils/dotgraph.ml: CEA_LGPL
-src/libraries/utils/dotgraph.mli: CEA_LGPL
-src/libraries/utils/escape.ml: CIL
-src/libraries/utils/escape.mli: CIL
-src/libraries/utils/filepath.ml: CEA_LGPL
-src/libraries/utils/filepath.mli: CEA_LGPL
-src/libraries/utils/floating_point.ml: CEA_LGPL
-src/libraries/utils/floating_point.mli: CEA_LGPL
-src/libraries/utils/hook.ml: CEA_LGPL
-src/libraries/utils/hook.mli: CEA_LGPL
-src/libraries/utils/hptmap.ml: MODIFIED_MENHIR
-src/libraries/utils/hptmap.mli: MODIFIED_MENHIR
-src/libraries/utils/hptmap_sig.mli: MODIFIED_MENHIR
-src/libraries/utils/hptset.ml: CEA_LGPL
-src/libraries/utils/hptset.mli: CEA_LGPL
-src/libraries/utils/indexer.ml: CEA_LGPL
-src/libraries/utils/indexer.mli: CEA_LGPL
-src/libraries/utils/markdown.ml: CEA_LGPL
-src/libraries/utils/markdown.mli: CEA_LGPL
-src/libraries/utils/pretty_utils.ml: CEA_LGPL
-src/libraries/utils/pretty_utils.mli: CEA_LGPL
-src/libraries/utils/qstack.ml: CEA_LGPL
-src/libraries/utils/qstack.mli: CEA_LGPL
-src/libraries/utils/rangemap.ml: OCAML_STDLIB
-src/libraries/utils/rangemap.mli: OCAML_STDLIB
-src/libraries/utils/rgmap.ml: CEA_LGPL
-src/libraries/utils/rgmap.mli: CEA_LGPL
-src/libraries/utils/rich_text.ml: CEA_LGPL
-src/libraries/utils/rich_text.mli: CEA_LGPL
-src/libraries/utils/sanitizer.ml: CEA_LGPL
-src/libraries/utils/sanitizer.mli: CEA_LGPL
-src/libraries/utils/task.ml: CEA_LGPL
-src/libraries/utils/task.mli: CEA_LGPL
-src/libraries/utils/unicode.ml: CEA_LGPL
-src/libraries/utils/unicode.mli: CEA_LGPL
-src/libraries/utils/utf8_logic.ml: CEA_INRIA_LGPL
-src/libraries/utils/utf8_logic.mli: CEA_INRIA_LGPL
-src/libraries/utils/vector.ml: CEA_LGPL
-src/libraries/utils/vector.mli: CEA_LGPL
-src/libraries/utils/wto.ml: CEA_LGPL
-src/libraries/utils/wto.mli: CEA_LGPL
-src/plugins/README.md: .ignore
-src/plugins/aorai/.gitignore: .ignore
-src/plugins/aorai/Aorai.mli: AORAI_LGPL
-src/plugins/aorai/INSTALL: .ignore
-src/plugins/aorai/Makefile.in: AORAI_LGPL
-src/plugins/aorai/VERSIONS.txt: .ignore
-src/plugins/aorai/YA.README: .ignore
-src/plugins/aorai/aorai_dataflow.ml: AORAI_LGPL
-src/plugins/aorai/aorai_dataflow.mli: AORAI_LGPL
-src/plugins/aorai/aorai_eva_analysis.disabled.ml: AORAI_LGPL
-src/plugins/aorai/aorai_eva_analysis.enabled.ml: AORAI_LGPL
-src/plugins/aorai/aorai_eva_analysis.mli: AORAI_LGPL
-src/plugins/aorai/aorai_graph.ml: AORAI_LGPL
-src/plugins/aorai/aorai_graph.mli: AORAI_LGPL
-src/plugins/aorai/aorai_metavariables.ml: AORAI_LGPL
-src/plugins/aorai/aorai_metavariables.mli: AORAI_LGPL
-src/plugins/aorai/aorai_option.ml: AORAI_LGPL
-src/plugins/aorai/aorai_option.mli: AORAI_LGPL
-src/plugins/aorai/aorai_register.ml: AORAI_LGPL
-src/plugins/aorai/aorai_register.mli: AORAI_LGPL
-src/plugins/aorai/aorai_utils.ml: AORAI_LGPL
-src/plugins/aorai/aorai_utils.mli: AORAI_LGPL
-src/plugins/aorai/aorai_visitors.ml: AORAI_LGPL
-src/plugins/aorai/aorai_visitors.mli: AORAI_LGPL
-src/plugins/aorai/bool3.ml: AORAI_LGPL
-src/plugins/aorai/bool3.mli: AORAI_LGPL
-src/plugins/aorai/configure.ac: AORAI_LGPL
-src/plugins/aorai/data_for_aorai.ml: AORAI_LGPL
-src/plugins/aorai/data_for_aorai.mli: AORAI_LGPL
-src/plugins/aorai/logic_simplification.ml: AORAI_LGPL
-src/plugins/aorai/logic_simplification.mli: AORAI_LGPL
-src/plugins/aorai/ltl_output.ml: AORAI_LGPL
-src/plugins/aorai/ltl_output.mli: AORAI_LGPL
-src/plugins/aorai/ltlast.mli: AORAI_LGPL
-src/plugins/aorai/ltllexer.mli: AORAI_LGPL
-src/plugins/aorai/ltllexer.mll: AORAI_LGPL
-src/plugins/aorai/ltlparser.mly: AORAI_LGPL
-src/plugins/aorai/path_analysis.ml: AORAI_LGPL
-src/plugins/aorai/path_analysis.mli: AORAI_LGPL
-src/plugins/aorai/promelaast.mli: AORAI_LGPL
-src/plugins/aorai/promelalexer.mli: AORAI_LGPL
-src/plugins/aorai/promelalexer.mll: AORAI_LGPL
-src/plugins/aorai/promelalexer_withexps.mli: AORAI_LGPL
-src/plugins/aorai/promelalexer_withexps.mll: AORAI_LGPL
-src/plugins/aorai/promelaoutput.ml: AORAI_LGPL
-src/plugins/aorai/promelaoutput.mli: AORAI_LGPL
-src/plugins/aorai/promelaparser.mly: AORAI_LGPL
-src/plugins/aorai/promelaparser_withexps.mly: AORAI_LGPL
-src/plugins/aorai/utils_parser.ml: AORAI_LGPL
-src/plugins/aorai/utils_parser.mli: AORAI_LGPL
-src/plugins/aorai/yalexer.mli: AORAI_LGPL
-src/plugins/aorai/yalexer.mll: AORAI_LGPL
-src/plugins/aorai/yaparser.mly: AORAI_LGPL
-src/plugins/callgraph/Callgraph.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/callgraph_api.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/cg.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/cg.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/cg_viewer.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/cg_viewer.yes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/services.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/services.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/subgraph.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/subgraph.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/uses.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/uses.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/constant_propagation/Constant_Propagation.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/constant_propagation/propagationParameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/constant_propagation/propagationParameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/constant_propagation/api.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/constant_propagation/api.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/build.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/context.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/context.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/dive_graph.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/dive_graph.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/dive_types.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/main.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/node_range.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/node_range.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/dive/server_interface.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/From.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/callwise.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/callwise.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_compute.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_compute.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/from_register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/functionwise.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/from/functionwise.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/GSourceView2.ml.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/GSourceView2.mli.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/GSourceView3.ml.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/GSourceView3.mli.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/analyses_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/analyses_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/book_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/book_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/debug_manager.yes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/debug_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/design.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/design.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/dgraph_helper.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/dgraph_helper.no.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/dgraph_helper.yes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/file_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/file_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/filetree.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/filetree.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_compat.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_compat.2.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_compat.3.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_form.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_form.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_helper.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gtk_helper.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gui_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gui_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gui_printers.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/gui_printers.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/help_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/help_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/history.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/history.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/launcher.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/launcher.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/menu_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/menu_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/pretty_source.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/pretty_source.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/project_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/project_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/property_navigator.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/property_navigator.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/source_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/source_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/source_viewer.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/source_viewer.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/warning_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/warning_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wbox.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wbox.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wfile.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wfile.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/widget.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/widget.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wpane.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wpane.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wpalette.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wpalette.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wtable.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wtable.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wtext.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wtext.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wutil.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wutil.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wutil_once.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/wutil_once.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/Impact.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/compute_impact.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/compute_impact.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/pdg_aux.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/pdg_aux.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/reason_graph.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/reason_graph.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/impact/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/Inout.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/context.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/cumulative_analysis.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/cumulative_analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/derefs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/derefs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/inout_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/inout_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/inputs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/inputs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/operational_inputs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/operational_inputs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/outputs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/outputs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/inout/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/.gitignore: .ignore
-src/plugins/loop_analysis/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/LoopAnalysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/README.org: .ignore
-src/plugins/loop_analysis/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/loop_analysis.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/loop_analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis_sig.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/eva_info.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/eva_info.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/META.in: .ignore
-src/plugins/markdown-report/md_gen.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/md_gen.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/mdr_params.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/mdr_params.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/mdr_register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/mdr_register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/parse_remarks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/sarif.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/sarif.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/share/acsl.xml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/Metrics.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/css_html.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/css_html.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_acsl.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_acsl.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_base.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_base.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_cabs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_cabs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_cilast.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_cilast.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_coverage.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_coverage.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_pivot.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/metrics_pivot.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/metrics/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/nonterm/.gitignore: .ignore
-src/plugins/nonterm/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/nonterm/Nonterm.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/nonterm/README.md: .ignore
-src/plugins/nonterm/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/nonterm/nonterm_run.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/nonterm/nonterm_run.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/.gitignore: .ignore
-src/plugins/obfuscator/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/Obfuscator.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/dictionary.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/dictionary.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/obfuscate.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/obfuscate.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/obfuscator_kind.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/obfuscator_kind.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/obfuscator_register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/obfuscator_register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/obfuscator/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/Occurrence.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/global_context.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/global_context.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/Instantiate.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/instantiator_builder.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/instantiator_builder.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/basic_alloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/basic_alloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/calloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/calloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/free.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/free.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/mem_utils.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/mem_utils.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memcmp.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memcpy.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memcpy.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memmove.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memmove.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memset.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/string/memset.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/transform.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/transform.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/Pdg.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/annot.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/annot.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/build.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/build.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/ctrlDpds.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/ctrlDpds.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/marks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/marks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/pdg_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/pdg_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/pdg_state.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/pdg_state.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/sets.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg/sets.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg_types/pdgIndex.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg_types/pdgIndex.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg_types/pdgMarks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg_types/pdgMarks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg_types/pdgTypes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/pdg_types/pdgTypes.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/Postdominators.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/compute.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/compute.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/postdominators_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/postdominators_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/print.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/postdominators/print.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/.gitignore: .ignore
-src/plugins/print_api/Makefile: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/Print_api.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/grammar.mly: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/lexer.mll: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/lexer.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/print_interface.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/print_api/print_interface.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/qed/.gitignore: .ignore
-src/plugins/qed/Makefile: CEA_WP
-src/plugins/qed/bvars.ml: CEA_WP
-src/plugins/qed/bvars.mli: CEA_WP
-src/plugins/qed/cache.ml: CEA_WP
-src/plugins/qed/cache.mli: CEA_WP
-src/plugins/qed/collection.ml: CEA_WP
-src/plugins/qed/collection.mli: CEA_WP
-src/plugins/qed/engine.mli: CEA_WP
-src/plugins/qed/export.ml: CEA_WP
-src/plugins/qed/export.mli: CEA_WP
-src/plugins/qed/export_why3.ml: CEA_WP
-src/plugins/qed/export_why3.mli: CEA_WP
-src/plugins/qed/export_whycore.ml: CEA_WP
-src/plugins/qed/export_whycore.mli: CEA_WP
-src/plugins/qed/hcons.ml: CEA_WP
-src/plugins/qed/hcons.mli: CEA_WP
-src/plugins/qed/idxmap.ml: CEA_WP
-src/plugins/qed/idxmap.mli: CEA_WP
-src/plugins/qed/idxset.ml: CEA_WP
-src/plugins/qed/idxset.mli: CEA_WP
-src/plugins/qed/intmap.ml: CEA_WP
-src/plugins/qed/intmap.mli: CEA_WP
-src/plugins/qed/intset.ml: CEA_WP
-src/plugins/qed/intset.mli: CEA_WP
-src/plugins/qed/kind.ml: CEA_WP
-src/plugins/qed/kind.mli: CEA_WP
-src/plugins/qed/listmap.ml: CEA_WP
-src/plugins/qed/listmap.mli: CEA_WP
-src/plugins/qed/listset.ml: CEA_WP
-src/plugins/qed/listset.mli: CEA_WP
-src/plugins/qed/logic.mli: CEA_WP
-src/plugins/qed/mergemap.ml: CEA_WP
-src/plugins/qed/mergemap.mli: CEA_WP
-src/plugins/qed/mergeset.ml: CEA_WP
-src/plugins/qed/mergeset.mli: CEA_WP
-src/plugins/qed/partition.ml: CEA_WP
-src/plugins/qed/partition.mli: CEA_WP
-src/plugins/qed/plib.ml: CEA_WP
-src/plugins/qed/plib.mli: CEA_WP
-src/plugins/qed/pool.ml: CEA_WP
-src/plugins/qed/pool.mli: CEA_WP
-src/plugins/qed/pretty.ml: CEA_WP
-src/plugins/qed/pretty.mli: CEA_WP
-src/plugins/qed/term.ml: CEA_WP
-src/plugins/qed/term.mli: CEA_WP
-src/plugins/reduc/Reduc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/collect.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/collect.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/hyp.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/hyp.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/misc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/misc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/reduc_options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/reduc_options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/value2acsl.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/reduc/value2acsl.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/.gitignore: .ignore
-src/plugins/report/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/Report.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/classify.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/classify.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/csv.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/csv.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/dump.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/dump.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/report_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/report_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/scan.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/scan.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/RteGen.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/flags.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/flags.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/generator.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/generator.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/rte.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/rte.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/visit.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/rte/visit.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/.gitignore: .ignore
-src/plugins/server/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/Server.mli: .ignore
-src/plugins/server/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/data.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/data.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/jbuffer.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/jbuffer.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_ast.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_ast.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_main.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_main.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_project.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_project.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_properties.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/kernel_properties.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/main.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/main.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/package.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/package.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/request.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/request.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_doc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_doc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_batch.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_batch.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_socket.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_socket.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_zmq.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/server_zmq.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/states.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/server/states.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/Scope.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/datascope.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/datascope.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/defs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/defs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/dpds_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/dpds_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/zones.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/scope/zones.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/.gitignore: .ignore
-src/plugins/security_slicing/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/Security_slicing.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/components.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/components.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/security_slicing_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/security_slicing/security_slicing_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/Slicing.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/api.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/api.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/fct_slice.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/fct_slice.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/printSlice.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/printSlice.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingActions.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingActions.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingCmds.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingCmds.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingInternals.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingInternals.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingMacros.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingMacros.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingMarks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingMarks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingParameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingParameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingProject.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingProject.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingSelect.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingSelect.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingState.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingState.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingTransform.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingTransform.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingTypes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/slicing/slicingTypes.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/Sparecode.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/globs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/globs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/spare_marks.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/spare_marks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/sparecode_params.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/sparecode_params.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/transform.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/sparecode/transform.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/reads.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/reads.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/studia_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/studia_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/studia_request.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/studia_request.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/Studia.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/writes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/studia/writes.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/users/Users.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/users/users_register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/users/users_register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/.merlin: .ignore
-src/plugins/value/Changelog_non_free: .ignore
-src/plugins/value/Eva.mli: .ignore
-src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/eval.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/eval.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gen-api.sh: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/self.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/self.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/test.assert.sh: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/test.sh: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/api/values_request.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/simpler_domains.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/apron/apron_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/apron/apron_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_float.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_float.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_malloc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_malloc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_misc.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_misc.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_memory.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_memory.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_print_c.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_print_c.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_watchpoint.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_watchpoint.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_split.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_split.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_string.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/builtins_string.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_init.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_init.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_offsetmap.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_offsetmap.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_specification.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_specification.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_transfer.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/cvalue_transfer.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/locals_scoping.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/locals_scoping.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/warn.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/cvalue/warn.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_mode.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_mode.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_builder.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_builder.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_lift.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_lift.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_product.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_product.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_store.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/domain_store.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/equality/equality.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/equality/equality.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/equality/equality_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/equality/equality_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/gauges/gauges_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/gauges/gauges_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/traces_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/traces_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/hcexprs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/hcexprs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/inout_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/inout_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/abstract_memory.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/abstract_memory.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/abstract_offset.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/abstract_offset.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/abstract_structure.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/abstract_structure.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/multidim.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/multidim.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/multidim_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/multidim_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/pretty_memory.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/pretty_memory.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/segmentation.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/segmentation.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/typed_memory.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim/typed_memory.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/octagons.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/octagons.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/offsm_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/offsm_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/powerset.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/powerset.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/sign_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/sign_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/numerors/numerors_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/numerors/numerors_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/simple_memory.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/simple_memory.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/symbolic_locs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/symbolic_locs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/taint_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/taint_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/unit_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/unit_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/abstractions.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/abstractions.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/analysis.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/compute_functions.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/compute_functions.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/evaluation.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/evaluation.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/function_calls.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/function_calls.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/initialization.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/initialization.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/iterator.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/iterator.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/mem_exec.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/mem_exec.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/recursion.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/recursion.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/subdivided_evaluation.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/subdivided_evaluation.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/transfer_logic.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/transfer_logic.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/transfer_specification.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/transfer_specification.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/transfer_stmt.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/transfer_stmt.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_callstacks_filters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_callstacks_filters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_callstacks_manager.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_callstacks_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_eval.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_eval.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_types.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_types.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_red.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/gui_red.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gui_files/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/eval_annots.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/eval_annots.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/eval_op.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/eval_op.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/eval_terms.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/eval_terms.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/function_args.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/legacy/function_args.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/auto_loop_unroll.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/auto_loop_unroll.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/partition.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/partition.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/partitioning_index.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/partitioning_index.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/partitioning_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/partitioning_parameters.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/per_stmt_slevel.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/per_stmt_slevel.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/split_return.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/split_return.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/split_strategy.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/split_strategy.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/trace_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/partitioning/trace_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/abstract.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/abstract.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/active_behaviors.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/active_behaviors.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/backward_formals.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/backward_formals.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_audit.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_dynamic.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_dynamic.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_perf.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_perf.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_results.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_results.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_utils.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_utils.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eval_typ.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eval_typ.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/red_statuses.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/red_statuses.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/library_functions.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/results.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/results.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/summary.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/summary.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/unit_tests.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/widen.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/widen.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/widen_hints_ext.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/widen_hints_ext.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/abstract_location.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/abstract_value.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/cvalue_backward.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/cvalue_backward.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/cvalue_forward.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/cvalue_forward.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/location_lift.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/location_lift.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/main_locations.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/main_locations.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/main_values.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/main_values.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/offsm_value.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/offsm_value.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/sign_value.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/sign_value.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_utils.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_utils.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_float.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_float.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_interval.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_interval.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_arithmetics.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_arithmetics.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_value.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/numerors/numerors_value.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/value_product.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/value_product.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/README.md: .ignore
-src/plugins/value_types/cilE.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/cilE.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/cvalue.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/cvalue.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/function_Froms.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/function_Froms.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/inout_type.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/inout_type.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/precise_locs.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/precise_locs.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/value_types.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/value_types.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/widen_type.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value_types/widen_type.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/Makefile.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/configure.ac: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/Variadic.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/classify.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/classify.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/environment.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/environment.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/extends.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/extends.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_parser.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_parser.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_pprint.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_pprint.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_string.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_string.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_typer.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_typer.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/format_types.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/generic.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/generic.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/options.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/options.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/replacements.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/replacements.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/standard.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/standard.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/translate.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/translate.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/va_types.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/wp/.gitignore: .ignore
-src/plugins/wp/AssignsCompleteness.ml: CEA_WP
-src/plugins/wp/AssignsCompleteness.mli: CEA_WP
-src/plugins/wp/Auto.ml: CEA_WP
-src/plugins/wp/Auto.mli: CEA_WP
-src/plugins/wp/Cache.ml: CEA_WP
-src/plugins/wp/Cache.mli: CEA_WP
-src/plugins/wp/Cfloat.ml: CEA_WP
-src/plugins/wp/Cfloat.mli: CEA_WP
-src/plugins/wp/Changelog: .ignore
-src/plugins/wp/Cint.ml: CEA_WP
-src/plugins/wp/Cint.mli: CEA_WP
-src/plugins/wp/Cleaning.ml: CEA_WP
-src/plugins/wp/Cleaning.mli: CEA_WP
-src/plugins/wp/Cmath.ml: CEA_WP
-src/plugins/wp/Cmath.mli: CEA_WP
-src/plugins/wp/CodeSemantics.ml: CEA_WP
-src/plugins/wp/CodeSemantics.mli: CEA_WP
-src/plugins/wp/Conditions.ml: CEA_WP
-src/plugins/wp/Conditions.mli: CEA_WP
-src/plugins/wp/Context.ml: CEA_WP
-src/plugins/wp/Context.mli: CEA_WP
-src/plugins/wp/Cstring.ml: CEA_WP
-src/plugins/wp/Cstring.mli: CEA_WP
-src/plugins/wp/Cvalues.ml: CEA_WP
-src/plugins/wp/Cvalues.mli: CEA_WP
-src/plugins/wp/Definitions.ml: CEA_WP
-src/plugins/wp/Definitions.mli: CEA_WP
-src/plugins/wp/Factory.ml: CEA_WP
-src/plugins/wp/Factory.mli: CEA_WP
-src/plugins/wp/Filtering.ml: CEA_WP
-src/plugins/wp/Filtering.mli: CEA_WP
-src/plugins/wp/Footprint.ml: CEA_WP
-src/plugins/wp/Footprint.mli: CEA_WP
-src/plugins/wp/Generator.ml: CEA_WP
-src/plugins/wp/Generator.mli: CEA_WP
-src/plugins/wp/GuiConfig.ml: CEA_WP
-src/plugins/wp/GuiConfig.mli: CEA_WP
-src/plugins/wp/GuiComposer.ml: CEA_WP
-src/plugins/wp/GuiComposer.mli: CEA_WP
-src/plugins/wp/GuiGoal.ml: CEA_WP
-src/plugins/wp/GuiGoal.mli: CEA_WP
-src/plugins/wp/GuiList.ml: CEA_WP
-src/plugins/wp/GuiList.mli: CEA_WP
-src/plugins/wp/GuiNavigator.ml: CEA_WP
-src/plugins/wp/GuiNavigator.mli: CEA_WP
-src/plugins/wp/GuiPanel.ml: CEA_WP
-src/plugins/wp/GuiPanel.mli: CEA_WP
-src/plugins/wp/GuiProver.ml: CEA_WP
-src/plugins/wp/GuiProver.mli: CEA_WP
-src/plugins/wp/GuiProof.ml: CEA_WP
-src/plugins/wp/GuiProof.mli: CEA_WP
-src/plugins/wp/GuiSequent.ml: CEA_WP
-src/plugins/wp/GuiSequent.mli: CEA_WP
-src/plugins/wp/GuiSource.ml: CEA_WP
-src/plugins/wp/GuiSource.mli: CEA_WP
-src/plugins/wp/GuiTactic.ml: CEA_WP
-src/plugins/wp/GuiTactic.mli: CEA_WP
-src/plugins/wp/Layout.ml: CEA_WP
-src/plugins/wp/Layout.mli: CEA_WP
-src/plugins/wp/Lang.ml: CEA_WP
-src/plugins/wp/Lang.mli: CEA_WP
-src/plugins/wp/Letify.ml: CEA_WP
-src/plugins/wp/Letify.mli: CEA_WP
-src/plugins/wp/LogicAssigns.ml: CEA_WP
-src/plugins/wp/LogicAssigns.mli: CEA_WP
-src/plugins/wp/LogicBuiltins.ml: CEA_WP
-src/plugins/wp/LogicBuiltins.mli: CEA_WP
-src/plugins/wp/LogicCompiler.ml: CEA_WP
-src/plugins/wp/LogicCompiler.mli: CEA_WP
-src/plugins/wp/LogicSemantics.ml: CEA_WP
-src/plugins/wp/LogicSemantics.mli: CEA_WP
-src/plugins/wp/LogicUsage.ml: CEA_WP
-src/plugins/wp/LogicUsage.mli: CEA_WP
-src/plugins/wp/Makefile.in: CEA_WP
-src/plugins/wp/Matrix.ml: CEA_WP
-src/plugins/wp/Matrix.mli: CEA_WP
-src/plugins/wp/MemoryContext.ml: CEA_WP
-src/plugins/wp/MemoryContext.mli: CEA_WP
-src/plugins/wp/MemDebug.ml: CEA_WP
-src/plugins/wp/MemDebug.mli: CEA_WP
-src/plugins/wp/MemEmpty.ml: CEA_WP
-src/plugins/wp/MemEmpty.mli: CEA_WP
-src/plugins/wp/MemLoader.ml: CEA_WP
-src/plugins/wp/MemLoader.mli: CEA_WP
-src/plugins/wp/MemMemory.ml: CEA_WP
-src/plugins/wp/MemMemory.mli: CEA_WP
-src/plugins/wp/MemRegion.ml: CEA_WP
-src/plugins/wp/MemRegion.mli: CEA_WP
-src/plugins/wp/MemTyped.ml: CEA_WP
-src/plugins/wp/MemTyped.mli: CEA_WP
-src/plugins/wp/MemVal.ml: CEA_WP
-src/plugins/wp/MemVal.mli: CEA_WP
-src/plugins/wp/MemVar.ml: CEA_WP
-src/plugins/wp/MemVar.mli: CEA_WP
-src/plugins/wp/MemZeroAlias.ml: CEA_WP
-src/plugins/wp/MemZeroAlias.mli: CEA_WP
-src/plugins/wp/Sigs.mli: CEA_WP
-src/plugins/wp/Mstate.ml: CEA_WP
-src/plugins/wp/Mstate.mli: CEA_WP
-src/plugins/wp/Passive.ml: CEA_WP
-src/plugins/wp/Passive.mli: CEA_WP
-src/plugins/wp/Pcfg.ml: CEA_WP
-src/plugins/wp/Pcfg.mli: CEA_WP
-src/plugins/wp/Pcond.ml: CEA_WP
-src/plugins/wp/Pcond.mli: CEA_WP
-src/plugins/wp/Plang.ml: CEA_WP
-src/plugins/wp/Plang.mli: CEA_WP
-src/plugins/wp/ProofEngine.ml: CEA_WP
-src/plugins/wp/ProofEngine.mli: CEA_WP
-src/plugins/wp/ProofSession.ml: CEA_WP
-src/plugins/wp/ProofSession.mli: CEA_WP
-src/plugins/wp/ProofScript.ml: CEA_WP
-src/plugins/wp/ProofScript.mli: CEA_WP
-src/plugins/wp/ProverScript.ml: CEA_WP
-src/plugins/wp/ProverScript.mli: CEA_WP
-src/plugins/wp/ProverSearch.ml: CEA_WP
-src/plugins/wp/ProverSearch.mli: CEA_WP
-src/plugins/wp/ProverTask.ml: CEA_WP
-src/plugins/wp/ProverTask.mli: CEA_WP
-src/plugins/wp/ProverWhy3.mli: CEA_WP
-src/plugins/wp/ProverWhy3.ml: CEA_WP
-src/plugins/wp/RefUsage.ml: CEA_WP
-src/plugins/wp/RefUsage.mli: CEA_WP
-src/plugins/wp/Region.ml: CEA_WP
-src/plugins/wp/Region.mli: CEA_WP
-src/plugins/wp/RegionAccess.ml: CEA_WP
-src/plugins/wp/RegionAccess.mli: CEA_WP
-src/plugins/wp/RegionAnalysis.ml: CEA_WP
-src/plugins/wp/RegionAnalysis.mli: CEA_WP
-src/plugins/wp/RegionAnnot.ml: CEA_WP
-src/plugins/wp/RegionAnnot.mli: CEA_WP
-src/plugins/wp/RegionDump.ml: CEA_WP
-src/plugins/wp/RegionDump.mli: CEA_WP
-src/plugins/wp/Repr.ml: CEA_WP
-src/plugins/wp/Repr.mli: CEA_WP
-src/plugins/wp/Sigma.ml: CEA_WP
-src/plugins/wp/Sigma.mli: CEA_WP
-src/plugins/wp/Splitter.ml: CEA_WP
-src/plugins/wp/Splitter.mli: CEA_WP
-src/plugins/wp/CfgCompiler.ml: CEA_WP
-src/plugins/wp/CfgCompiler.mli: CEA_WP
-src/plugins/wp/StmtSemantics.ml: CEA_WP
-src/plugins/wp/StmtSemantics.mli: CEA_WP
-src/plugins/wp/Strategy.ml: CEA_WP
-src/plugins/wp/Strategy.mli: CEA_WP
-src/plugins/wp/Tactical.ml: CEA_WP
-src/plugins/wp/Tactical.mli: CEA_WP
-src/plugins/wp/TacArray.ml: CEA_WP
-src/plugins/wp/TacArray.mli: CEA_WP
-src/plugins/wp/TacBitwised.ml: CEA_WP
-src/plugins/wp/TacBitwised.mli: CEA_WP
-src/plugins/wp/TacBitrange.ml: CEA_WP
-src/plugins/wp/TacBitrange.mli: CEA_WP
-src/plugins/wp/TacBittest.ml: CEA_WP
-src/plugins/wp/TacBittest.mli: CEA_WP
-src/plugins/wp/TacChoice.ml: CEA_WP
-src/plugins/wp/TacChoice.mli: CEA_WP
-src/plugins/wp/TacClear.ml: CEA_WP
-src/plugins/wp/TacClear.mli: CEA_WP
-src/plugins/wp/TacCongruence.ml: CEA_WP
-src/plugins/wp/TacCongruence.mli: CEA_WP
-src/plugins/wp/TacCompound.ml: CEA_WP
-src/plugins/wp/TacCompound.mli: CEA_WP
-src/plugins/wp/TacCut.ml: CEA_WP
-src/plugins/wp/TacCut.mli: CEA_WP
-src/plugins/wp/TacFilter.ml: CEA_WP
-src/plugins/wp/TacFilter.mli: CEA_WP
-src/plugins/wp/TacHavoc.ml: CEA_WP
-src/plugins/wp/TacHavoc.mli: CEA_WP
-src/plugins/wp/TacInduction.ml: CEA_WP
-src/plugins/wp/TacInduction.mli: CEA_WP
-src/plugins/wp/TacInstance.ml: CEA_WP
-src/plugins/wp/TacInstance.mli: CEA_WP
-src/plugins/wp/TacLemma.ml: CEA_WP
-src/plugins/wp/TacLemma.mli: CEA_WP
-src/plugins/wp/TacModMask.ml: CEA_WP
-src/plugins/wp/TacModMask.mli: CEA_WP
-src/plugins/wp/TacNormalForm.ml: CEA_WP
-src/plugins/wp/TacNormalForm.mli: CEA_WP
-src/plugins/wp/TacOverflow.ml: CEA_WP
-src/plugins/wp/TacOverflow.mli: CEA_WP
-src/plugins/wp/TacRange.ml: CEA_WP
-src/plugins/wp/TacRange.mli: CEA_WP
-src/plugins/wp/TacRewrite.ml: CEA_WP
-src/plugins/wp/TacRewrite.mli: CEA_WP
-src/plugins/wp/TacSequence.ml: CEA_WP
-src/plugins/wp/TacSequence.mli: CEA_WP
-src/plugins/wp/TacShift.ml: CEA_WP
-src/plugins/wp/TacShift.mli: CEA_WP
-src/plugins/wp/TacSplit.ml: CEA_WP
-src/plugins/wp/TacSplit.mli: CEA_WP
-src/plugins/wp/TacUnfold.ml: CEA_WP
-src/plugins/wp/TacUnfold.mli: CEA_WP
-src/plugins/wp/VC.ml: CEA_WP
-src/plugins/wp/VC.mli: CEA_WP
-src/plugins/wp/VCS.ml: CEA_WP
-src/plugins/wp/VCS.mli: CEA_WP
-src/plugins/wp/Vlist.ml: CEA_WP
-src/plugins/wp/Vlist.mli: CEA_WP
-src/plugins/wp/Vset.ml: CEA_WP
-src/plugins/wp/Vset.mli: CEA_WP
-src/plugins/wp/Warning.ml: CEA_WP
-src/plugins/wp/Warning.mli: CEA_WP
-src/plugins/wp/Why3Provers.ml: CEA_WP
-src/plugins/wp/Why3Provers.mli: CEA_WP
-src/plugins/wp/Wp.mli: .ignore
-src/plugins/wp/WpTac.ml: CEA_WP
-src/plugins/wp/WpTac.mli: CEA_WP
-src/plugins/wp/cfgAnnot.ml: CEA_WP
-src/plugins/wp/cfgAnnot.mli: CEA_WP
-src/plugins/wp/cfgInfos.ml: CEA_WP
-src/plugins/wp/cfgInfos.mli: CEA_WP
-src/plugins/wp/cfgCalculus.ml: CEA_WP
-src/plugins/wp/cfgCalculus.mli: CEA_WP
-src/plugins/wp/cfgDump.ml: CEA_WP
-src/plugins/wp/cfgDump.mli: CEA_WP
-src/plugins/wp/cfgGenerator.ml: CEA_WP
-src/plugins/wp/cfgGenerator.mli: CEA_WP
-src/plugins/wp/cfgInit.ml: CEA_WP
-src/plugins/wp/cfgInit.mli: CEA_WP
-src/plugins/wp/cfgWP.ml: CEA_WP
-src/plugins/wp/cfgWP.mli: CEA_WP
-src/plugins/wp/clabels.ml: CEA_WP
-src/plugins/wp/clabels.mli: CEA_WP
-src/plugins/wp/configure.ac: CEA_WP
-src/plugins/wp/ctypes.ml: CEA_WP
-src/plugins/wp/ctypes.mli: CEA_WP
-src/plugins/wp/filter_axioms.ml: CEA_WP
-src/plugins/wp/filter_axioms.mli: CEA_WP
-src/plugins/wp/doc/MakeDoc: CEA_WP
-src/plugins/wp/doc/coqdoc/Makefile: CEA_WP
-src/plugins/wp/doc/coqdoc/coqdoc.sty: .ignore
-src/plugins/wp/doc/coqdoc/qed_generated.tex: .ignore
-src/plugins/wp/doc/coqdoc/typed_generated.tex: .ignore
-src/plugins/wp/doc/coqdoc/wpcoq.tex: .ignore
-src/plugins/wp/doc/manual/.gitignore: .ignore
-src/plugins/wp/doc/manual/Makefile: CEA_WP
-src/plugins/wp/doc/manual/mem.pdf: .ignore
-src/plugins/wp/doc/manual/size_base.pdf: .ignore
-src/plugins/wp/doc/manual/size_compl.pdf: .ignore
-src/plugins/wp/doc/manual/wp-complete.png: .ignore
-src/plugins/wp/doc/manual/wp-gui-main.png: .ignore
-src/plugins/wp/doc/manual/wp-gui-run.png: .ignore
-src/plugins/wp/doc/manual/wp-invalid.png: .ignore
-src/plugins/wp/doc/manual/wp-unknown.png: .ignore
-src/plugins/wp/doc/manual/wp-valid.png: .ignore
-src/plugins/wp/doc/manual/wp.bib: .ignore
-src/plugins/wp/doc/manual/wp.tex: .ignore
-src/plugins/wp/doc/manual/wp_acsl.tex: .ignore
-src/plugins/wp/doc/manual/wp_calculus.tex: .ignore
-src/plugins/wp/doc/manual/wp_caveat.tex: .ignore
-src/plugins/wp/doc/manual/wp_hoare.tex: .ignore
-src/plugins/wp/doc/manual/wp_implementation.tex: .ignore
-src/plugins/wp/doc/manual/wp_intro.tex: .ignore
-src/plugins/wp/doc/manual/wp_logic.tex: .ignore
-src/plugins/wp/doc/manual/wp_logicvar.tex: .ignore
-src/plugins/wp/doc/manual/wp_models.tex: .ignore
-src/plugins/wp/doc/manual/wp_plugin.tex: .ignore
-src/plugins/wp/doc/manual/wp_runtime.tex: .ignore
-src/plugins/wp/doc/manual/wp_simplifier.tex: .ignore
-src/plugins/wp/doc/manual/wp_store.tex: .ignore
-src/plugins/wp/doc/manual/wp_typed.tex: .ignore
-src/plugins/wp/driver.mli: CEA_WP
-src/plugins/wp/driver.mll: CEA_WP
-src/plugins/wp/dyncall.ml: CEA_WP
-src/plugins/wp/dyncall.mli: CEA_WP
-src/plugins/wp/intro_wp.txt: CEA_WP
-src/plugins/wp/mcfg.mli: CEA_WP
-src/plugins/wp/normAtLabels.ml: CEA_WP
-src/plugins/wp/normAtLabels.mli: CEA_WP
-src/plugins/wp/prover.ml: CEA_WP
-src/plugins/wp/prover.mli: CEA_WP
-src/plugins/wp/register.ml: CEA_WP
-src/plugins/wp/register.mli: CEA_WP
-src/plugins/wp/rformat.mli: CEA_WP
-src/plugins/wp/rformat.mll: CEA_WP
-src/plugins/wp/script.mli: CEA_WP
-src/plugins/wp/script.mll: CEA_WP
-src/plugins/wp/share/.gitignore: .ignore
-src/plugins/wp/share/Makefile.resources: CEA_WP
-src/plugins/wp/share/coqwp/ArcTrigo.v: CEA_WP
-src/plugins/wp/share/coqwp/Bits.v: CEA_WP
-src/plugins/wp/share/coqwp/BuiltIn.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/Cbits.v: CEA_WP
-src/plugins/wp/share/coqwp/Cfloat.v: CEA_WP
-src/plugins/wp/share/coqwp/Cint.v: CEA_WP
-src/plugins/wp/share/coqwp/Cmath.v: CEA_WP
-src/plugins/wp/share/coqwp/ExpLog.v: CEA_WP
-src/plugins/wp/share/coqwp/HighOrd.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/Memory.v: CEA_WP
-src/plugins/wp/share/coqwp/Qed.v: CEA_WP
-src/plugins/wp/share/coqwp/Qedlib.v: CEA_WP
-src/plugins/wp/share/coqwp/Square.v: CEA_WP
-src/plugins/wp/share/coqwp/Vlist.v: CEA_WP
-src/plugins/wp/share/coqwp/Vset.v: CEA_WP
-src/plugins/wp/share/coqwp/Zbits.v: CEA_WP
-src/plugins/wp/share/coqwp/bool/Bool.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/Abs.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/ComputerDivision.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/EuclideanDivision.v: MODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/Exponentiation.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/Int.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/MinMax.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/Power.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v: MODIFIED_WHY3
-src/plugins/wp/share/coqwp/map/Map.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/map/Const.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/Abs.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/FromInt.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/ExpLog.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/MinMax.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/PowerReal.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/Real.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/RealInfix.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/Square.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/real/Trigonometry.v: UNMODIFIED_WHY3
-src/plugins/wp/share/install.ml: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/cbits.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/cint.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/cmath.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/memory.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/qed.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/vlist.mlw: CEA_WP
-src/plugins/wp/share/why3/frama_c_wp/vset.mlw: CEA_WP
-src/plugins/wp/share/wp.driver: CEA_WP
-src/plugins/wp/wpContext.ml: CEA_WP
-src/plugins/wp/wpContext.mli: CEA_WP
-src/plugins/wp/wpPropId.ml: CEA_WP
-src/plugins/wp/wpPropId.mli: CEA_WP
-src/plugins/wp/wpReached.ml: CEA_WP
-src/plugins/wp/wpReached.mli: CEA_WP
-src/plugins/wp/wpReport.ml: CEA_WP
-src/plugins/wp/wpReport.mli: CEA_WP
-src/plugins/wp/wpRTE.ml: CEA_WP
-src/plugins/wp/wpRTE.mli: CEA_WP
-src/plugins/wp/wpTarget.ml: CEA_WP
-src/plugins/wp/wpTarget.mli: CEA_WP
-src/plugins/wp/wp_error.ml: CEA_WP
-src/plugins/wp/wp_error.mli: CEA_WP
-src/plugins/wp/wp_parameters.ml: CEA_WP
-src/plugins/wp/wp_parameters.mli: CEA_WP
-src/plugins/wp/wpo.ml: CEA_WP
-src/plugins/wp/wpo.mli: CEA_WP
-src/plugins/wp/wprop.ml: CEA_WP
-src/plugins/wp/wprop.mli: CEA_WP
diff --git a/ivette/headers/header_spec.txt b/ivette/headers/header_spec.txt
deleted file mode 100644
index 649ed47c9564883ad2bfdc95277c9831e3a661f3..0000000000000000000000000000000000000000
--- a/ivette/headers/header_spec.txt
+++ /dev/null
@@ -1,214 +0,0 @@
-.babelrc: .ignore
-.dome-pkg-app.lock: .ignore
-.dome-pkg-dev.lock: .ignore
-.eslintignore: .ignore
-.eslintrc.js: .ignore
-.gitignore: .ignore
-CONTRIBUTING.md: .ignore
-INSTALL.md: .ignore
-Makefile: CEA_LGPL
-README.md: .ignore
-configure.js: .ignore
-distrib.sh: CEA_LGPL
-doc/pandoc/href.lua: .ignore
-doc/pandoc/index.json: .ignore
-doc/pandoc/template.html: .ignore
-electron-builder.json: .ignore
-electron-webpack.json: .ignore
-ivette-macos.sh: CEA_LGPL
-package.json: .ignore
-sandboxer.js: .ignore
-src/dome/.gitignore: .ignore
-src/dome/CONTRIBUTING.md: .ignore
-src/dome/CONTRIBUTORS.md: .ignore
-src/dome/LICENSE.md: .ignore
-src/dome/README.md: .ignore
-src/dome/doc/README.md: .ignore
-src/dome/doc/config.json: .ignore
-src/dome/doc/gallery.css: .ignore
-src/dome/doc/guides/application.md: .ignore
-src/dome/doc/guides/development.md: .ignore
-src/dome/doc/guides/dome.md: .ignore
-src/dome/doc/guides/glossary.md: .ignore
-src/dome/doc/guides/hooks.md: .ignore
-src/dome/doc/guides/hotreload.md: .ignore
-src/dome/doc/guides/quickstart.md: .ignore
-src/dome/doc/guides/styling.md: .ignore
-src/dome/doc/icons.js: .ignore
-src/dome/doc/iconsmd.js: .ignore
-src/dome/doc/template/gallery-head.html: .ignore
-src/dome/doc/template/gallery-tail.html: .ignore
-src/dome/doc/template/publish.js: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Bold-webfont.eot: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Bold-webfont.svg: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Bold-webfont.woff: .ignore
-src/dome/doc/template/static/fonts/OpenSans-BoldItalic-webfont.eot: .ignore
-src/dome/doc/template/static/fonts/OpenSans-BoldItalic-webfont.svg: .ignore
-src/dome/doc/template/static/fonts/OpenSans-BoldItalic-webfont.woff: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Italic-webfont.eot: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Italic-webfont.svg: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Italic-webfont.woff: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Light-webfont.eot: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Light-webfont.svg: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Light-webfont.woff: .ignore
-src/dome/doc/template/static/fonts/OpenSans-LightItalic-webfont.eot: .ignore
-src/dome/doc/template/static/fonts/OpenSans-LightItalic-webfont.svg: .ignore
-src/dome/doc/template/static/fonts/OpenSans-LightItalic-webfont.woff: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Regular-webfont.eot: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Regular-webfont.svg: .ignore
-src/dome/doc/template/static/fonts/OpenSans-Regular-webfont.woff: .ignore
-src/dome/doc/template/static/scripts/linenumber.js: .ignore
-src/dome/doc/template/static/scripts/prettify/Apache-License-2.0.txt: .ignore
-src/dome/doc/template/static/scripts/prettify/lang-css.js: .ignore
-src/dome/doc/template/static/scripts/prettify/prettify.js: .ignore
-src/dome/doc/template/static/styles/jsdoc-default.css: .ignore
-src/dome/doc/template/static/styles/prettify-jsdoc.css: .ignore
-src/dome/doc/template/static/styles/prettify-tomorrow.css: .ignore
-src/dome/doc/template/tmpl/augments.tmpl: .ignore
-src/dome/doc/template/tmpl/container.tmpl: .ignore
-src/dome/doc/template/tmpl/details.tmpl: .ignore
-src/dome/doc/template/tmpl/example.tmpl: .ignore
-src/dome/doc/template/tmpl/examples.tmpl: .ignore
-src/dome/doc/template/tmpl/exceptions.tmpl: .ignore
-src/dome/doc/template/tmpl/layout.tmpl: .ignore
-src/dome/doc/template/tmpl/mainpage.tmpl: .ignore
-src/dome/doc/template/tmpl/members.tmpl: .ignore
-src/dome/doc/template/tmpl/method.tmpl: .ignore
-src/dome/doc/template/tmpl/params.tmpl: .ignore
-src/dome/doc/template/tmpl/properties.tmpl: .ignore
-src/dome/doc/template/tmpl/returns.tmpl: .ignore
-src/dome/doc/template/tmpl/source.tmpl: .ignore
-src/dome/doc/template/tmpl/tutorial.tmpl: .ignore
-src/dome/doc/template/tmpl/type.tmpl: .ignore
-src/dome/examples/Makefile: CEA_LGPL
-src/dome/examples/README.md: .ignore
-src/dome/main/dome.ts: CEA_LGPL
-src/dome/main/menubar.ts: CEA_LGPL
-src/dome/misc/devtools.js: CEA_LGPL
-src/dome/misc/register.js: CEA_LGPL
-src/dome/misc/system.ts: CEA_LGPL
-src/dome/misc/utils.ts: CEA_LGPL
-src/dome/renderer/controls/buttons.tsx: CEA_LGPL
-src/dome/renderer/controls/displays.tsx: CEA_LGPL
-src/dome/renderer/controls/gallery.json: .ignore
-src/dome/renderer/controls/icons.tsx: CEA_LGPL
-src/dome/renderer/controls/labels.tsx: CEA_LGPL
-src/dome/renderer/controls/style.css: .ignore
-src/dome/renderer/dark.css: .ignore
-src/dome/renderer/data/compare.ts: CEA_LGPL
-src/dome/renderer/data/json.ts: CEA_LGPL
-src/dome/renderer/data/library.js: CEA_LGPL
-src/dome/renderer/data/settings.ts: CEA_LGPL
-src/dome/renderer/data/states.ts: CEA_LGPL
-src/dome/renderer/dialogs.tsx: CEA_LGPL
-src/dome/renderer/dnd.js: CEA_LGPL
-src/dome/renderer/dome.tsx: CEA_LGPL
-src/dome/renderer/errors.tsx: CEA_LGPL
-src/dome/renderer/frame/sidebars.tsx: CEA_LGPL
-src/dome/renderer/frame/style.css: .ignore
-src/dome/renderer/frame/tabs.tsx: CEA_LGPL
-src/dome/renderer/frame/toolbars.tsx: CEA_LGPL
-src/dome/renderer/layout/boxes.tsx: CEA_LGPL
-src/dome/renderer/layout/dispatch.tsx: CEA_LGPL
-src/dome/renderer/layout/forms.tsx: CEA_LGPL
-src/dome/renderer/layout/grids.js: CEA_LGPL
-src/dome/renderer/layout/qsplit.tsx: CEA_LGPL
-src/dome/renderer/layout/splitters.tsx: CEA_LGPL
-src/dome/renderer/layout/style.css: .ignore
-src/dome/renderer/light.css: .ignore
-src/dome/renderer/style.css: .ignore
-src/dome/renderer/table/arrays.ts: CEA_LGPL
-src/dome/renderer/table/models.ts: CEA_LGPL
-src/dome/renderer/table/style.css: .ignore
-src/dome/renderer/table/views.tsx: CEA_LGPL
-src/dome/renderer/text/buffers.ts: CEA_LGPL
-src/dome/renderer/text/dark-code.css: .ignore
-src/dome/renderer/text/editors.tsx: CEA_LGPL
-src/dome/renderer/text/pages.tsx: CEA_LGPL
-src/dome/renderer/text/style.css: .ignore
-src/dome/renderer/themes.tsx: CEA_LGPL
-src/dome/template/Application.js: CEA_LGPL
-src/dome/template/Preferences.js: CEA_LGPL
-src/dome/template/babelrc.json: .ignore
-src/dome/template/dome-pull.sh: CEA_LGPL
-src/dome/template/dome-push.sh: CEA_LGPL
-src/dome/template/electron-webpack.json: .ignore
-src/dome/template/export.sh: CEA_LGPL
-src/dome/template/git-ignore: .ignore
-src/dome/template/main.js: CEA_LGPL
-src/dome/template/makefile: CEA_LGPL
-src/dome/template/makefile.app.packages: CEA_LGPL
-src/dome/template/makefile.packages: CEA_LGPL
-src/dome/template/package.sh: CEA_LGPL
-src/dome/template/renderer.js: CEA_LGPL
-src/dome/template/typescript.el: .ignore
-src/dome/template/update.sh: CEA_LGPL
-src/dome/template/webpack.main.js: CEA_LGPL
-src/dome/template/webpack.renderer.js: CEA_LGPL
-src/frama-c/api_generator.ml: CEA_LGPL
-src/frama-c/client.ts: CEA_LGPL
-src/frama-c/client_socket.ts: CEA_LGPL
-src/frama-c/client_zmq.ts: CEA_LGPL
-src/frama-c/index.tsx: CEA_LGPL
-src/frama-c/kernel/ASTinfo.tsx: CEA_LGPL
-src/frama-c/kernel/ASTview.tsx: CEA_LGPL
-src/frama-c/kernel/Globals.tsx: CEA_LGPL
-src/frama-c/kernel/History.tsx: CEA_LGPL
-src/frama-c/kernel/Locations.tsx: CEA_LGPL
-src/frama-c/kernel/Messages.tsx: CEA_LGPL
-src/frama-c/kernel/PivotTable-style.css: .ignore
-src/frama-c/kernel/PivotTable.tsx: CEA_LGPL
-src/frama-c/kernel/Properties.tsx: CEA_LGPL
-src/frama-c/kernel/SourceCode.tsx: CEA_LGPL
-src/frama-c/kernel/Status.tsx: CEA_LGPL
-src/frama-c/kernel/api/ast/index.ts: CEA_LGPL
-src/frama-c/kernel/api/data/index.ts: CEA_LGPL
-src/frama-c/kernel/api/project/index.ts: CEA_LGPL
-src/frama-c/kernel/api/properties/index.ts: CEA_LGPL
-src/frama-c/kernel/api/services/index.ts: CEA_LGPL
-src/frama-c/kernel/style.css: .ignore
-src/frama-c/menu.ts: CEA_LGPL
-src/frama-c/pkg.json: .ignore
-src/frama-c/plugins/dive/api/index.ts: CEA_LGPL
-src/frama-c/plugins/dive/cytoscape_libs.js: CEA_LGPL
-src/frama-c/plugins/dive/index.tsx: CEA_LGPL
-src/frama-c/plugins/dive/layouts.json: .ignore
-src/frama-c/plugins/dive/pkg.json: .ignore
-src/frama-c/plugins/dive/react-cytoscapejs.d.ts: CEA_LGPL
-src/frama-c/plugins/dive/style.json: .ignore
-src/frama-c/plugins/dive/tippy.css: .ignore
-src/frama-c/plugins/eva/Coverage.tsx: CEA_LGPL
-src/frama-c/plugins/eva/CoverageMeter.tsx: CEA_LGPL
-src/frama-c/plugins/eva/Summary.tsx: CEA_LGPL
-src/frama-c/plugins/eva/api/general/index.ts: CEA_LGPL
-src/frama-c/plugins/eva/api/values/index.ts: CEA_LGPL
-src/frama-c/plugins/eva/index.tsx: CEA_LGPL
-src/frama-c/plugins/eva/pkg.json: .ignore
-src/frama-c/plugins/eva/style.css: .ignore
-src/frama-c/plugins/eva/style_summary.css: .ignore
-src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL
-src/frama-c/plugins/pivot/api/general/index.ts: CEA_LGPL
-src/frama-c/plugins/studia/api/studia/index.ts: CEA_LGPL
-src/frama-c/react-pivottable.d.ts: CEA_LGPL
-src/frama-c/richtext.tsx: CEA_LGPL
-src/frama-c/server.ts: CEA_LGPL
-src/frama-c/states.ts: CEA_LGPL
-src/ivette/index.tsx: CEA_LGPL
-src/ivette/prefs.tsx: CEA_LGPL
-src/main/index.js: CEA_LGPL
-src/renderer/Application.tsx: CEA_LGPL
-src/renderer/Controller.tsx: CEA_LGPL
-src/renderer/Extensions.tsx: CEA_LGPL
-src/renderer/Laboratory.tsx: CEA_LGPL
-src/renderer/Preferences.tsx: CEA_LGPL
-src/renderer/index.js: CEA_LGPL
-src/renderer/style.css: .ignore
-src/sandbox/README.md: .ignore
-src/sandbox/qsplit.tsx: CEA_LGPL
-tests/eva-1.i: .ignore
-tests/eva-2.i: .ignore
-tsconfig.json: .ignore
-tsfmt.json: .ignore
-webpack.main.js: CEA_LGPL
-webpack.renderer.js: CEA_LGPL
-yarn.lock: .ignore
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
deleted file mode 100644
index b7744174c9546fc79de00c3eac1f52f84188f988..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ /dev/null
@@ -1,202 +0,0 @@
-E_ACSL.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-Makefile.in: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-README: .ignore
-configure.ac: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-tab-in-changelog.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-contrib/libdlmalloc/dlmalloc.c: MODIFIED_DLMALLOC
-doc/Changelog: .ignore
-doc/doxygen/doxygen.cfg.in: .ignore
-license/CEA_LGPL: .ignore
-license/LGPLv2.1: .ignore
-license/SPARETIMELABS: .ignore
-license/headache_config.txt: .ignore
-man/e-acsl-gcc.sh.1: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-scripts/e-acsl-gcc.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-scripts/e-acsl-gcc.sh.comp: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_assert.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_assert.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_assert_data.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_contract.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_contract.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_temporal.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_temporal.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_alias.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_bits.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_bits.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_concurrency.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_config.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_debug.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_malloc.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_malloc.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_private_assert.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_private_assert.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_rtl_error.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_rtl_error.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_rtl_io.c: MODIFIED_SPARETIMELABS
-share/e-acsl/internals/e_acsl_rtl_io.h: MODIFIED_SPARETIMELABS
-share/e-acsl/internals/e_acsl_rtl_string.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_rtl_string.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_shexec.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_shexec.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_trace.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/internals/e_acsl_trace.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/libc_replacements/e_acsl_stdio.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/libc_replacements/e_acsl_stdio.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/libc_replacements/e_acsl_string.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/libc_replacements/e_acsl_string.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/numerical_model/e_acsl_floating_point.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/numerical_model/e_acsl_floating_point.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/numerical_model/e_acsl_gmp_api.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_safe_locations.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_safe_locations.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/e_acsl_heap.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/e_acsl_heap.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/analyses_datatype.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/analyses_datatype.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/analyses.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/analyses.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/analyses_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/e_acsl_visitor.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/e_acsl_visitor.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/labels.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/labels.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/logic_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/logic_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/memory_tracking.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/rte.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/rte.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/assert.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/assert.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/assigns.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/assigns.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/contract.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/contract.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/contract_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/env.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/env.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/global_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/global_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/gmp.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/gmp.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/injector.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/injector.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/libc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/libc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/literal_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/literal_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/logic_array.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/logic_array.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/memory_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/memory_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/memory_translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/memory_translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/quantif.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/quantif.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/rational.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/rational.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/smart_exp.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/smart_exp.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/smart_stmt.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/smart_stmt.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_annots.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_annots.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_ats.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_ats.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_predicates.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_predicates.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_rtes.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_rtes.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_terms.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_terms.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_utils.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate_utils.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translation_error.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translation_error.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/typed_number.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/typed_number.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/builtins.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/builtins.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/error.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/error.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/gmp_types.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/gmp_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/logic_aggr.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/logic_aggr.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/misc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/misc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/varname.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/varname.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/main.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/main.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/options.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/options.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/rtl.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/rtl.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-tests/E_ACSL_test.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-tests/wrapper.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-tests/test_config: .ignore
-tests/test_config_dev: .ignore
-tests/builtin/test_config: .ignore
-tests/builtin/test_config_dev: .ignore
-tests/concurrency/test_config: .ignore
-tests/concurrency/test_config_dev: .ignore
-tests/format/test_config: .ignore
-tests/format/test_config_dev: .ignore
-tests/full-mtracking/test_config: .ignore
-tests/full-mtracking/test_config_dev: .ignore
-tests/gmp-only/test_config: .ignore
-tests/gmp-only/test_config_dev: .ignore
-tests/temporal/test_config: .ignore
-tests/temporal/test_config_dev: .ignore
diff --git a/src/plugins/from/From.mli.bak b/src/plugins/from/From.mli.bak
deleted file mode 100644
index 37c080316da19087a5b5be4601cdbfdfed815d6c..0000000000000000000000000000000000000000
--- a/src/plugins/from/From.mli.bak
+++ /dev/null
@@ -1,25 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* $Id: From.mli,v 1.6 2008-04-01 09:25:20 uid568 Exp $ *)
-
-(** No function is directly exported: they are registered in {!Db.From}. *)
diff --git a/src/plugins/impact/Impact.ml.bak b/src/plugins/impact/Impact.ml.bak
deleted file mode 100644
index 982e44e587fab3d2611a7e5e7a0a4d2b5b624ce3..0000000000000000000000000000000000000000
--- a/src/plugins/impact/Impact.ml.bak
+++ /dev/null
@@ -1,45 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* $Id: Impact.mli,v 1.1 2008-04-08 14:59:02 uid568 Exp $ *)
-
-open Cil_types
-
-(** Impact analysis.
-    @see <../impact/index.html> internal documentation. *)
-module Register : sig
-  val compute_pragmas: (unit -> stmt list)
-  (** Compute the impact analysis from the impact pragma in the program.
-      Print and slice the results according to the parameters -impact-print
-      and -impact-slice.
-      @return the impacted statements *)
-
-  val from_stmt: (stmt -> stmt list)
-  (** Compute the impact analysis of the given statement.
-      @return the impacted statements *)
-
-  val from_nodes:
-    (kernel_function -> PdgTypes.Node.t list -> PdgTypes.NodeSet.t)
-    (** Compute the impact analysis of the given set of PDG nodes,
-        that come from the given function.
-        @return the impacted nodes *)
-end = Register
diff --git a/src/plugins/inout/Inout.mli.bak b/src/plugins/inout/Inout.mli.bak
deleted file mode 100644
index 3d0eae33a80d9eb424f37fb0582598518bcb98af..0000000000000000000000000000000000000000
--- a/src/plugins/inout/Inout.mli.bak
+++ /dev/null
@@ -1,31 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* $Id: Inout.mli,v 1.5 2008-04-01 09:25:20 uid568 Exp $ *)
-
-(** Inputs-outputs computations. *)
-
-(** No function is directly exported: they are registered in:
-    - {!Db.Inputs} for computations of non functional inputs;
-    - {!Db.Outputs} for computations of outputs;
-    - {!Db.Operational_inputs} for computation of inout context; and
-    - {!Db.Derefs}. *)
diff --git a/src/plugins/postdominators/Postdominators.mli.bak b/src/plugins/postdominators/Postdominators.mli.bak
deleted file mode 100644
index 9f4252e6b4a8647acd8738fed5a9729c9245affb..0000000000000000000000000000000000000000
--- a/src/plugins/postdominators/Postdominators.mli.bak
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* $Id: Postdominators.mli,v 1.5 2008-04-01 09:25:21 uid568 Exp $ *)
-
-(** Postdominators analysis. *)
-
-(** No function is directly exported: they are registered in
-    {!Db.Postdominators}. *)
diff --git a/src/plugins/slicing/Slicing.ml.bak b/src/plugins/slicing/Slicing.ml.bak
deleted file mode 100644
index 879455704b3b52de4e211adcb21e46c02ce52aa8..0000000000000000000000000000000000000000
--- a/src/plugins/slicing/Slicing.ml.bak
+++ /dev/null
@@ -1,583 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Cil_types
-open Cil_datatype
-
-(** Slicing API. *)
-module Api:sig
-
-  val self: State.t
-  (** Internal state of the slicing tool from project viewpoints. *)
-
-  val set_modes : ?calls:int -> ?callers:bool -> ?sliceUndef:bool ->
-    ?keepAnnotations:bool -> unit -> unit
-  (** Sets slicing parameters related to command line options
-      [-slicing-level], [-slice-callers], [-slice-undef-functions],
-      [-slicing-keep-annotations].
-  *)
-
-  (* ---------------------------------------------------------------------- *)
-
-  (** Slicing project management. *)
-  module Project : sig
-
-    val reset_slicing : unit -> unit
-    (** Function that can be used for:
-        - initializing the slicing tool before starting a slicing project;
-        - removing all computed slices and all internal pending requests
-          of the current slicing project. *)
-
-    (** {3 Kernel function} *)
-
-    val is_called : kernel_function -> bool
-    (** Return [true] iff the source function is called (even indirectly via
-        transitivity) from a [Slice.t]. *)
-
-    val has_persistent_selection : kernel_function -> bool
-    (** Return [true] iff the source function has persistent selection *)
-
-    val change_slicing_level : kernel_function -> int -> unit
-    (** Change the slicing level of this function (see the [-slicing-level]
-        option documentation to know the meaning of the number).
-        @raise SlicingTypes.ExternalFunction if [kf] has no definition.
-        @raise SlicingTypes.WrongSlicingLevel if [n] is not valid. *)
-
-    (** {3 Extraction} *)
-
-    val default_slice_names : kernel_function -> bool  -> int -> string
-    (** Default function used for the optional [?f_slice_names] argument of
-        [extract] function. *)
-
-    val extract : ?f_slice_names:(kernel_function -> bool  -> int -> string) ->
-      string -> Project.t
-    (** Build a new [Db.Project.t] from all [Slice.t] of a project.
-        The string argument is used for naming the new project.
-        Can optionally specify how to name the sliced functions
-        by defining [f_slice_names].
-        [f_slice_names kf src_visi num_slice] has to return the name
-        of the exported functions based on the source function [kf].
-        - [src_visi] tells if the source function name is used
-                     (if not, it can be used for a slice)
-        - [num_slice] gives the number of the slice to name.
-          The entry point function is only exported once :
-          it is VERY recommended to give to it its original name,
-          even if it is sliced.
-    *)
-
-    (** {3 Not for casual users} *)
-
-    val is_directly_called_internal : kernel_function -> bool
-    (** Return [true] if the source function is directly (even via pointer
-        function) called from a [Slice.t]. *)
-
-    val print_dot : filename:string -> title:string -> unit
-    (** May be used to for debugging...
-        Pretty print a representation of the slicing project (call graph)
-        in a dot file which name is the given string. *)
-
-    val pretty : Format.formatter -> unit
-    (** May be used for debugging... Pretty print project information. *)
-
-  end
-
-  (* ---------------------------------------------------------------------- *)
-
-  (** Access to slicing results. *)
-  module Mark : sig
-
-    (** Abstract data type for mark value. *)
-    type t
-
-    val dyn_t : t Type.t
-    (** For dynamic type checking. *)
-
-    val make : data:bool -> addr:bool -> ctrl:bool -> t
-    (** To construct a mark such as
-        [(is_ctrl result, is_data result, isaddr result) =
-        (~ctrl, ~data, ~addr)],
-        [(is_bottom result) = false] and
-        [(is_spare result) = not (~ctrl || ~data || ~addr)]. *)
-
-    val compare : t -> t -> int
-    (** A total ordering function similar to the generic structural
-        comparison function [compare].
-        Can be used to build a map from [t] marks to, for example, colors for
-        the GUI. *)
-
-    val is_bottom : t -> bool
-    (** [true] iff the mark is empty: it is the only case where the
-        associated element is invisible. *)
-
-    val is_spare : t -> bool
-    (** Smallest visible mark. Usually used to mark element that need to be
-        visible for compilation purpose, not really for the selected
-        computations. *)
-
-    val is_data : t -> bool
-    (** The element is used to compute selected data.
-        Notice that a mark can be [is_data] and/or [is_ctrl] and/or [is_addr]
-        at the same time. *)
-
-    val is_ctrl : t -> bool
-    (** The element is used to control the program point of a selected
-        data. *)
-
-    val is_addr : t -> bool
-    (** The element is used to compute the address of a selected data. *)
-
-    val get_from_src_func : kernel_function -> t
-    (** The mark [m] related to all statements of a source function [kf].
-        Property : [is_bottom (get_from_func proj kf) = not (Project.is_called proj kf) ] *)
-
-    (** {3 Not for casual users} *)
-
-    val pretty : Format.formatter -> t -> unit
-    (** May be used for debugging... Pretty mark information. *)
-
-  end
-
-  (* ---------------------------------------------------------------------- *)
-
-  (** Slicing selections. *)
-  module Select : sig
-
-    type t
-    (** Internal selection. *)
-
-    val dyn_t : t Type.t
-    (** For dynamic type checking. *)
-
-    type set
-    (** Set of colored selections. *)
-
-    val dyn_set : set Type.t
-    (** For dynamic type checking. *)
-
-    (** {3 Journalized selectors} *)
-
-    val empty_selects : set
-    (** Empty selection. *)
-
-    val select_stmt : set -> spare:bool -> stmt -> kernel_function -> set
-    (** To select a statement. *)
-
-    val select_stmt_ctrl : set -> spare:bool -> stmt -> kernel_function -> set
-    (** To select a statement reachability.
-        Note: add also a transparent selection on the whole statement. *)
-
-    val select_stmt_lval_rw :
-      (set ->
-       Mark.t ->
-       rd:Datatype.String.Set.t ->
-       wr:Datatype.String.Set.t ->
-       stmt ->
-       eval:stmt ->
-       kernel_function -> set)
-    (** To select rw accesses to lvalues (given as a string) related to a
-        statement.
-        Variable names used in the sets of strings [~rd] and [~wr] are relative
-        to the function scope.
-        The interpretation of the address of the lvalues is
-        done just before the execution of the statement [~eval].
-        The selection preserves the [~rd] and ~[wr] accesses contained into
-        the statement [ki].
-        Note: add also a transparent selection on the whole statement.
-    *)
-
-    val select_stmt_lval :
-      (set -> Mark.t -> Datatype.String.Set.t -> before:bool -> stmt ->
-       eval:stmt -> kernel_function -> set)
-    (** To select lvalues (given as string) related to a statement.
-        Variable names used in the sets of strings [~rd] and [~wr] are relative
-        to the function scope.
-        The interpretation of the address of the lvalue is
-        done just before the execution of the statement [~eval].
-        The selection preserve the value of these lvalues before or
-        after (c.f. boolean [~before]) the statement [ki].
-        Note: add also a transparent selection on the whole statement.
-    *)
-
-    val select_stmt_annots :
-      (set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool ->
-       slicing_pragma:bool -> loop_inv:bool -> loop_var:bool ->
-       stmt -> kernel_function -> set)
-    (** To select the annotations related to a statement.
-        Note: add also a transparent selection on the whole statement. *)
-
-    val select_func_lval_rw :
-      (set -> Mark.t -> rd:Datatype.String.Set.t -> wr:Datatype.String.Set.t ->
-       eval:stmt -> kernel_function -> set)
-    (** To select rw accesses to lvalues (given as a string) related to a
-        function.
-        Variable names used in the sets of strings [~rd] and [~wr] are relative
-        to the function scope.
-        The interpretation of the address of the lvalues is
-        done just before the execution of the statement [~eval].
-        The selection preserve the value of these lvalues into the whole
-        project.
-    *)
-
-    val select_func_lval :
-      (set -> Mark.t -> Datatype.String.Set.t -> kernel_function -> set)
-    (** To select lvalues (given as a string) related to a function.
-        Variable names used in the sets of strings [lval_str] string are
-        relative to the scope of the first statement of [kf].
-        The interpretation of the address of the lvalues is
-        done just before the execution of the first statement [kf].
-        The selection preserve the value of these lvalues before
-        execution of the return statement. *)
-
-    val select_func_return : set -> spare:bool -> kernel_function -> set
-    (** To select the function result (returned value). *)
-
-    val select_func_calls_to : set -> spare:bool -> kernel_function -> set
-    (** To select every calls to the given function, i.e. the call keeps
-        its semantics in the slice. *)
-
-    val select_func_calls_into : set -> spare:bool -> kernel_function -> set
-    (** To select every calls to the given function without the selection of
-        its inputs/outputs. *)
-
-    val select_func_annots :
-      (set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool ->
-       slicing_pragma:bool -> loop_inv:bool -> loop_var:bool ->
-       kernel_function -> set)
-    (** To select the annotations related to a function. *)
-
-    val select_func_zone :
-      (set -> Mark.t -> Locations.Zone.t -> kernel_function -> set)
-    (** To select an output zone related to a function. *)
-
-    val select_stmt_zone :
-      (set -> Mark.t -> Locations.Zone.t -> before:bool -> stmt ->
-       kernel_function -> set)
-    (** To select a zone value related to a statement.
-        Note: add also a transparent selection on the whole statement. *)
-
-    val select_stmt_term :
-      (set -> Mark.t -> term -> stmt ->
-       kernel_function -> set)
-    (** To select a predicate value related to a statement.
-        Note: add also a transparent selection on the whole statement. *)
-
-    val select_stmt_pred :
-      (set -> Mark.t -> predicate -> stmt ->
-       kernel_function -> set)
-    (** To select a predicate value related to a statement.
-        Note: add also a transparent selection on the whole statement. *)
-
-    val select_stmt_annot :
-      (set -> Mark.t -> spare:bool -> code_annotation ->  stmt ->
-       kernel_function -> set)
-    (** To select the annotations related to a statement.
-        Note: add also a transparent selection on the whole statement. *)
-
-    val select_pdg_nodes :
-      (set -> Mark.t  -> PdgTypes.Node.t list -> kernel_function -> set)
-    (** To select nodes of the PDG
-        - if [is_ctrl_mark m],
-          propagate ctrl_mark on ctrl dependencies
-        - if [is_addr_mark m],
-          propagate addr_mark on addr dependencies
-        - if [is_data_mark m],
-          propagate data_mark on data dependencies
-        - mark the node with a spare_mark and propagate so that
-          the dependencies that were not selected yet will be marked spare. *)
-
-    (** {3 Not for casual users} *)
-
-    val get_function : t -> kernel_function
-    (** May be used to get the function related to an internal selection. *)
-
-    val merge_internal : t -> t -> t
-    val add_to_selects_internal : t -> set -> set
-    val iter_selects_internal : (t -> unit) -> set -> unit
-    val fold_selects_internal : ('a -> t -> 'a) -> 'a -> set -> 'a
-
-    val select_stmt_internal : (kernel_function -> ?select:t ->
-                                stmt -> Mark.t -> t)
-    (** May be used to select a statement :
-        - if [is_ctrl_mark m],
-          propagates ctrl_mark on ctrl dependencies of the statement
-        - if [is_addr_mark m],
-          propagates addr_mark on addr dependencies of the statement
-        - if [is_data_mark m],
-          propagates data_mark on data dependencies of the statement
-        - otherwise, marks the node with a spare_mark and propagate so that
-          the dependencies that were not selected yet will be marked spare.
-          When the statement is a call, its functional inputs/outputs are
-          also selected (The call is still selected even it has no output).
-          When the statement is a composed one (block, if, etc...),
-          all the sub-statements are selected.
-          @raise SlicingTypes.NoPdg when there is no PDG for the
-               [kernel_function] (related to [PdgTypes.Pdg.is_top]). *)
-
-    val select_label_internal : (kernel_function -> ?select:t ->
-                                 Logic_label.t -> Mark.t -> t)
-    (** May be used to select a label. *)
-
-    val select_min_call_internal :
-      (kernel_function -> ?select:t -> stmt -> Mark.t -> t)
-    (** May be used to select a statement call without its
-        inputs/outputs so that it doesn't select the statements computing the
-        inputs of the called function as [select_stmt_internal] would do.
-        @raise Invalid_argument when the [stmt] isn't a call.
-        @raise SlicingTypes.NoPdg when there is no PDG for the
-               [kernel_function] (related to [PdgTypes.Pdg.is_top]). *)
-
-    val select_stmt_zone_internal :
-      (kernel_function -> ?select:t ->
-       stmt -> before:bool -> Locations.Zone.t -> Mark.t -> t)
-    (** May be used to select a zone value at a program point.
-        @raise SlicingTypes.NoPdg when there is no PDG for the
-               [kernel_function] (related to [PdgTypes.Pdg.is_top]). *)
-
-    val select_zone_at_entry_point_internal :
-      (kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t)
-    (** May be used to select a zone value at the beginning of a function.
-        For a defined function, it is similar to [select_stmt_zone_internal]
-        with the initial statement, but it can also be used for undefined
-        functions.
-        @raise SlicingTypes.NoPdg when there is no PDG for the
-               [kernel_function] (related to [PdgTypes.Pdg.is_top]). *)
-
-    val select_zone_at_end_internal :
-      (kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t)
-    (** May be used to select a zone value at the end of a function.
-        For a defined function, it is similar to [select_stmt_zone_internal]
-        with the return statement, but it can also be used for undefined
-        functions.
-        @raise SlicingTypes.NoPdg when there is no PDG for the
-               [kernel_function] (related to [PdgTypes.Pdg.is_top]). *)
-
-    val select_modified_output_zone_internal :
-      (kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t)
-    (** May be used to select the statements that modify the
-        given zone considered as in output.
-        Be careful that it is NOT the same as selecting the zone at the end!
-        (the 'undef' zone is not propagated...). *)
-
-    val select_stmt_ctrl_internal : kernel_function -> ?select:t -> stmt -> t
-    (** May be used to select a statement reachability :
-        Only propagate a ctrl_mark on the statement control dependencies.
-        @raise SlicingTypes.NoPdg when there is no PDG for the
-               [kernel_function] (related to [PdgTypes.Pdg.is_top]). *)
-
-    val select_entry_point_internal :
-      (kernel_function -> ?select:t ->  Mark.t -> t)
-    val select_return_internal :
-      (kernel_function -> ?select:t ->  Mark.t -> t)
-    val select_decl_var_internal :
-      (kernel_function -> ?select:t ->  Cil_types.varinfo -> Mark.t -> t)
-
-    val select_pdg_nodes_internal :
-      (kernel_function -> ?select:t -> PdgTypes.Node.t list -> Mark.t -> t)
-    (** May be used to select PDG nodes. *)
-
-    val pretty : Format.formatter -> t -> unit
-    (** May be used for debugging... Pretty mark information. *)
-
-  end
-
-  (* ---------------------------------------------------------------------- *)
-
-  (** Function slice. *)
-  module Slice : sig
-
-    type t
-    (** Abstract data type for function slice. *)
-
-    val dyn_t : t Type.t
-    (** For dynamic type checking. *)
-
-    val create : kernel_function -> t
-    (** Used to get an empty slice (nothing selected) related to a
-        function. *)
-
-    val remove : t -> unit
-    (** Remove the slice from the project. The slice shouldn't be called. *)
-
-    val remove_uncalled : unit -> unit
-    (** Remove the uncalled slice from the project. *)
-
-    (** {3 Getters} *)
-
-    val get_all: kernel_function -> t list
-    (** Get all slices related to a function. *)
-
-    val get_function : t -> kernel_function
-    (** To get the function related to a slice *)
-
-    val get_callers : t -> t list
-    (** Get the slices having direct calls to a slice. *)
-
-    val get_called_slice : t -> stmt -> t option
-    (** To get the slice directly called by the statement of a slice.
-        Returns None when the statement mark is bottom,
-        or else the statement isn't a call
-        or else the statement is a call to one or several (via pointer)
-        source functions. *)
-
-    val get_called_funcs : t -> stmt -> kernel_function list
-    (** To get the source functions called by the statement of a slice.
-        Returns an empty list when the statement mark is bottom,
-        or else the statement isn't a call
-        or else the statement is a call to a function slice. *)
-
-    val get_mark_from_stmt : t -> stmt -> Mark.t
-    (** Get the mark value of a statement. *)
-
-    val get_mark_from_label : t -> stmt -> Cil_types.label -> Mark.t
-    (** Get the mark value of a label. *)
-
-    val get_mark_from_local_var : t -> varinfo -> Mark.t
-    (** Get the mark value of local variable. *)
-
-    val get_mark_from_formal : t -> varinfo -> Mark.t
-    (** Get the mark from the formal of a function. *)
-
-    val get_user_mark_from_inputs : t -> Mark.t
-    (** Get a mark that is the merged user inputs marks of the slice *)
-
-    (** {3 Not for casual users} *)
-
-    val get_num_id : t -> int
-
-    val from_num_id : kernel_function -> int -> t
-
-    val pretty : Format.formatter -> t -> unit
-    (** May be used for debugging... Pretty print slice information. *)
-
-  end
-
-  (* ---------------------------------------------------------------------- *)
-
-  (** Requests for slicing jobs.
-      Slicing requests are part of a slicing project.
-      So, user requests affect slicing project. *)
-  module Request : sig
-
-    (** {3 Applying the added requests} *)
-
-    val apply_all: propagate_to_callers:bool -> unit
-    (** Apply all slicing requests. *)
-
-    (** {3 Adding slicing requests} *)
-
-    val add_selection: Select.set -> unit
-    (** Add a selection request to all (existing) slices
-        of a function to the project requests. *)
-
-    val add_persistent_selection: Select.set -> unit
-    (** Add a persistent selection request to all slices (already existing or
-        created later) of a function to the project requests. *)
-
-    val add_persistent_cmdline : unit -> unit
-    (** Add persistent selection from the command line. *)
-
-    (** {3 Not for casual users} *)
-
-    val add_slice_selection_internal:Slice.t -> Select.t -> unit
-    (** May be used to add a selection request for a function slice
-        to the project requests. *)
-
-    val add_selection_internal: Select.t -> unit
-    (** May be used to add a selection request to the project requests.
-        This selection will be applied to every slicies of the function
-        (already existing or created later). *)
-
-    val add_call_slice:caller:Slice.t -> to_call:Slice.t -> unit
-    (** May be used to change every call to any [to_call] source or specialisation in order
-        to call [to_call] in [caller]. *)
-
-    val add_call_fun: caller:Slice.t -> to_call:kernel_function -> unit
-    (** May be used to change every call to any [to_call] source or specialisation
-        in order to call the source function [to_call] in [caller]. *)
-
-    val add_call_min_fun: caller:Slice.t -> to_call:kernel_function -> unit
-    (** May be used to change each call to [to_call] in [caller] such that, at least, it
-        will be visible at the end, ie. call either the source function or
-        one of [to_call] slice (depending on the [slicing_level]). *)
-
-    val is_request_empty_internal: unit -> bool
-    (** May be used to know if internal requests are pending. *)
-
-    (* REMOVED: val is_already_selected_internal: Slice.t -> Select.t -> bool *)
-    (** Return true when the requested selection is already selected into the
-        slice. *)
-
-    val apply_all_internal: unit -> unit
-    (** May be used to apply all slicing requests. *)
-
-    val apply_next_internal: unit -> unit
-    (** May be used to apply the first slicing request of the project list
-        and remove it from the list.
-        That may modify the contents of the remaining list.
-        For example, new requests may be added to the list. *)
-
-    val merge_slices: Slice.t  -> Slice.t -> replace:bool -> Slice.t
-    (** May be used to build a new slice which marks is a merge of the two given slices.
-        [choose_call] requests are added to the project in order to choose
-        the called functions for this new slice.
-        If [replace] is true, more requests are added to call this new
-        slice instead of the two original slices. When these requests will
-        be applied, the user will be able to remove those two slices using
-        [Db.Slicing.Slice.remove]. *)
-
-    val copy_slice: Slice.t -> Slice.t
-    (** May be used to copy the input slice. The new slice is not called, so it is the user
-        responsibility to change the calls if he wants to. *)
-
-    val split_slice: Slice.t  -> Slice.t list
-    (** May be used to copy the input slice to have one slice for each call of the original
-        slice and generate requests in order to call them.
-        @return the newly created slices. *)
-
-    val propagate_user_marks : unit -> unit
-    (** May be used to apply pending request then propagate user marks to callers
-        recursively then apply pending requests *)
-
-    val pretty : Format.formatter -> unit
-    (** May be used for debugging... Pretty print the request list. *)
-
-  end
-
-end = Api
-
-(* ---------------------------------------------------------------------- *)
-(** For debugging purpose only.
-
-    API used by the tests of slicing (see tests/slicing/libSelect.ml). *)
-
-module PrintSlice: sig
-  val print_fct_stmts:
-    Format.formatter ->
-    kernel_function ->
-    unit
-end = PrintSlice
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/test-file b/test-file
deleted file mode 100644
index 9ab0d2c65c867e9c0ae58b3b99378f09d7c218da..0000000000000000000000000000000000000000
Binary files a/test-file and /dev/null differ