From 03ea95633debf87f6baca7db687fc62b8e945c91 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Jun 2022 10:00:46 +0200
Subject: [PATCH] [devguide] better consistency between LaTeX index and code
comments
---
doc/developer/advance.tex | 7 ++++---
doc/developer/check_api/check_and_compare.ml | 21 ++++++++++++++++++-
doc/developer/tutorial.tex | 4 ++--
src/kernel_services/ast_data/cil_types.mli | 14 +++++++++----
.../ast_queries/logic_typing.mli | 5 ++++-
src/libraries/datatype/datatype.mli | 5 ++++-
src/libraries/datatype/type.mli | 2 +-
src/libraries/project/project.mli | 1 +
src/libraries/stdlib/FCHashtbl.mli | 5 ++++-
src/plugins/gui/pretty_source.mli | 5 ++++-
10 files changed, 54 insertions(+), 15 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 2de2c656364..fa0f3c01ef3 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -131,7 +131,7 @@ lexicographic ordering.
For instance, Section \emph{Wished Plug-in} introduces a new sub-section for
the plug-in \texttt{occurrence} in the following way.
-\codeidxdef{check\_plugin}
+\scodeidxdef{configure.in}{check\_plugin}
\begin{configurecode}
# occurrence
############
@@ -3994,8 +3994,9 @@ stored in the \texttt{b\_extended}\scodeidx{Cil\_types}{behavior}{b\_extended} f
\texttt{Cil\_types.behavior}\scodeidx{Cil\_types}{behavior}.
\item A global extension will be found as a global ACSL annotation in the form of a
\sscodeidx{Cil\_types}{global\_annotation}{Dextended}\texttt{Cil\_types.Dextended} constructor.
-\item A code annotation extension will be stored with an
-\scodeidx{Cil\_types}{AExtended}\texttt{Cil\_types.AExtended} constructor. Such an extension has itself
+\item A code annotation extension will be stored with the
+\sscodeidx{Cil\_types}{code\_annotation}{AExtended}\texttt{Cil\_types.AExtended}
+constructor. Such an extension has itself
different flavors, determined by the \scodeidx{Cil\_types}{ext\_code\_annot\_context} type:
\begin{itemize}
\item it can be meant to be evaluated exactly at the current program point
diff --git a/doc/developer/check_api/check_and_compare.ml b/doc/developer/check_api/check_and_compare.ml
index 0f80ca36c46..2ba4da64a13 100644
--- a/doc/developer/check_api/check_and_compare.ml
+++ b/doc/developer/check_api/check_and_compare.ml
@@ -19,6 +19,23 @@ let index_subentry = Str.regexp {|^.*@\texttt *{\([A-Za-z0-9_]+\)}$|}
let all_caps = Str.regexp "^[A-Z0-9_]+$"
+let is_lower s = 'a' <= s.[0] && s.[0] <= 'z'
+let is_upper s = 'A' <= s.[0] && s.[0] <= 'Z'
+
+(* We have a prefix composed of module names, then maybe a lower case
+ symbol, possibly followed by a single symbol (in the case of a
+ type constructor or record field).
+*)
+let is_ocaml_symbol l =
+ let rec aux = function
+ | [] | [_] -> true
+ | [ t; _ ] when is_lower t -> true
+ | x :: l -> is_upper x && aux l
+ in
+ match l with
+ | [] -> false
+ | x :: l -> is_upper x && aux l
+
let inspect_subentry l =
let check_one_entry e =
let e = repair_word e in
@@ -29,7 +46,9 @@ let inspect_subentry l =
in
try
let l = List.map check_one_entry l in
- (String.concat "." l) ^ "\n"
+ if is_ocaml_symbol l then
+ (String.concat "." l) ^ "\n"
+ else ""
with Exit -> ""
let inspect_entry line =
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 737008eb49d..8a6918be6c6 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -797,7 +797,7 @@ nothing for the other globals.
\sscodeidx{Cil}{visitAction}{DoChildrenPost}
\sscodeidx{Cil}{visitAction}{SkipChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vglob\_aux}
-\scodeidx{Cil\_types}{GFun}
+\sscodeidx{Cil\_types}{global}{GFun}
\scodeidx{Printer\_api}{S.pp\_varinfo}
\texttt{Cil.SkipChildren} tells the visitor not to visit the children
@@ -999,7 +999,7 @@ representing a function definition.
Now we write the GUI extension code:
\ocamlinput{./tutorial/viewcfg/src/gui.ml}
-\scodeidx{Pretty\_source}{PVDecl}
+\sscodeidx{Pretty\_source}{localizable}{PVDecl}
\sscodeidx{Globals}{Functions}{get}
\scodeidx{Kernel\_function}{get\_definition}
\scodeidx{Dgraph\_helper}{graph\_window}
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 506f932eaf8..0cb56d772c0 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -143,7 +143,9 @@ and global =
entire program. Cannot have storage Extern or function type. *)
| GFun of fundec * location
- (** A function definition. *)
+ (** A function definition.
+ @plugin development guide
+ *)
| GAsm of string * location
(** Global asm statement. These ones can contain only a template *)
@@ -1694,6 +1696,8 @@ and ext_code_annot_context =
@since Carbon-20101201 [b_requires] has been added.
@modify Boron-20100401 [b_ensures] is replaced by [b_post_cond].
Old [b_ensures] represent the [Normal] case of [b_post_cond].
+
+ @plugin development guide
*)
and behavior = {
mutable b_name : string; (** name of the behavior. *)
@@ -1704,8 +1708,7 @@ and behavior = {
mutable b_assigns : assigns; (** assignments. *)
mutable b_allocation : allocation; (** frees, allocates. *)
mutable b_extended : acsl_extension list
- (** extensions
- @plugin development guide *)
+ (** extensions *)
}
(** kind of termination a post-condition applies to. See ACSL manual. *)
@@ -1769,7 +1772,10 @@ and code_annotation_node =
| AExtended of string list * bool * acsl_extension
(** extension in a code or loop annotation.
Boolean flag is true for loop extensions and false for code extensions
- @since Silicon-20161101 *)
+ @since Silicon-20161101
+
+ @plugin development guide
+ *)
(** function contract. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e28f890ce5d..be799be80ee 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -91,7 +91,10 @@ type type_namespace = Typedef | Struct | Union | Enum
module Type_namespace: Datatype.S with type t = type_namespace
-(** Functions that can be called when type-checking an extension of ACSL. *)
+(** Functions that can be called when type-checking an extension of ACSL.
+
+ @plugin development guide
+*)
type typing_context = {
is_loop: unit -> bool;
anonCompFieldName : string;
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 31ee2e8af69..02bad2ddd43 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -286,7 +286,10 @@ module type Hashtbl = sig
end
(** A datatype for a type [t] extended with predefined set, map and hashtbl
- over [t]. *)
+ over [t].
+
+ @plugin development guide
+*)
module type S_with_collections = sig
include S
module Set: Set with type elt = t
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 0cc7b1ff57f..8e32184c6b0 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -45,7 +45,7 @@ type 'a ty = 'a t
(** Precedences used for generating the minimal number of parenthesis in
combination with function {!par} below. *)
type precedence =
- | Basic (** @plugin development guide *)
+ | Basic (** Normal precedence @plugin development guide *)
| Call (** @plugin development guide *)
| Tuple
| List
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index 47d055df191..0b607c99804 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -208,6 +208,7 @@ val register_before_remove_hook: (t -> unit) -> unit
(* ************************************************************************* *)
exception IOError of string
+(** @plugin development guide *)
val save: ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit
(** Save a given project in a file. Default project is [current ()].
diff --git a/src/libraries/stdlib/FCHashtbl.mli b/src/libraries/stdlib/FCHashtbl.mli
index c890d905578..3fe0a74217b 100644
--- a/src/libraries/stdlib/FCHashtbl.mli
+++ b/src/libraries/stdlib/FCHashtbl.mli
@@ -20,7 +20,10 @@
(* *)
(**************************************************************************)
-(** Extension of OCaml's [Hashtbl] module. *)
+(** Extension of OCaml's [Hashtbl] module.
+
+ @plugin development guide
+*)
(* No need to expand OCaml's [Hashtbl.S] here: we do not provide an alternative
implementation of [Hashtbl]. Hence, we will always be compatible with the
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index a76f237f0cb..5880954f800 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -36,7 +36,10 @@ type localizable = Printer_tag.localizable =
of the varinfo to distinguish between the various possibilities.
If the varinfo is a global or a local, the kernel_function is the
one in which the variable is declared. The [kinstr] argument is given
- for local variables with an explicit initializer. *)
+ for local variables with an explicit initializer.
+
+ @plugin development guide
+ *)
| PGlobal of global (** all globals but variable declarations and function
definitions. *)
| PIP of Property.t
--
GitLab