diff --git a/Makefile b/Makefile
index 458c48a190606e107506fba09460c33697b62c19..7a62602f3aef3a28b0419d968f24f9bf2d31f629 100644
--- a/Makefile
+++ b/Makefile
@@ -109,16 +109,20 @@ PTEST_USE_WP_CACHE:=yes
include share/Makefile.testing
###############################################################################
-# Server Documentation
+# Linters
################################
-include share/Makefile.serverdoc
-
###############################################################################
# Code prettyfication and lint
include share/Makefile.linting
+###############################################################################
+# Frama-C Documentation
+################################
+
+include share/Makefile.documentation
+
###############################################################################
# Local Variables:
# compile-command: "make"
diff --git a/share/Makefile.serverdoc b/share/Makefile.documentation
similarity index 84%
rename from share/Makefile.serverdoc
rename to share/Makefile.documentation
index 9857ea8f9a53f655d7e98f2439bd2e92ed09e379..4d59b94fec99babcb06e1e63bc10feaf01195d03 100644
--- a/share/Makefile.serverdoc
+++ b/share/Makefile.documentation
@@ -20,6 +20,19 @@
# #
##########################################################################
+##########################################################################
+# #
+# Frama-C Documentation targets #
+# #
+##########################################################################
+
+.PHONY: doc
+
+doc:
+ dune build @doc
+ @echo "Generated Documentation:"
+ @echo " file:///$(PWD)/_build/default/_doc/_html/index.html"
+
##########################################################################
# #
# Generate Documentation for Server Requests and Protocols. #
diff --git a/src/plugins/wp/wp.ml b/src/plugins/wp/wp.ml
index 037fd72723fa408543d6934f7f65151d32ae07e9..3399514978fdea64794d8a15165a3f9cafbf911f 100644
--- a/src/plugins/wp/wp.ml
+++ b/src/plugins/wp/wp.ml
@@ -20,64 +20,220 @@
(* *)
(**************************************************************************)
+(** This the API of the WP plug-in *)
+
+(* -------------------------------------------------------------------------- *)
+(** {1 High-Level External API}
+
+ The following modules are the recommanded entry points for using WP
+ programmatically. They are meant to be relatively stable over time.
+
+*)
+(* -------------------------------------------------------------------------- *)
+
+(** WP Proof Obligation Generator and Management *)
+module VC = VC
+
+(** Provers and Proof Obligations Results *)
+module VCS = VCS
+
+(** WP Plugin Interface *)
module Wp_parameters = Wp_parameters
-module Ctypes = Ctypes
-module Clabels = Clabels
-module MemoryContext = MemoryContext
-module LogicUsage = LogicUsage
-module RefUsage = RefUsage
-module NormatLabels = NormAtLabels
-module WpPropId = WpPropId
-module Mcfg = Mcfg
-module Context = Context
-module Warning = Warning
-module Lang = Lang
+
+(* -------------------------------------------------------------------------- *)
+(** {1 Advanced Usage API}
+
+ The following modules entry points for using WP advanced features,
+ such as proof obligation manipulation, tactics and strategies.
+ These modules might expose internal features of WP that are subject
+ to change. Developpers using this API are encouraged to contact us
+ for a roadmap information and further collaboration.
+*)
+(* -------------------------------------------------------------------------- *)
+
+(** High-Level Term Representation *)
module Repr = Repr
-module Passive = Passive
-module Splitter = Splitter
-module LogicBuiltins = LogicBuiltins
+
+(** Low-Level Logic Terms and Predicates *)
+module Lang = Lang
+
+(** Generated Logic Definitions *)
module Definitions = Definitions
-module Cint = Cint
+
+(** Proof Task and Simplifiers *)
+module Conditions = Conditions
+
+(** Tactics Entry Points *)
+module Tactical = Tactical
+
+(** Strategies Entry Points *)
+module Strategy = Strategy
+
+(** WP Proof Obligation Generator *)
+module Generator = Generator
+
+(** Command Line Processing *)
+module Register = Register
+
+(* -------------------------------------------------------------------------- *)
+(** {1 Low-Level Internal API}
+
+ The following modules are _not_ intended to be used externally. The target
+ audience is WP plug-in developpers. However, developpers interested in
+ such low-level features are encouraged to contact us for more informations.
+*)
+(* -------------------------------------------------------------------------- *)
+
+(** {2 Model Registration} *)
+
+module Factory = Factory
+module WpContext = WpContext
+
+(** {2 Memory Models} *)
+
+module MemDebug = MemDebug
+module MemEmpty = MemEmpty
+module MemLoader = MemLoader
+module MemMemory = MemMemory
+module MemRegion = MemRegion
+module MemTyped = MemTyped
+module MemVal = MemVal
+module MemVar = MemVar
+module MemZeroAlias = MemZeroAlias
+
+(** {2 Other Models} *)
+
+module Cint = Cint
module Cfloat = Cfloat
-module Vset = Vset
+module Cmath = Cmath
module Cstring = Cstring
-module Sigs = Sigs
+
+(** {2 State Model} *)
+
+module Sigma = Sigma
+module Passive = Passive
module Mstate = Mstate
-module Conditions = Conditions
-module Filtering = Filtering
-module Plang = Plang
-module Pcfg = Pcfg
-module Pcond = Pcond
+
+(** {2 Model Hypotheses}*)
+
+module MemoryContext = MemoryContext
+module RefUsage = RefUsage
+module WpTarget = WpTarget
+module AssignsCompleteness = AssignsCompleteness
+
+(** {2 Region Analysis} *)
+
+module Region = Region
+module Layout = Layout
+module RegionAccess = RegionAccess
+module RegionAnalysis = RegionAnalysis
+module RegionAnnot = RegionAnnot
+module RegionDump = RegionDump
+
+(** {2 Compilers} *)
+
+module Sigs = Sigs
+module Driver = Driver
+module Context = Context
+module Ctypes = Ctypes
+module Cvalues = Cvalues
+module Clabels = Clabels
module CodeSemantics = CodeSemantics
+module LogicAssigns = LogicAssigns
+module LogicBuiltins = LogicBuiltins
module LogicCompiler = LogicCompiler
module LogicSemantics = LogicSemantics
-module Sigma = Sigma
-module MemVar = MemVar
-module MemTyped = MemTyped
-module CfgCompiler = CfgCompiler
+module LogicUsage = LogicUsage
module StmtSemantics = StmtSemantics
-module Factory = Factory
-module Driver = Driver
-module VCS = VCS
-module Tactical = Tactical
-module Strategy = Strategy
-module Auto = Auto
-module VC = VC
+module Dyncall = Dyncall
+module Matrix = Matrix
+module NormAtLabels = NormAtLabels
+
+(** {2 Core Engine} *)
+
+module CfgAnnot = CfgAnnot
+module CfgCalculus = CfgCalculus
+module CfgCompiler = CfgCompiler
+module CfgDump = CfgDump
+module CfgGenerator = CfgGenerator
+module CfgInfos = CfgInfos
+module CfgInit = CfgInit
+module CfgWP = CfgWP
+module WpReached = WpReached
+module WpPropId = WpPropId
+module WpRTE = WpRTE
+
+(** {2 Proof Engine} *)
+
module Wpo = Wpo
-module ProverTask = ProverTask
+module Auto = Auto
+module Cache = Cache
+module Cleaning = Cleaning
+module Letify = Letify
+module Splitter = Splitter
+module Filtering = Filtering
+
+(** {2 Prover Interface} *)
+
+module Why3Provers = Why3Provers
+module Filter_axioms = Filter_axioms
module Prover = Prover
-module AssignsCompleteness = AssignsCompleteness
+module ProverTask = ProverTask
+module ProverWhy3 = ProverWhy3
+
+(** {2 Script Engine} *)
-(** For gui *)
+module Script = Script
+module Footprint = Footprint
module ProofEngine = ProofEngine
module ProofScript = ProofScript
-module ProofSession = ProofSession
module ProverScript = ProverScript
module ProverSearch = ProverSearch
-module WpRTE = WpRTE
+module ProofSession = ProofSession
+
+(** {2 Tactics} *)
+
+module WpTac = WpTac
+module TacArray = TacArray
+module TacBitrange = TacBitrange
+module TacBittest = TacBittest
+module TacBitwised = TacBitwised
+module TacChoice = TacChoice
+module TacClear = TacClear
+module TacCompound = TacCompound
+module TacCongruence = TacCongruence
+module TacCut = TacCut
+module TacFilter = TacFilter
+module TacHavoc = TacHavoc
+module TacInduction = TacInduction
+module TacInstance = TacInstance
+module TacLemma = TacLemma
+module TacModMask = TacModMask
+module TacNormalForm = TacNormalForm
+module TacOverflow = TacOverflow
+module TacRange = TacRange
+module TacRewrite = TacRewrite
+module TacSequence = TacSequence
+module TacShift = TacShift
+module TacSplit = TacSplit
+module TacUnfold = TacUnfold
+
+(** {2 Error Management} *)
+
+module Warning = Warning
+module Wp_error = Wp_error
+
+(** {2 Printers and Reporting} *)
+
+module Pcfg = Pcfg
+module Pcond = Pcond
+module Plang = Plang
module Rformat = Rformat
-module WpContext = WpContext
-module Why3Provers = Why3Provers
-module ProverWhy3 = ProverWhy3
-module Cache = Cache
-module WpTarget = WpTarget
+module Stats = Stats
+module WpReport = WpReport
+
+(** {2 EVA Proxy} *)
+
+module Wp_eva = Wp_eva
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wprop.ml b/src/plugins/wp/wprop.ml
deleted file mode 100644
index a8684483885d021290a49bdc793ac24facf4753e..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wprop.ml
+++ /dev/null
@@ -1,112 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Indexed Interface --- *)
-(* -------------------------------------------------------------------------- *)
-
-type property =
- | Later of Property.t
- | Proxy of Property.t * Emitter.t * Property.t list
-
-module type Info =
-sig
- include State_builder.Info_with_size
- type key
- val property : key -> property
-end
-
-module type Indexed =
-sig
- type key
- val mem : key -> bool
- val property : key -> Property.t
- val add_hook : (key -> Property.t -> unit) -> unit
-end
-
-module type Indexed2 =
-sig
- type key1
- type key2
- val mem : key1 -> key2 -> bool
- val property : key1 -> key2 -> Property.t
- val add_hook : (key1 -> key2 -> Property.t -> unit) -> unit
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Index-1 Implementation --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Indexed
- (Key:Datatype.S_with_collections)
- (Info:Info with type key = Key.t) =
-struct
-
- type key = Key.t
-
- module H = State_builder.Hashtbl(Key.Hashtbl)(Property)(Info)
-
- let hooks = ref []
- let add_hook f = hooks := !hooks @ [f]
-
- let mem = H.mem
-
- let property (key:key) =
- try H.find key
- with Not_found ->
- let ip =
- match Info.property key with
- | Later ip -> ip
- | Proxy(ip,emitter,ips) ->
- Property_status.logical_consequence emitter ip ips ; ip
- in
- List.iter (fun f -> f key ip) !hooks ;
- H.add key ip ; ip
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Index-2 Wrapper --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Indexed2
- (Key1:Datatype.S_with_collections)
- (Key2:Datatype.S_with_collections)
- (Info:Info with type key = Key1.t * Key2.t) =
-struct
-
- module P = Datatype.Pair_with_collections(Key1)(Key2)
- (struct
- let module_name = Info.name
- end)
- module I = Indexed(P)(Info)
-
- type key1 = Key1.t
- type key2 = Key2.t
-
- let mem a b = I.mem (a,b)
- let property a b = I.property (a,b)
- let add_hook f = I.add_hook (fun (a,b) -> f a b)
-
-end
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wprop.mli b/src/plugins/wp/wprop.mli
deleted file mode 100644
index eaaa2aff6dcbcbfd82d02608597be8a353197769..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wprop.mli
+++ /dev/null
@@ -1,70 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* ------------------------------------------------------------------------ *)
-(**{2 Indexed API} *)
-(* ------------------------------------------------------------------------ *)
-
-type property =
- | Later of Property.t
- | Proxy of Property.t * Emitter.t * Property.t list
-
-module type Info =
-sig
- include State_builder.Info_with_size
- type key
- val property : key -> property
-end
-
-module type Indexed =
-sig
- type key
- val mem : key -> bool
- val property : key -> Property.t
- val add_hook : (key -> Property.t -> unit) -> unit
- (** Hooks are executed once at property creation *)
-end
-
-module type Indexed2 =
-sig
- type key1
- type key2
- val mem : key1 -> key2 -> bool
- val property : key1 -> key2 -> Property.t
- val add_hook : (key1 -> key2 -> Property.t -> unit) -> unit
- (** Hooks are executed once at property creation *)
-end
-
-(* ------------------------------------------------------------------------ *)
-(**{2 Indexes} *)
-(* ------------------------------------------------------------------------ *)
-
-module Indexed
- (Key:Datatype.S_with_collections)
- (Info:Info with type key = Key.t) :
- Indexed with type key = Key.t
-
-module Indexed2
- (Key1:Datatype.S_with_collections)
- (Key2:Datatype.S_with_collections)
- (Info:Info with type key = Key1.t * Key2.t) :
- Indexed2 with type key1 = Key1.t and type key2 = Key2.t