diff --git a/dev/ocamldep_transitive_closure.ml b/dev/ocamldep_transitive_closure.ml
deleted file mode 100644
index e5d845ee0e51f9a9fae3d511626e290af64366a7..0000000000000000000000000000000000000000
--- a/dev/ocamldep_transitive_closure.ml
+++ /dev/null
@@ -1,102 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-let depend_files = ref []
-
-let add_deps s = depend_files:= s :: !depend_files
-
-let root = ref ""
-
-module Dep_graph = Graph.Imperative.Digraph.Concrete(
- struct
- type t = string
- let compare = String.compare
- let hash = Hashtbl.hash
- let equal = (=)
- end)
-
-module Dfs = Graph.Traverse.Dfs(Dep_graph)
-
-module Topological = Graph.Topological.Make(Dep_graph)
-
-module String_set = Set.Make(String)
-
-let dependencies = Dep_graph.create ()
-
-let tokenize_input chan =
- let rec aux acc =
- let line = input_line chan in
- let tokens = Str.(split (regexp " +") line) in
- match List.rev tokens with
- | "\\" :: tail -> aux (tail @ acc)
- | l -> l @ acc
- in
- List.rev (aux [])
-
-let add_edge user provider =
- if Filename.check_suffix user ".cmx" &&
- Filename.check_suffix provider ".cmx"
- then Dep_graph.add_edge dependencies user provider
-
-let parse_one_dependency chan =
- match tokenize_input chan with
- | [] -> () (* Empty line *)
- | target :: ":" :: deps ->
- List.iter (add_edge target) deps;
- | _ -> failwith ("ill formed rule")
-
-let read_dep_file file =
- let chan = open_in file in
- try
- while true do
- parse_one_dependency chan
- done;
- with End_of_file -> close_in chan
-
-let usage =
- Printf.sprintf
- "usage: %s -root file.cmx -deps .depend\n\
- provides the ordered list of .cmx needed to link file.cmx \
- (excluding the latter)"
- (Filename.basename Sys.executable_name)
-
-let err_usage () = Printf.printf "%s\n%!" usage; exit 2
-
-let arguments =
- [ "-deps", Arg.String add_deps, "add a .depend file to set of dependencies";
- "-root", Arg.Set_string root, "root of the dependencies computation";
- ]
-
-let () =
- Arg.parse arguments (fun _ -> err_usage()) usage;
- List.iter read_dep_file !depend_files;
- let add v acc = if v = !root then acc else String_set.add v acc in
- let res = Dfs.fold_component add String_set.empty dependencies !root in
- let l =
- Topological.fold
- (fun s acc -> if String_set.mem s res then s :: acc else acc)
- dependencies []
- in
- Format.(printf "@[<h>%a@]"
- (pp_print_list
- ~pp_sep:(fun fmt () -> pp_print_string fmt " ") pp_print_string)
- l)
diff --git a/dev/size.ml b/dev/size.ml
deleted file mode 100644
index 116006f2bb7c8b8c84a70987bfadb898573c2cd1..0000000000000000000000000000000000000000
--- a/dev/size.ml
+++ /dev/null
@@ -1,93 +0,0 @@
-(**************************************************************************)
-(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
-(* *)
-(* This software is free software; you can redistribute it and/or *)
-(* modify it under the terms of the GNU Library General Public *)
-(* License version 2, with the special exception on linking *)
-(* described in file LICENSE. *)
-(* *)
-(* This software 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. *)
-(* *)
-(**************************************************************************)
-
-(*i $Id: size.ml,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*)
-
-(*i*)
-open Obj
-(*i*)
-
-(*s Pointers already visited are stored in a hash-table, where
- comparisons are done using physical equality. *)
-
-external address_of_value: 'a -> int = "address_of_value"
-
-module H = Hashtbl.Make(
- struct
- type t = Obj.t
- let equal = (==)
- let hash = address_of_value
- end)
-
-let node_table = (H.create 257 : unit H.t)
-
-let in_table o = try H.find node_table o; true with Not_found -> false
-
-let add_in_table o = H.add node_table o ()
-
-let reset_table () = H.clear node_table
-
-(*s Objects are traversed recursively, as soon as their tags are less than
- [no_scan_tag]. [count] records the numbers of words already visited. *)
-
-let size_of_double = size (repr 1.0)
-
-let count = ref 0
-
-let rec traverse t =
- if not (in_table t) then begin
- add_in_table t;
- if is_block t then begin
- let n = size t in
- let tag = tag t in
- if tag < no_scan_tag then begin
- count := !count + 1 + n;
- for i = 0 to n - 1 do
- let f = field t i in
- if is_block f then traverse f
- done
- end else if tag = string_tag then
- count := !count + 1 + n
- else if tag = double_tag then
- count := !count + size_of_double
- else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
- else
- incr count
- end
- end
-
-(*s Sizes of objects in words and in bytes. The size in bytes is computed
- system-independently according to [Sys.word_size]. *)
-
-let res () =
- let r = !count in
- reset_table ();
- r
-
-let size_w ?except o =
- reset_table ();
- (match except with
- | None -> ()
- | Some except -> traverse (repr except)
- );
- count := 0;
- traverse (repr o);
- res ()
-
-
-let size_b ?except o = (size_w ?except o) * (Sys.word_size / 8)
-
-let size_kb ?except o = (size_w ?except o) / (8192 / Sys.word_size)
diff --git a/dev/size.mli b/dev/size.mli
deleted file mode 100644
index 9d67f0a8da54ae7c88ff0d3e5fa369503bb1d7a2..0000000000000000000000000000000000000000
--- a/dev/size.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
-(* *)
-(* This software is free software; you can redistribute it and/or *)
-(* modify it under the terms of the GNU Library General Public *)
-(* License version 2.1, with the special exception on linking *)
-(* described in file LICENSE. *)
-(* *)
-(* This software 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. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(**************************************************************************)
-
-(*i $Id: size.mli,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*)
-
-(* Sizes of ocaml values (in their memory representation).
- Sizes are given in words ([size_w]), bytes ([size_b]) or kilobytes
- ([size_kb]), in a system-independent way. *)
-
-val size_w : ?except:'a -> 'b -> int
-
-val size_b : ?except:'a -> 'b -> int
-
-val size_kb : ?except:'a -> 'b -> int
diff --git a/dev/size_states.ml b/dev/size_states.ml
deleted file mode 100644
index 020f68ab4c2b4c7abe1cd1f60821069c1f91f7d8..0000000000000000000000000000000000000000
--- a/dev/size_states.ml
+++ /dev/null
@@ -1,112 +0,0 @@
-(**************************************************************************)
-(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
-(* *)
-(* This software is free software; you can redistribute it and/or *)
-(* modify it under the terms of the GNU Library General Public *)
-(* License version 2, with the special exception on linking *)
-(* described in file LICENSE. *)
-(* *)
-(* This software 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. *)
-(* *)
-(**************************************************************************)
-
-(* Modified by CEA *)
-
-open Obj
-
-(* Pointers already visited are stored in a hash-table, where
- comparisons are done using physical equality. *)
-
-external address_of_value: 'a -> int = "address_of_value"
-
-module H = Hashtbl.Make(
- struct
- type t = Obj.t
- let equal = (==)
- let hash = address_of_value
- end)
-
-let node_table = (H.create 257 : unit H.t)
-
-(* Addresses that will be skipped *)
-let except_table = (H.create 257 : unit H.t)
-
-let in_table o = H.mem node_table o || H.mem except_table o
-
-let add_in_table o = H.add node_table o ()
-
-let mark_as_skipped () =
- H.iter (fun addr () -> H.add except_table addr ()) node_table
-
-let reset_table () = H.clear node_table
-
-(*s Objects are traversed recursively, as soon as their tags are less than
- [no_scan_tag]. [count] records the numbers of words already visited. *)
-
-let size_of_double = size (repr 1.0)
-
-let count = ref 0
-
-let rec traverse t =
- if not (in_table t) then begin
- add_in_table t;
- if is_block t then begin
- let n = size t in
- let tag = tag t in
- if tag < no_scan_tag then begin
- count := !count + 1 + n;
- for i = 0 to n - 1 do
- let f = field t i in
- if is_block f then traverse f
- done
- end else if tag = string_tag then
- count := !count + 1 + n
- else if tag = double_tag then
- count := !count + size_of_double
- else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
- else
- incr count
- end
- end
-
-let res () =
- let r = !count in
- reset_table ();
- count := 0;
- r
-
-(* CEA *)
-
-let all_sizes () =
- Gc.compact ();
- Gc.set { (Gc.get ()) with
- Gc.max_overhead = 1000000; allocation_policy = 1 } (* disable compaction *);
- let states =
- State_builder.States.fold (fun name _ v _ acc -> (name, Obj.repr v) :: acc) []
- in
- let ast = List.assoc "AST" states in
- let add acc name =
- let size : int = (res ()) / 1000 in
- if size <> 0 then (size, name) :: acc else acc
- in
- (* Compute the size of the AST, and mark the entire AST as skipped *)
- traverse ast;
- mark_as_skipped ();
- let res = add [] "AST" in
- (* Now traverse the other states, but implicitly excluding the AST *)
- let aux acc (state, v) =
- traverse v;
- add acc state
- in
- let res = List.fold_left aux res states in
- (* Sort by increasing size *)
- let res = List.sort (fun (s1, _) (s2, _) -> compare s1 s2) res in
- let pp fmt (size, name) = Format.fprintf fmt "@[%d kW, %s@]" size name in
- Kernel.result "## Sizes ##@.%a"
- (Pretty_utils.pp_list ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pp) res
-
-let () = Boot.Main.extend all_sizes
diff --git a/doc/developer/METADOC.txt b/doc/developer/METADOC.txt
deleted file mode 100644
index e17f478eed5b7fead89092dcdbd419fd6f54e0f8..0000000000000000000000000000000000000000
--- a/doc/developer/METADOC.txt
+++ /dev/null
@@ -1,36 +0,0 @@
-=========================================================================
-Ce fichier contient les règles à suivre pour écrire la doc du développeur
-=========================================================================
-
-* Les instructions de "doc/www/src/metadoc.NE_PAS_ECRIRE" doivent être
- appliquées.
-
-* Les fichiers portent l'extension .pretex pour permettre leur preprocessing
-
-* L'index doit être tenu à jour
-
-* Les redondances dans l'index (deux entrées différentes correspondant à la
- même chose) ne sont autorisées seulement si une des deux entrées référence
- proprement l'autre à l'aide d'un tag "see".
-
-* L'annexe "Changes" doit être tenue à jour.
-
-* Les macros doivent être définies dans macros.tex
-
-* Les macros doivent être au maximum utilisées.
- En particulier:
- o les environnements dérivés de "code" pour le code
- - autoconfcode pour les configure.in
- - makecode pour les makefile
- - ccode pour le C
- - camlcode pour le caml
- - code pour les autres codes (ligne de commandes par exemple)
- o l'environnement "example" pour les exemples
- o l'environnement "important" pour les choses importantes
- o l'environnement "convention" pour les conventions qu'un développeur doit
- respecter
- o l'environnement "prereq" pour les prérequis nécessaires à la bonne
- compréhension
- o les macros pour les noms de langage/d'outils (c'est la même macro
- \langage à l'origine)
- o les macros pour les entrées d'index
diff --git a/lib/plugins/PLUGINS.README b/lib/plugins/PLUGINS.README
deleted file mode 100644
index 3c65748fbb04e13488b954dd5a722b7b2952007f..0000000000000000000000000000000000000000
--- a/lib/plugins/PLUGINS.README
+++ /dev/null
@@ -1,2 +0,0 @@
-Do not add any files in this directory:
-It should only be used by Makefile.plugin.
diff --git a/share/META.frama-c b/share/META.frama-c
deleted file mode 100644
index be05739fdfee70b426d186932e71a06352db62e4..0000000000000000000000000000000000000000
--- a/share/META.frama-c
+++ /dev/null
@@ -1,16 +0,0 @@
-description="frama-c"
-version=""
-requires=""
-
-package "kernel" (
- description="The kernel library of frama-c"
- version=""
- requires="@REQUIRES"
- archive(byte) = "frama-c.cma"
- plugin(byte) = "frama-c.cma"
- archive(native) = "frama-c.cmxa"
- plugin(native) = "frama-c.cmxs"
- directory=""
-)
-
-directory=""
diff --git a/share/libc.c b/share/libc.c
deleted file mode 100644
index f243b8dfdb570788ede392ad3b446d10b2c82939..0000000000000000000000000000000000000000
--- a/share/libc.c
+++ /dev/null
@@ -1,22 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2024 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
diff --git a/share/win32_installer.iss b/share/win32_installer.iss
deleted file mode 100755
index ee7d435102c3cca564bd0778f9b5b6774608c72a..0000000000000000000000000000000000000000
--- a/share/win32_installer.iss
+++ /dev/null
@@ -1,59 +0,0 @@
-; Script generated by the Inno Setup Script Wizard.
-; SEE THE DOCUMENTATION FOR DETAILS ON CREATING INNO SETUP SCRIPT FILES!
-
-#define MyAppName "Frama-C"
-#define MyAppVerName "Frama-C Boron 20100401"
-#define MyAppPublisher "CEA LIST"
-#define MyAppURL "http://frama-c.com"
-#define MyAppExeName "frama-c-gui.exe"
-
-[Setup]
-; NOTE: The value of AppId uniquely identifies this application.
-; Do not use the same AppId value in installers for other applications.
-; (To generate a new GUID, click Tools | Generate GUID inside the IDE.)
-AppId={{0726456B-CCA1-4836-BEBB-4C5D0DD832E2}
-AppName={#MyAppName}
-AppVerName={#MyAppVerName}
-AppPublisher={#MyAppPublisher}
-AppPublisherURL={#MyAppURL}
-AppSupportURL={#MyAppURL}
-AppUpdatesURL={#MyAppURL}
-DefaultDirName=C:\{#MyAppName}
-DefaultGroupName={#MyAppName}
-AllowNoIcons=yes
-OutputBaseFilename=frama-c-Boron-20100401
-SetupIconFile=C:\Frama-C\share\frama-c\frama-c.ico
-Compression=lzma
-SolidCompression=yes
-ChangesEnvironment=yes
-InfoAfterFile=win32_manual_installation_step.txt
-[Languages]
-Name: "english"; MessagesFile: "compiler:Default.isl"
-
-[Tasks]
-Name: "desktopicon"; Description: "{cm:CreateDesktopIcon}"; GroupDescription: "{cm:AdditionalIcons}"; Flags: unchecked
-Name: "quicklaunchicon"; Description: "{cm:CreateQuickLaunchIcon}"; GroupDescription: "{cm:AdditionalIcons}"; Flags: unchecked
-
-[Files]
-Source: "C:\Frama-C\bin\frama-c-gui.exe"; DestDir: "{app}\bin"; Flags: ignoreversion
-Source: "C:\Frama-C\*"; DestDir: "{app}"; Flags: ignoreversion recursesubdirs createallsubdirs
-Source: "C:\DEV_ROOT\GTK\*"; DestDir: "{app}"; Flags: ignoreversion recursesubdirs createallsubdirs
-Source: "C:\DEV_ROOT\ocamlmgw\*"; DestDir: "{app}"; Flags: ignoreversion recursesubdirs createallsubdirs
-; NOTE: Don't use "Flags: ignoreversion" on any shared system files
-
-[Icons]
-Name: "{group}\{#MyAppName}"; Filename: "{app}\bin\{#MyAppExeName}"; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
-Name: "{group}\manuals"; Filename: "{app}\share\frama-c\manuals"; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
-Name: "{commondesktop}\{#MyAppName}"; Filename: "{app}\bin\{#MyAppExeName}"; Tasks: desktopicon; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
-Name: "{userappdata}\Microsoft\Internet Explorer\Quick Launch\{#MyAppName}"; Filename: "{app}\bin\{#MyAppExeName}"; Tasks: quicklaunchicon; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
-
-[Registry]
-Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "FRAMAC_SHARE"; ValueData: "{app}\share\frama-c"; Flags: uninsdeletevalue
-Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "FRAMAC_LIB"; ValueData: "{app}\lib\frama-c"; Flags: uninsdeletevalue
-Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "FRAMAC_PLUGIN"; ValueData: "{app}\lib\frama-c\plugins"; Flags: uninsdeletevalue
-Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "OCAMLLIB"; ValueData: "{app}\lib"; Flags: uninsdeletevalue
-Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "WHYLIB"; ValueData: "'{app}\lib\why'"; Flags: uninsdeletevalue
-Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "ERGOLIB"; ValueData: "{app}\lib\alt-ergo"; Flags: uninsdeletevalue
-
-
-
diff --git a/share/win32_manual_installation_step.txt b/share/win32_manual_installation_step.txt
deleted file mode 100755
index 6633fc508a6d1e49b1f8e2c2bf90590bfa8a1633..0000000000000000000000000000000000000000
--- a/share/win32_manual_installation_step.txt
+++ /dev/null
@@ -1,4 +0,0 @@
-Frama-C is now installed on your computer.
-Note that no C preprocessor is installed by Frama-C itself.
-We encourage you to install cygwin from http://cygwin.org and to launch Frama-C tools from a shell which contains "gcc" and the "bin" directory of Frama-C in its path.
-
diff --git a/src/plugins/e-acsl/.gitattributes b/src/plugins/e-acsl/.gitattributes
index 88dec68a316871e6ecb5212168857d51337adb01..5309cc70acd8695cc3e277326612d2da6738f9dd 100644
--- a/src/plugins/e-acsl/.gitattributes
+++ b/src/plugins/e-acsl/.gitattributes
@@ -5,10 +5,7 @@
dune-project header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
dune header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
-configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
-
Makefile header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
-Makefile.in header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
*.c header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
*.h header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/markdown-report/META.in b/src/plugins/markdown-report/META.in
deleted file mode 100644
index 28043759d7571d4c856d12af47d511f662f0a1ef..0000000000000000000000000000000000000000
--- a/src/plugins/markdown-report/META.in
+++ /dev/null
@@ -1,12 +0,0 @@
-description = "Frama-C Markdown_report plug-in"
-version = "@VERSION@"
-requires = "frama-c.kernel ppx_deriving ppx_deriving_yojson yojson"
-archive(byte) = "top/Markdown_report.cmo"
-archive(native) = "top/Markdown_report.cmx"
-plugin(native) = "top/Markdown_report.cmxs"
-plugin(byte) = "top/Markdown_report.cmo"
-package "eva_info" (
- requires = "frama-c-markdown_report frama-c-eva"
- plugin(native) = "top/eva_info.cmxs"
- plugin(byte) = "top/eva_info.cmo"
-)