From 3281ad9ceac18280464caafd32ab28916d1c0d4a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 8 Nov 2023 15:31:32 +0100
Subject: [PATCH] [doc] removed broken links

---
 doc/pdg/conclusion.tex                        |  8 +-
 doc/scope/scope.tex                           | 87 +++++++++----------
 .../plugin_entry_points/db.mli                |  6 --
 src/plugins/pdg/register.ml                   |  8 --
 src/plugins/rte/api.mli                       |  3 +-
 src/plugins/scope/scope.mli                   |  3 +-
 src/plugins/slicing/fct_slice.ml              |  3 +-
 src/plugins/slicing/register.ml               |  3 +-
 src/plugins/users/Users.mli                   |  3 -
 9 files changed, 47 insertions(+), 77 deletions(-)

diff --git a/doc/pdg/conclusion.tex b/doc/pdg/conclusion.tex
index 646d2642d4a..b888f9275b0 100644
--- a/doc/pdg/conclusion.tex
+++ b/doc/pdg/conclusion.tex
@@ -6,17 +6,11 @@ Elle est utilisée par les greffons {\sc Security}, {\sc Sparecode} et
 graphiquement en utilisant la fonction d'exportation
 au format {\tt .dot}.\\
 
-D'autres information relatives au développement peuvent être trouvées dans la documentation du code dont un point d'entrée
-est~:
-
-\centerline{\tt doc/code/pdg/index.html}
-
 \section{Limitations}
 
-Les fonctions ayant un nombre d'arguments variable 
+Les fonctions ayant un nombre d'arguments variable
 ne sont pas traitées (mais les appels à de telles fonctions sont gérés).
 
 Par ailleurs, les calculs se basant sur l'analyse de valeur,
 et sur le calcul des dépendances fonctionnelles (\from)
 il hérite des limitations de ces modules.
-
diff --git a/doc/scope/scope.tex b/doc/scope/scope.tex
index f4bb75086d5..4e9847acd94 100644
--- a/doc/scope/scope.tex
+++ b/doc/scope/scope.tex
@@ -31,8 +31,6 @@
 \usepackage{fancyhdr}
 %------------------------------------
 
-\toplinks{}{../index.html}{}
-
 %==============================================================================
 \begin{document}
 
@@ -64,23 +62,23 @@ ou
 On utilise souvent le terme de portée ({\it scope} en anglais)
 en parlant d'une variable pour désigner la zone du programme
 dans laquelle il est valide de l'utiliser.
