From f76321ae16375ea24894975f0054180d27a480b2 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Wed, 8 Feb 2023 15:34:24 +0100 Subject: [PATCH] [doc] adapt PDG to new theme --- doc/pdg/.gitignore | 7 +++---- doc/pdg/calls.tex | 6 +++--- doc/pdg/ctrl.tex | 12 ++++++------ doc/pdg/intro.tex | 14 +++++++------- doc/pdg/macros_pdg.tex | 4 +--- doc/pdg/main.tex | 32 +++++++++++++------------------- doc/pdg/pdg.tex | 1 + 7 files changed, 34 insertions(+), 42 deletions(-) diff --git a/doc/pdg/.gitignore b/doc/pdg/.gitignore index 62322591627..61b9f639da6 100644 --- a/doc/pdg/.gitignore +++ b/doc/pdg/.gitignore @@ -2,8 +2,7 @@ anr-logo.png biblio.bib eu-flag.jpg frama-c-book.cls -frama-c-cover.pdf -frama-c-left.pdf -frama-c-right.pdf -frama-c-affiliation.tex main.pdf +frama-c-guy.png +fc-macros.tex +logos diff --git a/doc/pdg/calls.tex b/doc/pdg/calls.tex index f50ff876f08..4d6db98b032 100644 --- a/doc/pdg/calls.tex +++ b/doc/pdg/calls.tex @@ -44,7 +44,7 @@ Cela permettra en particulier, d'utiliser d'éventuelles propriétés fournies par la suite par l'utilisateur. \begin{exemple} -\begin{tabular}{m{0.35\textwidth} m{0.6\textwidth}} +\begin{tabular}{m{0.35\textwidth} m{0.59\textwidth}} \begin{verbatim} struct {int a; int b; } G; @@ -145,7 +145,7 @@ dans le cas où certains calcul ne dépendent pas de la valeur du paramètre, mais uniquement de sa déclaration. \begin{exemple} -\begin{tabular}{m{5cm} m{\linewidth - 6cm}} +\begin{tabular}{m{5cm} m{\dimexpr\linewidth-6cm}} \begin{verbatim} int g (int a) { G = 2 * a; @@ -203,7 +203,7 @@ Graphe de la fonction \verbtt{f}: \\ Graphe de la fonction \verbtt{g}: \\ -\includegraphics[width=1\textwidth]{call-g} +\includegraphics[width=.9\textwidth]{call-g} \\ Les graphes sont ceux qui sont effectivement produits par l'outil. diff --git a/doc/pdg/ctrl.tex b/doc/pdg/ctrl.tex index a5bbd5d1617..c47244fe31d 100644 --- a/doc/pdg/ctrl.tex +++ b/doc/pdg/ctrl.tex @@ -209,7 +209,7 @@ uniquement les dépendances directes ou d'inclure les dépendances indirectes. indirecte, comme on pouvait s'y attendre, car Z dépend de \n{a}, et Z1 et Z2 dépendent de Z. & -\includegraphics[width=0.3\textwidth]{ctrl-dpds} +\includegraphics[width=4cm]{ctrl-dpds} \end{tabular} \end{exemple} @@ -370,7 +370,7 @@ ou si elles doivent être présentes dans le programme réduit.\\ L'exemple simple suivant, tiré de \cite{Choi94}, met en évidence ce problème~: \begin{exemple} -\begin{tabular}{m{4cm}m{5cm}} +\begin{tabular}{m{5cm}m{5cm}} \begin{clisting} 1 : <entry> 2 : if (Q) goto 5; @@ -381,7 +381,7 @@ L'exemple simple suivant, tiré de \cite{Choi94}, met en évidence ce problème~ 7 : <exit> \end{clisting} & -\includegraphics[width=0.5\textwidth]{ex-goto} +\includegraphics[width=5cm]{ex-goto} \end{tabular} \begin{tabular}{p{5cm} p{7cm}} @@ -484,7 +484,7 @@ Examinons les différents cas~: personne ne dépend donc de \n{g}, \item si \n{l} postdomine \n{s}, \n{s} dépend de \n{g}, ainsi que tous les postdominateurs de \n{s} qui ne postdomine pas \n{l}, - \item si \n{l} ne postdomine pas \n{s}, + \item si \n{l} ne postdomine pas \n{s}, tous les \n{a} qui postdominent \n{s}, mais pas \n{l} ou l'inverse, dépendent de \n{g}. \end{enumerate} @@ -512,7 +512,7 @@ autres points du graphe. Or, comme l'explique très bien \cite{ranganath04new}, cette hypothèse ne tient plus dans les programmes contenant des boucles infinies ou des \verbtt{exit} (ou même des exceptions, mais pour le langage C, nous n'avons pas le problème). -Cet article présente également avec beaucoup de détails +Cet article présente également avec beaucoup de détails différents types de dépendances et des algorithmes pour les calculer, mais il s'avère probablement trop complexe pour ce que l'on souhaite faire.\\ @@ -530,7 +530,7 @@ La question qui se pose est de savoir s'il faut ajouter des dépendances de contrôle sur les instructions qui, potentiellement, ne terminent pas. \begin{exemple} - \begin{tabular}{p{4.5cm}p{\linewidth-5.5cm}} + \begin{tabular}{p{5.5cm}p{\dimexpr\linewidth-6.5cm}} \begin{clisting} while (f(x) > 0) x++; L: y = 3; diff --git a/doc/pdg/intro.tex b/doc/pdg/intro.tex index 8336e2eca54..5df54278615 100644 --- a/doc/pdg/intro.tex +++ b/doc/pdg/intro.tex @@ -44,7 +44,7 @@ Les \indextxtdef{dépendances sur la valeur}{dépendance!valeur} d'une donnée sont les plus intuitives. \begin{exemple} - \begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}} + \begin{tabular}{m{3.5cm}m{\dimexpr\linewidth-4.5cm}} \begin{clisting} x = a + b; \end{clisting} @@ -68,7 +68,7 @@ droite, mais le choix de l'adresse à laquelle on l'écrit peut également dépe de variables qui apparaissent dans la partie gauche. \begin{exemple} -\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}} +\begin{tabular}{m{3.5cm}m{\dimexpr\linewidth-4.5cm}} \begin{clisting} *p = x; \end{clisting} @@ -76,7 +76,7 @@ de variables qui apparaissent dans la partie gauche. Ici, la valeur de la donnée modifiée dépend de \verbtt{x}, mais le choix de la case dans laquelle on la range dépend de \verbtt{p}. En effet, si $p$ pointe sur $a$ ou $b$, c'est soit \verbtt{a} soit \verbtt{b} qui -va être modifié. +va être modifié. \end{tabular} \end{exemple} @@ -88,13 +88,13 @@ Lorsqu'une donnée peut-être modifiée par plusieurs chemins d'exécution, elle dépend des conditions qui permettent de choisir le chemin. \begin{exemple} -\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}} +\begin{tabular}{m{3.5cm}m{\dimexpr\linewidth-4.5cm}} \begin{clisting} -if (c) +if (c) x = a; L : \end{clisting} -& +& La valeur de \verbtt{x} en \verbtt{L} dépend de \verbtt{a}, mais aussi de \verbtt{c}.\\ \end{tabular} \end{exemple} @@ -114,7 +114,7 @@ variables utilisées pour déterminer la case affectée (partie gauche d'une affectation) sont considérées comme des dépendances sur l'adresse. \begin{exemple} -\begin{tabular}{m{3.5cm}m{\linewidth-4.3cm}} +\begin{tabular}{m{4cm}m{\dimexpr\linewidth-5cm}} \begin{clisting} /* 1 */ int x; /* 2 */ int y; diff --git a/doc/pdg/macros_pdg.tex b/doc/pdg/macros_pdg.tex index 8741fa85bf2..b21ad84e67d 100644 --- a/doc/pdg/macros_pdg.tex +++ b/doc/pdg/macros_pdg.tex @@ -2,6 +2,7 @@ \usepackage{tabularx} \usepackage{wasysym} \usepackage{stmaryrd} +\usepackage{makeidx} %------------------------------------------------------------------------------ \newcommand{\setenvclass}[2]{} @@ -39,9 +40,6 @@ \newcommand{\verbtt}[1]{{\small{\tt{#1}}}} %------------------------------------------------------------------------------ % Légende des figures : -\usepackage[hang,small]{caption} -\renewcommand{\captionfont}{\it} -\renewcommand{\captionlabelfont}{\it \bf \small} %\renewcommand{\captionlabeldelim}{ : } %----------------------------------------------- % prend le nom du fichier diff --git a/doc/pdg/main.tex b/doc/pdg/main.tex index c31cbb3dbb6..ad26c54a144 100644 --- a/doc/pdg/main.tex +++ b/doc/pdg/main.tex @@ -1,28 +1,22 @@ -\documentclass[a4paper,11pt,twoside,openright,web,lang=french]{frama-c-book} +\documentclass[lang=french]{frama-c-book} \input{macros_pdg.tex} -\input{./frama-c-affiliation.tex} %============================================================================== + +\title{Greffon PDG} +\subtitle{Calcul de dépendances dans un programme C} +\author{Anne Pacalet et Patrick Baudin} + + +\cclicence{by-sa} +\copyrightstarts{2007} + \begin{document} +\sloppy +\emergencystretch 3em -\coverpage{PDG --- Documentation technique} +\maketitle -\begin{titlepage} -\begin{flushleft} -\includegraphics[height=14mm]{../images/cealistlogo.jpg} -\end{flushleft} -\vfill -\title{Documentation du greffon PDG}{Calcul de dépendances dans un programme C} -\author{Anne Pacalet et Patrick Baudin} -\begin{tabular}{l} - \fcaffiliationfr -\end{tabular} -\vfill -\begin{flushleft} - \textcopyright 2007-2023 CEA LIST - -\end{flushleft} -\end{titlepage} \input{pdg.tex} \end{document} diff --git a/doc/pdg/pdg.tex b/doc/pdg/pdg.tex index 92fca55150b..89b809edb11 100644 --- a/doc/pdg/pdg.tex +++ b/doc/pdg/pdg.tex @@ -3,6 +3,7 @@ \section*{Versions} \begin{small} + Seules les versions Vx.0 sont des documents achevés~; les autres sont à considérer comme des brouillons. -- GitLab