-Nous parlerons ici de la {\bf portée d'une donnée} pour désigner 
+Nous parlerons ici de la {\bf portée d'une donnée} pour désigner
 de l'ensemble des points de programme pour lesquels la donnée n'est pas
 modifiée. Nous préciserons en \S\ref{data-scope} ce que cela veut dire.\\
 
-Puis, nous généraliserons en \S\ref{prop-scope} à la 
+Puis, nous généraliserons en \S\ref{prop-scope} à la
 {\bf portée d'une propriété}.
 
 \section{Portée d'une donnée}\label{data-scope}
 
 \subsection{Donnée vs. {\it lvalue}}
 
-Nous utilisons ici le terme de {\bf donnée} pour représenter une zone mémoire. 
+Nous utilisons ici le terme de {\bf donnée} pour représenter une zone mémoire.
 Une donnée est généralement désignée
 par une expression de la famille des {\it lvalues} qui caractérise
 les expressions qui apparaissent à gauche d'une affectation.
 Lorsqu'on parle de la donnée correspondant à une variable X,
-il n'y a pas d'ambiguïté, il s'agit précisement la zone mémoire allouée pour 
+il n'y a pas d'ambiguïté, il s'agit précisement la zone mémoire allouée pour
 ranger la valeur de X.
 En revanche, lorsque la donnée est désignée par {\tt T[i]},
 la traduction en terme de zone mémoire fait intervenir la valeur de i.
@@ -92,20 +90,20 @@ information sur i.
 
 \subsection{Discussion sur la portée}
 
-On souhaite déterminer l'ensemble $\sc(D@L)$ des points 
+On souhaite déterminer l'ensemble $\sc(D@L)$ des points
 pour lesquels la donnée D a la même valeur qu'au point L.
 Cette définition semble relativement claire au premier abord,
 mais nous allons voir qu'elle manque quelque peu de précision...\\
 
 Pour parler de la valeur d'une donnée en différents points,
 nous allons raisonner en terme de traces d'exécution.
-Si on cherche à déterminer $\sc(D@L)$, 
+Si on cherche à déterminer $\sc(D@L)$,
 il peut sembler naturel de ne s'intéresser qu'aux traces qui passent par L
 car que signifierait {\it avoir la même valeur qu'en L} pour les autres traces~?
 
 Mais qu'en est-il des points appartenant à $\sc$ ?
 
-Pour la séquence~: 
+Pour la séquence~:
 
 \centerline{\verb!L: if (c) L1:.. else L2:...!}
 
@@ -117,32 +115,32 @@ par L et P, D ait la même valeur.
 Mais avec cette définition, si on a :
 
 \begin{verbatim}
-L0 :... 
-if (c) { 
-  L1:.. 
-  } 
-else { 
-  L2a:... 
-  D=x; 
-  L2b:... 
-} 
+L0 :...
+if (c) {
+  L1:..
+  }
+else {
+  L2a:...
+  D=x;
+  L2b:...
+}
 L3:...
 \end{verbatim}
 
 on va avoir $L3 \in \sc(D@L1)$. Est-ce que c'est bien ce qu'on veut avoir ?
 Comme par ailleurs, on a évidemment $L0 \in \sc(D@L1)$, est-ce qu'on aura pas
 tendance à penser que D à la même valeur en L0 et en L3 ?
-Il faudra mettre en évidence le fait qu'on s'intéresse uniquement 
+Il faudra mettre en évidence le fait qu'on s'intéresse uniquement
 aux traces passant pas L1...\\
- 
-Au premier abord, on a l'intuition qu'une relation 
+
+Au premier abord, on a l'intuition qu'une relation
 {\it avoir la même valeur pour D} est une relation d'équivalence, mais ce n'est
 si simple étant donné qu'on
 ne considère pas les mêmes traces. Si c'était le cas, on se retrouverait
 rapidement à dire que D a la même valeur en L2a et L2b en propageant en
 arrière à partir de L3, et en avant à partir de L0 !!!
 
-Par ailleurs, qu'est-ce que ça veut dire pour les traces 
+Par ailleurs, qu'est-ce que ça veut dire pour les traces
 qui contiennent plusieurs fois L et/ou P ?
 
 Prenons quelques exemples :
@@ -163,14 +161,14 @@ Prenons quelques exemples :
 \end{itemize}
 
 Il semble alors judicieux de distinguer une sélection avant $\sca$
-et une sélection arrière $\scb$, pour pouvoir avoir $n1 \in \sca$ et $n2 \in \scb$.  
-La signification serait alors : 
-$P \in \sca$ ssi à chaque fois que l'on va de L à P, 
-D a la même valeur en ces deux points, 
-mais il faut se restreindre aux chemins qui ne font pas un tour de boucles... 
+et une sélection arrière $\scb$, pour pouvoir avoir $n1 \in \sca$ et $n2 \in \scb$.
+La signification serait alors :
+$P \in \sca$ ssi à chaque fois que l'on va de L à P,
+D a la même valeur en ces deux points,
+mais il faut se restreindre aux chemins qui ne font pas un tour de boucles...
 càd ceux qui ne repassent pas par L.
 
-Mais si on a : 
+Mais si on a :
 
 \centerline{\verb!P:... Lp:... L:... D=x; ... goto Lp;!}
 
@@ -189,7 +187,7 @@ Ou alors, on dit que c'est normal~?
 \subsection{Définitions}
 
 On définit finalement les ensembles en considérant les traces d'exécution
-qui traversent une fonction 
+qui traversent une fonction
 sans rentrer dans les appels de fonction (en cas d'appel récursif, on ne
 considère donc qu'une exécution de la fonction).
 On considère les exécutions de la fonction
@@ -200,11 +198,11 @@ comme si on en regardait la trace dans un débogueur.
 \begin{itemize}
   \item $P \in \sca(D@L)$ si et seulement pour toute exécution de la fonction
     qui passe par L, si on s'arrête en P,
-    D a toujours la même valeur 
+    D a toujours la même valeur
     que la {\bf dernière} fois que l'on est passé en L~;
   \item $P \in \scb(D@L)$ si et seulement si pour toute exécution
     de la fonction qui passe par L, si on s'arrête en P,
-    D a toujours la même valeur que 
+    D a toujours la même valeur que
     la {\bf prochaine} fois que l'on passe en L.
 \end{itemize}
 
@@ -212,7 +210,7 @@ comme si on en regardait la trace dans un débogueur.
 
 En pratique, les résultats sont présentés comme une liste d'instructions et non
 directement de points de programme. Il faut donc préciser
-qu'on choisit de considérer l'étiquette de départ L comme une instruction 
+qu'on choisit de considérer l'étiquette de départ L comme une instruction
 à part entière, et l'instruction $I_L$ comme étant l'instruction suivante~:
 donc en suivant la définition, si on place un point d'arrêt en $I_L$,
 D a toujours la même valeur que la dernière fois que l'on est passé en L,
@@ -258,13 +256,13 @@ Puis on lance le calcul en indiquant qu'il faut traiter l'instruction L.
 Pour chaque chaque instruction I à traiter, le calcul consiste à
 calculer la marque $m' = T(I, m_a(I))$ à propager à ses successeurs.
 Pour chaque successeur I' de I, on va ajoute la marque m'
-à un éventuel résultat précédent $m_a(I')$ 
+à un éventuel résultat précédent $m_a(I')$
 à l'aide de l'opération {\tt merge}
 ($m_a(I')=m'$ si on n'a encore rien calculé).
 Si $m_a(I')$ n'est pas modifiée par l'opération, on arrête de propager par ce
 chemin. Sinon, on met I' dans la liste des instructions à traiter.
 
-Quand le résultat est stabilisé (plus d'instructions à traiter), 
+Quand le résultat est stabilisé (plus d'instructions à traiter),
 on a donc~:
 $$
 m_a(I') = \bigcup_{I \in pred(I')} T(I, m_a(I))
@@ -293,7 +291,7 @@ Il s'agit encore de calculer une marque $m_b(P)$ pour chaque point P.
 
 Cela nécessite d'initialiser tous les points à {\tt NotSeen},
 sauf le point de départ L qui est initialisé à  {\tt Start}.
-Puis on lance le calcul en indiquant qu'il faut traiter 
+Puis on lance le calcul en indiquant qu'il faut traiter
 les prédécesseurs de L.
 
 Pour chaque chaque instruction I à traiter, le calcul consiste à
@@ -312,8 +310,8 @@ $$
 m_b(I) = T(I, \bigcup_{I' \in succ(I)} m_b(I'))
 $$
 On récupère la liste des instructions
-marquées {\tt SameVal}, 
-et on ajoute l'instruction L de départ marquée {\tt Start} 
+marquées {\tt SameVal},
+et on ajoute l'instruction L de départ marquée {\tt Start}
 si $T(L, \bigcup_{I \in succ(L)} m_b(I))$ vaut {\tt SameVal}.
 Cela nous donne $\scb(D,L)$.\\
 
@@ -330,7 +328,7 @@ soit il s'agit du point de départ L, soit I est aussi dans $\scb(D,L)$.
 
 Pour tout $P \in \sca(D@L)$, il existe nécessairement un chemin entre L et P,
 et tous les points du chemin sont aussi dans $ \sca(D@L)$.
-De même, pour tout $P \in \scb(D@L)$,  
+De même, pour tout $P \in \scb(D@L)$,
 il existe nécessairement un chemin entre P et L,
 
 Il n'y a pas forcement de relation de domination/postdomination entre P et L.\\
@@ -354,7 +352,7 @@ L3b:... \} L4:...!}
 \begin{itemize}
   \item si on a une propriété P portant sur x en L2 (disons $x>0$), on ne peut pas
     forcement la déplacer en L1 car elle peut très bien n'être vraie que dans le
-    cas où la condition c est vraie (par exemple, grâce à une précondition :  
+    cas où la condition c est vraie (par exemple, grâce à une précondition :
     $c \Rightarrow x>0$);
   \item par contre, si on a P en L1, elle est aussi vraie en L2, mais il n'y a pas équivalence, car il faut aussi qu'elle soit vraie en L3a.
   \item idem dans l'autre sens :
@@ -375,7 +373,7 @@ on va voir apparaître~:
 
 \begin{verbatim}
 /*@ assert \valid(p);
-      // synthesized 
+      // synthesized
  */
 x = *p;
 \end{verbatim}
@@ -403,17 +401,17 @@ c'est-à-dire sur le déplacement de propriétés à travers des instructions
 qui ne modifient pas les données utilisées.
 La comparaison des menaces sera donc uniquement syntaxique.\\
 
-Si une propriété P est vraie à un point de programme L1, 
+Si une propriété P est vraie à un point de programme L1,
 elle est aussi vraie pour les points L2 qui suivent L1 tels que~:
 \begin{itemize}
-  \item L2 est dominé par L1 
-(ie. si on passe en L2, on est forcement passé en L1) 
+  \item L2 est dominé par L1
+(ie. si on passe en L2, on est forcement passé en L1)
 \item et la propriété n'est pas modifiée entre L1 et L2.
 \end{itemize}
 Donc si on rencontre une menace identique à P en un point L2
 qui vérifie ces caractéristiques, elle peut être éliminée.\\
 
-Si une propriété est vraie à un point de programme L1, 
+Si une propriété est vraie à un point de programme L1,
 on pourrait aussi se dire qu'elle est
 vraie pour les points L0 qui précèdent L1 tels que~:
 \begin{itemize}
@@ -429,4 +427,3 @@ car à cause des problèmes de terminaison des instructions que l'on traverse,
 %------------------------------------------------------------------------------
 \end{document}
 %==============================================================================
- 
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index f90a7a9fd23..e191d7d2f3a 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -126,16 +126,10 @@ module PostdominatorsTypes: sig
   end
 end
 
-(** Syntactic postdominators plugin.
-    @see <../postdominators/index.html> internal documentation. *)
 module Postdominators: PostdominatorsTypes.Sig
 
-(** Postdominators using value analysis results.
-    @see <../postdominators/index.html> internal documentation. *)
 module PostdominatorsValue: PostdominatorsTypes.Sig
 
-(** Security analysis.
-    @see <../security/index.html> internal documentation. *)
 module Security : sig
 
   val run_whole_analysis: (unit -> unit) ref
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 61d4c901f22..b065d1184b5 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -125,10 +125,6 @@ let () = Db.Main.extend main
 
    A dependency between two nodes can have any combination of these kinds.
 
-   You can find more documentation, particularly on how this graph is built,
-   in this {{:../../pdg/index.html}report} (in French).
-
-
    {2 Dynamic dependencies}
 
    After having built the PDG for a function, there is a way of adding dynamically
@@ -170,10 +166,6 @@ let () = Db.Main.extend main
    So a solid blue edge with a circle arrow represent a data+control dependency for
    instance, while a dotted black edge with a triangle arrow represent a address
    dependency.
-
-   You are invited to look at
-   {{:../../../tests/pdg/doc.g.svg}a simple example}
-   to see the different kinds of dependencies.
 *)
 
 
diff --git a/src/plugins/rte/api.mli b/src/plugins/rte/api.mli
index afae2205b5b..0649aee8d4f 100644
--- a/src/plugins/rte/api.mli
+++ b/src/plugins/rte/api.mli
@@ -20,8 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Runtime Error Annotation Generation plugin.
-    @see <./index.html> internal documentation. *)
+(** Runtime Error Annotation Generation plugin. *)
 
 (** Same result as having [-rte] on the command line*)
 val compute : unit -> unit
diff --git a/src/plugins/scope/scope.mli b/src/plugins/scope/scope.mli
index 560213e8a0d..1221840f6f2 100644
--- a/src/plugins/scope/scope.mli
+++ b/src/plugins/scope/scope.mli
@@ -25,8 +25,7 @@ open Cil_datatype
 
 (** Scope analysis. *)
 
-(** Interface for the Scope plugin.
-    @see <index.html> internal documentation. *)
+(** Interface for the Scope plugin. *)
 module Defs : sig
   val get_defs :
     Kernel_function.t -> stmt -> lval ->
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index c3df7b4ff70..7611cece658 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -27,8 +27,7 @@
  *
  * Most high level function, named [apply_xxx],
  * like [apply_change_call], [apply_missing_outputs], ...,
- * correspond the actions defined in the
- * {{:../../slicing/index.html}specification report}.
+ * correspond the actions defined in the specification report}.
  *
  * Many functions are modifying the marks of a slice,
  * so they can return a list of actions to be applied in order to deal with
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 732110543a6..42bcad35768 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -65,8 +65,7 @@ let () = Db.Main.extend main
 (* {2 Overview}
 
    To have more details about what we are trying to do,
-   you may have a look to the
-   {{:../../slicing/index.html}specification} report (in French).
+   you may have a look to the specification report (in French).
 
    The internal types module ({!module:SlicingTypes.Internals})
    can give a pretty good idea of the kind of objects that we deal with in this
diff --git a/src/plugins/users/Users.mli b/src/plugins/users/Users.mli
index fbc7382de6f..962ae86f83d 100644
--- a/src/plugins/users/Users.mli
+++ b/src/plugins/users/Users.mli
@@ -20,12 +20,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: Users.mli,v 1.5 2008-04-01 09:25:22 uid568 Exp $ *)
 open Cil_types
 (** Users analysis. *)
 
-(** Functions used by another function.
-    @see <../users/index.html> internal documentation. *)
 module Users_register : sig
   val get: (kernel_function -> Kernel_function.Hptset.t)
 end
-- 
GitLab