diff --git a/.gitignore b/.gitignore index 90dbf023094a2487344f8dea65b2d5226897ab97..67d2ecff0864dfc61fb2e2b59b61016e32e78fed 100644 --- a/.gitignore +++ b/.gitignore @@ -125,19 +125,11 @@ _bisect /doc/pdg/call-g.pdf /doc/pdg/compil.ok /doc/pdg/contents_motif.gif -/doc/pdg/ctrl-dpds.eps -/doc/pdg/ctrl-dpds.pdf -/doc/pdg/ex-goto.eps -/doc/pdg/ex-goto.pdf /doc/pdg/exple-call.c -/doc/pdg/goto.eps -/doc/pdg/goto.pdf /doc/pdg/index.html /doc/pdg/logo-inria-sophia.eps /doc/pdg/logo-inria-sophia.pdf /doc/pdg/next_motif.gif -/doc/pdg/pdg-call.eps -/doc/pdg/pdg-call.pdf /doc/pdg/pdg.css /doc/pdg/pdg.dvi /doc/pdg/pdg.haux diff --git a/doc/MakeLaTeXModern b/doc/MakeLaTeXModern index fd5a01480cd307c4ba842623adb17af2f053c32f..2067d82c3aeb8c130d014fa6bc189bfad743f7a1 100644 --- a/doc/MakeLaTeXModern +++ b/doc/MakeLaTeXModern @@ -1,5 +1,5 @@ FRAMAC_DOC_ROOT_DIR?=.. -FRAMAC_MODERN=frama-c-book.cls fc-macros.tex eu-flag.jpg anr-logo.png frama-c-guy.png logos +FRAMAC_MODERN=frama-c-book.cls fc-macros.tex eu-flag.jpg anr-logo.png logos frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls @rm -f $@ @@ -19,12 +19,6 @@ anr-logo.png: $(FRAMAC_DOC_ROOT_DIR)/anr-logo.png @chmod a-w $@ @echo "import $<" -frama-c-guy.png: $(FRAMAC_DOC_ROOT_DIR)/frama-c-guy.png - @rm -f $@ - @cp $< . - @chmod a-w $@ - @echo "import $<" - fc-macros.tex: $(FRAMAC_DOC_ROOT_DIR)/fc-macros.tex @rm -f $@ @cp $< . diff --git a/doc/aorai/.gitignore b/doc/aorai/.gitignore index 06797055f9322042d505be5e932f71611778678f..e2fc89583b75fdbaa8a45ba8af9d4779fc38a79d 100644 --- a/doc/aorai/.gitignore +++ b/doc/aorai/.gitignore @@ -5,5 +5,4 @@ /logos /anr-logo.png /eu-flag.jpg -/frama-c-guy.png /Schemas/example.pdf diff --git a/doc/developer/.gitignore b/doc/developer/.gitignore index 13351af6250bbe72a94cd3cb696bb24ebc74cac3..13fff2e3450d4b314e878a4d3f3dcd841f201649 100644 --- a/doc/developer/.gitignore +++ b/doc/developer/.gitignore @@ -2,7 +2,6 @@ /developer.pdf /eu-flag.jpg /frama-c-book.cls -/frama-c-guy.png /fc-macros.tex /logos /hello_world/ diff --git a/doc/eva/.gitignore b/doc/eva/.gitignore index f0fe5f9ebbe02db28d816333079a6f6102b481b9..29354296e97dd657cfc8f2f71d7d62b9b8d452b9 100644 --- a/doc/eva/.gitignore +++ b/doc/eva/.gitignore @@ -1,6 +1,5 @@ /anr-logo.png /eu-flag.jpg -/frama-c-guy.png /frama-c-book.cls /main.pdf /logos diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls index 33d011f24f924c93e307f0030648ea7c65edd577..8b4212939908fd25efd51404c3016777bc2cbb97 100644 --- a/doc/frama-c-book.cls +++ b/doc/frama-c-book.cls @@ -164,15 +164,6 @@ \thispagestyle{empty} \noindent\includegraphics{logos/frama-c.png} - \tikzfading[name=fade right,left color=transparent!0, right color=transparent!80] - \tikz[remember picture,overlay]{ - \node[inner sep=0pt,anchor=south,yshift=35mm] (named) at (current page.south){ - \includegraphics[width=\paperwidth]{frama-c-guy} - }; - \fill[white,path fading=fade right] - (named.south west) rectangle (named.north east); - } - \vspace{12em} \begin{center} \textbf{\Huge\@title} diff --git a/doc/frama-c-cover.pdf b/doc/frama-c-cover.pdf deleted file mode 100644 index 4e14243c8064ca92d696fd354476dcdb31092895..0000000000000000000000000000000000000000 Binary files a/doc/frama-c-cover.pdf and /dev/null differ diff --git a/doc/frama-c-guy.png b/doc/frama-c-guy.png deleted file mode 100644 index c6515ac3ed7808cb49c4f75f538b4b8a4053627e..0000000000000000000000000000000000000000 Binary files a/doc/frama-c-guy.png and /dev/null differ diff --git a/doc/frama-c-left.pdf b/doc/frama-c-left.pdf deleted file mode 100644 index ddf8888d292539177ab81c1b33d6411edf51c820..0000000000000000000000000000000000000000 Binary files a/doc/frama-c-left.pdf and /dev/null differ diff --git a/doc/frama-c-right.pdf b/doc/frama-c-right.pdf deleted file mode 100644 index db9b236dfdb19d9a6631ec55eee63f431f8d6f0d..0000000000000000000000000000000000000000 Binary files a/doc/frama-c-right.pdf and /dev/null differ diff --git a/doc/metrics/.gitignore b/doc/metrics/.gitignore index f599e2bb6e7bb61c5e5e357463d53e0b949119c5..a51348c397434abe7af3b018702dc72de0260b11 100644 --- a/doc/metrics/.gitignore +++ b/doc/metrics/.gitignore @@ -1,7 +1,6 @@ /anr-logo.png /eu-flag.jpg /frama-c-book.cls -/frama-c-guy.png /metrics.pdf /logos /fc-macros.tex diff --git a/doc/pdg/.gitignore b/doc/pdg/.gitignore index 61b9f639da65a88b24f35bb40bc25521c8dce744..dd3efee121787113a42d6169c13acefbb0c783a0 100644 --- a/doc/pdg/.gitignore +++ b/doc/pdg/.gitignore @@ -3,6 +3,5 @@ biblio.bib eu-flag.jpg frama-c-book.cls main.pdf -frama-c-guy.png fc-macros.tex logos diff --git a/doc/pdg/Makefile b/doc/pdg/Makefile index 25d22aaca5da90c069241475efd4bf75f2d7f99a..087093c38f77ae79507761cb75579f44e4a98142 100644 --- a/doc/pdg/Makefile +++ b/doc/pdg/Makefile @@ -25,14 +25,14 @@ all: main.pdf GENERATED=biblio.bib -GENERATED+=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf +GENERATED+=frama-c-book.cls include ../MakeLaTeXModern DWNLDDIR=../manuals DOCNAME=pdg-documentation-fr.pdf TEST_DIR=../../tests/pdg -BIB_FILE = ../slicing/bib-slicing.bib +BIB_FILE = ../slicing/design-fr/bib-slicing.bib main.bbl : $(BIB_FILE) @echo "=== Fichier .bib plus récent -> effacement du .bbl" rm -f $(SRC).bbl @@ -47,13 +47,9 @@ main.pdf: $(FRAMAC_MODERN) $(BIB_FILE) \ ############################################################################### -GENERATED+=call-f.fig call-g.fig -%.fig : %.dot - dot -Tfig $< > $@ - GENERATED+=call-f.pdf call-g.pdf -%.pdf : %.fig - fig2dev -L pdf $< $@ +%.pdf : %.dot + dot -Tpdf $< > $@ GENERATED+=call-f.dot call-g.dot call-%.dot : $(TEST_DIR)/oracle/call.%.dot diff --git a/doc/pdg/ctrl-dpds.fig b/doc/pdg/ctrl-dpds.fig deleted file mode 100644 index d41477b617f390b1c3fb6fc1f10e5ea6da28a72b..0000000000000000000000000000000000000000 --- a/doc/pdg/ctrl-dpds.fig +++ /dev/null @@ -1,106 +0,0 @@ -#FIG 3.2 -Portrait -Center -Metric -A4 -100.00 -Single --2 -1200 2 -0 32 #ffffff -6 4410 2610 5355 3195 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 4417 2645 5314 2645 5314 3165 4417 3165 4417 2645 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 4417 2645 5314 2645 5314 3165 4417 3165 4417 2645 -4 1 0 0 0 16 17 0.0000 6 180 810 4866 2976 START\001 --6 -6 5715 6210 6120 6795 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 5728 6236 6082 6236 6082 6755 5728 6755 5728 6236 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 5728 6236 6082 6236 6082 6755 5728 6755 5728 6236 -4 1 0 0 0 16 17 0.0000 6 180 165 5905 6566 B\001 --6 -6 7470 4860 7965 5445 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 7488 4889 7960 4889 7960 5409 7488 5409 7488 4889 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 7488 4889 7960 4889 7960 5409 7488 5409 7488 4889 -4 1 0 0 0 16 17 0.0000 6 180 300 7724 5220 S2\001 --6 -6 5715 4860 6120 5445 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 5740 4889 6094 4889 6094 5409 5740 5409 5740 4889 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 5740 4889 6094 4889 6094 5409 5740 5409 5740 4889 -4 1 0 0 0 16 17 0.0000 6 180 150 5917 5220 Z\001 --6 -6 4725 5715 5220 6255 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 4748 5716 5220 5716 5220 6236 4748 6236 4748 5716 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 4748 5716 5220 5716 5220 6236 4748 6236 4748 5716 -4 1 0 0 0 16 17 0.0000 6 180 285 4984 6047 Z1\001 --6 -6 6435 5715 6975 6255 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 6472 5716 6968 5716 6968 6236 6472 6236 6472 5716 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 6472 5716 6968 5716 6968 6236 6472 6236 6472 5716 -4 1 0 0 0 16 17 0.0000 6 180 285 6720 6047 Z2\001 --6 -6 4455 7155 5220 7740 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 4464 7181 5196 7181 5196 7700 4464 7700 4464 7181 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 4464 7181 5196 7181 5196 7700 4464 7700 4464 7181 -4 1 0 0 0 16 17 0.0000 6 180 675 4830 7511 STOP\001 --6 -6 6480 3375 6885 3960 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 6519 3401 6874 3401 6874 3921 6519 3921 6519 3401 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 6519 3401 6874 3401 6874 3921 6519 3921 6519 3401 -4 1 0 0 0 16 17 0.0000 6 180 165 6696 3732 A\001 --6 -6 4725 4185 5220 4725 -2 3 0 1 32 32 0 -1 20 0.000 0 0 0 0 0 5 - 4745 4204 5194 4204 5194 4724 4745 4724 4745 4204 -2 3 0 1 0 0 0 0 -1 0.000 0 0 0 0 0 5 - 4745 4204 5194 4204 5194 4724 4745 4724 4745 4204 -4 1 0 0 0 16 17 0.0000 6 180 300 4970 4535 S1\001 --6 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 5310 2925 6345 2925 6705 3420 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 4500 3150 4275 5445 4680 7200 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 6525 3600 5175 3600 4950 4185 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 6885 3600 7245 3600 7650 4905 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 5175 4455 5625 4455 5895 4905 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 5760 5175 5310 5175 4950 5715 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 6075 5175 6480 5175 6750 5715 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 4950 6210 4995 6390 5715 6615 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 6750 6210 6705 6390 6075 6615 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 7650 5400 7650 6300 5175 7425 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3 - 2 1 1.00 60.00 120.00 - 5850 6750 5850 6975 5175 7290 diff --git a/doc/pdg/ctrl-dpds.pdf b/doc/pdg/ctrl-dpds.pdf new file mode 100644 index 0000000000000000000000000000000000000000..b1445904135b34e10de6d0cf1d442cbb85310c1d Binary files /dev/null and b/doc/pdg/ctrl-dpds.pdf differ diff --git a/doc/pdg/ex-goto.fig b/doc/pdg/ex-goto.fig deleted file mode 100644 index aa846c27d6b2dfef2503555170d7640267570887..0000000000000000000000000000000000000000 --- a/doc/pdg/ex-goto.fig +++ /dev/null @@ -1,113 +0,0 @@ -#FIG 3.2 -Landscape -Center -Metric -A4 -100.00 -Single --2 -1200 2 -6 3195 2160 8010 5130 -6 3195 2385 4950 4950 -6 3195 2385 3780 2790 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 2565 270 180 3465 2565 3735 2745 -4 1 0 50 -1 0 12 0.0000 4 150 390 3465 2610 entry\001 --6 -6 3195 3105 3780 3510 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 3285 270 180 3465 3285 3735 3465 -4 1 0 50 -1 0 12 0.0000 4 135 90 3465 3330 2\001 --6 -6 3195 3825 3780 4230 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 4005 270 180 3465 4005 3735 4185 -4 1 0 50 -1 0 12 0.0000 4 135 90 3465 4050 5\001 --6 -6 4365 3105 4950 3510 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 4635 3285 270 180 4635 3285 4905 3465 -4 1 0 50 -1 0 12 0.0000 4 135 90 4635 3330 3\001 --6 -6 4365 3825 4950 4230 -6 4590 3915 4680 4050 -4 1 0 50 -1 0 12 0.0000 4 135 90 4635 4050 4\001 --6 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 4635 4005 270 180 4635 4005 4905 4185 --6 -6 3195 4545 3780 4950 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 3465 4725 270 180 3465 4725 3735 4905 -4 1 0 50 -1 0 12 0.0000 4 135 90 3465 4770 6\001 --6 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 3465 2745 3465 3105 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 3465 3465 3465 3825 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 3465 4185 3465 4545 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 4635 3465 4635 3825 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 3735 3285 4365 3285 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 4545 4185 3735 4725 --6 -6 5715 2385 7470 4950 -6 5715 2385 6300 2790 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 2565 270 180 5985 2565 6255 2745 -4 1 0 50 -1 0 12 0.0000 4 150 390 5985 2610 entry\001 --6 -6 5715 3105 6300 3510 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 3285 270 180 5985 3285 6255 3465 -4 1 0 50 -1 0 12 0.0000 4 135 90 5985 3330 2\001 --6 -6 5715 3825 6300 4230 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 4005 270 180 5985 4005 6255 4185 -4 1 0 50 -1 0 12 0.0000 4 135 90 5985 4050 5\001 --6 -6 6885 3105 7470 3510 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 7155 3285 270 180 7155 3285 7425 3465 -4 1 0 50 -1 0 12 0.0000 4 135 90 7155 3330 3\001 --6 -6 5715 4545 6300 4950 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 5985 4725 270 180 5985 4725 6255 4905 -4 1 0 50 -1 0 12 0.0000 4 135 90 5985 4770 6\001 --6 -6 6885 3825 7470 4230 -6 7110 3915 7200 4050 -4 1 0 50 -1 0 12 0.0000 4 135 90 7155 4050 4\001 --6 -1 1 0 1 0 7 50 -1 -1 0.000 1 0.0000 7155 4005 270 180 7155 4005 7425 4185 --6 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 5985 2745 5985 3105 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 5985 3465 5985 3825 -2 1 1 2 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 0 0 1.00 60.00 120.00 - 5985 4185 5985 4545 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 6255 3285 6885 3285 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 6255 3285 7155 3825 --6 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 2 1 1.00 60.00 120.00 - 7515 4860 7965 4860 -2 1 1 2 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 0 0 1.00 60.00 120.00 - 7515 5085 7965 5085 -2 1 1 2 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 0 0 1.00 60.00 120.00 - 6975 3375 6255 4725 -4 1 0 50 -1 2 12 0.0000 4 135 375 4365 2295 CFG\001 -4 1 0 50 -1 2 12 0.0000 4 135 390 6885 2295 PDG\001 -4 1 0 50 -1 2 10 0.0000 4 150 675 7065 4860 CDG edge\001 -4 1 0 50 -1 2 10 0.0000 4 150 690 7065 5085 DDG edge\001 --6 diff --git a/doc/pdg/ex-goto.pdf b/doc/pdg/ex-goto.pdf new file mode 100644 index 0000000000000000000000000000000000000000..1d6089fcc03be905850d5ba749a4120c1581c3d8 Binary files /dev/null and b/doc/pdg/ex-goto.pdf differ diff --git a/doc/pdg/goto.fig b/doc/pdg/goto.fig deleted file mode 100644 index ac14cc5a0d07c360da3514b4e19bb0a49bfe7832..0000000000000000000000000000000000000000 --- a/doc/pdg/goto.fig +++ /dev/null @@ -1,35 +0,0 @@ -#FIG 3.2 -Portrait -Center -Metric -A4 -100.000000 -Single --2 -1200 2 -0 32 #ffffff -6 0 0 0 0 -1 1 0 1 32 32 0 0 20 0.000000 1 0.0 5722 1299 767 472 0 0 0 0 -1 1 0 1 0 -1 0 0 -1 0.000000 1 0.0 5722 1299 767 472 0 0 0 0 -4 1 0 0 0 16 22.762205 0.0 6 0.0 0.0 5722 1393 G\001 --6 -6 0 0 0 0 -1 1 0 1 32 32 0 0 20 0.000000 1 0.0 5090 3622 767 472 0 0 0 0 -1 1 0 1 0 -1 0 0 -1 0.000000 1 0.0 5090 3622 767 472 0 0 0 0 -4 1 0 0 0 16 22.762205 0.0 6 0.0 0.0 5090 3716 S\001 --6 -6 0 0 0 0 -2 1 0 1 0 0 0 0 -1 0.000000 0 0 0 1 0 4 - 0 0 3.149606 236.220472 236.220472 - 6490 1299 6962 1299 6962 5756 6490 5756 --6 -6 0 0 0 0 -1 1 0 1 32 32 0 0 20 0.000000 1 0.0 5722 5756 767 472 0 0 0 0 -1 1 0 1 0 -1 0 0 -1 0.000000 1 0.0 5722 5756 767 472 0 0 0 0 -4 1 0 0 0 16 22.762205 0.0 6 0.0 0.0 5722 5851 L\001 --6 -6 0 0 0 0 -2 1 1 1 0 0 0 0 -1 12.598425 0 0 0 1 0 4 - 0 0 3.149606 236.220472 377.952756 - 5722 1771 5722 2460 5090 2460 5090 3149 --6 diff --git a/doc/pdg/goto.pdf b/doc/pdg/goto.pdf new file mode 100644 index 0000000000000000000000000000000000000000..c037ad942ec65e75ef0cef8d92d8589169d5349f Binary files /dev/null and b/doc/pdg/goto.pdf differ diff --git a/doc/pdg/pdg-call.fig b/doc/pdg/pdg-call.fig deleted file mode 100644 index f55a683a25f4ca4cd7ef67f8bd4c8f96db2e0eaf..0000000000000000000000000000000000000000 --- a/doc/pdg/pdg-call.fig +++ /dev/null @@ -1,151 +0,0 @@ -#FIG 3.2 -Landscape -Center -Metric -A4 -100.00 -Single --2 -1200 2 -6 7830 3330 8820 3780 -2 3 0 1 0 7 50 -1 -1 4.000 0 0 0 0 0 7 - 8190 3702 8301 3534 8211 3354 8010 3342 7899 3510 7989 3690 - 8190 3702 -2 3 0 1 0 7 50 -1 -1 4.000 0 0 0 0 0 7 - 8640 3690 8751 3522 8661 3342 8460 3330 8349 3498 8439 3678 - 8640 3690 -4 1 0 50 -1 0 12 0.0000 4 135 150 8100 3600 f0\001 -4 1 0 50 -1 0 12 0.0000 4 135 150 8550 3600 f1\001 --6 -6 7650 2880 8010 3150 -2 2 0 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 5 - 7650 2880 8010 2880 8010 3150 7650 3150 7650 2880 -4 1 0 50 -1 0 12 0.0000 4 90 90 7830 3060 a\001 --6 -6 8550 2880 8910 3150 -2 2 0 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 5 - 8550 2880 8910 2880 8910 3150 8550 3150 8550 2880 -4 1 0 50 -1 0 12 0.0000 4 135 90 8730 3060 b\001 --6 -6 8190 1440 8730 1980 -1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 8460 1710 180 180 8460 1890 8460 1530 -4 1 0 50 -1 0 12 0.0000 4 135 135 8460 1800 G\001 --6 -6 8550 2340 9090 2790 -1 2 0 1 0 7 50 -1 -1 4.000 1 0.0000 8820 2565 180 135 8640 2430 9000 2700 -4 1 0 50 -1 0 12 0.0000 4 90 90 8820 2610 z\001 --6 -6 7380 2340 8010 2790 -1 2 0 1 0 7 50 -1 -1 4.000 1 0.0000 7695 2565 225 135 7470 2430 7920 2700 -4 1 0 50 -1 0 12 0.0000 4 135 330 7740 2610 x+y \001 --6 -6 7290 1800 7650 2250 -1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 7470 2025 135 135 7470 2160 7470 1890 -4 1 0 50 -1 0 12 0.0000 4 90 90 7470 2070 x\001 --6 -6 7740 1800 8100 2250 -1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 7920 2025 135 135 7920 2160 7920 1890 -4 1 0 50 -1 0 12 0.0000 4 135 90 7920 2070 y\001 --6 -6 7650 3780 8010 4230 -1 4 0 1 0 7 50 -1 -1 4.000 1 0.0000 7830 4005 135 135 7830 4140 7830 3870 -4 1 0 50 -1 0 12 0.0000 4 90 90 7830 4050 z\001 --6 -6 4770 1620 6390 3870 -6 4860 1800 5220 2790 -2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 - 4860 1800 5220 1800 5220 2070 4860 2070 4860 1800 -2 3 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 - 4860 2430 5220 2430 5040 2790 4860 2430 4860 2430 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 5040 2070 5040 2430 -4 1 0 50 -1 0 12 0.0000 4 90 90 5040 1980 a\001 -4 1 0 50 -1 0 12 0.0000 4 90 90 5040 2610 a\001 --6 -6 5400 1800 5760 2790 -2 2 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 - 5400 1800 5760 1800 5760 2070 5400 2070 5400 1800 -2 3 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 - 5400 2430 5760 2430 5580 2790 5400 2430 5400 2430 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 5580 2070 5580 2430 -4 1 0 50 -1 0 12 0.0000 4 135 90 5580 2610 b\001 -4 1 0 50 -1 0 12 0.0000 4 135 90 5580 1980 b\001 --6 -6 5940 2430 6300 2790 -2 3 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 5 - 5940 2430 6300 2430 6120 2790 5940 2430 5940 2430 -4 1 0 50 -1 0 12 0.0000 4 135 135 6120 2610 G\001 --6 -2 4 0 1 0 7 50 -1 -1 0.000 0 0 7 0 0 5 - 6390 3870 6390 1620 4770 1620 4770 3870 6390 3870 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 6030 1620 6390 1980 -2 3 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 7 - 5490 3780 5601 3612 5511 3432 5310 3420 5199 3588 5289 3768 - 5490 3780 -2 3 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 7 - 6051 3780 6162 3612 6072 3432 5871 3420 5760 3588 5850 3768 - 6051 3780 -3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3 - 6120 2790 6210 3240 6030 3420 - 0.000 1.000 0.000 -3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3 - 5580 2790 5400 3060 5940 3420 - 0.000 1.000 0.000 -3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3 - 6120 2790 5940 3060 5490 3420 - 0.000 1.000 0.000 -3 0 2 2 0 7 50 -1 -1 4.500 0 0 0 3 - 5040 2790 4950 3150 5310 3420 - 0.000 1.000 0.000 -4 0 0 50 -1 0 12 0.0000 4 135 60 6210 1800 f\001 -4 1 0 50 -1 0 12 0.0000 4 135 90 5400 3690 0\001 -4 1 0 50 -1 0 12 0.0000 4 135 90 5940 3690 1\001 --6 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 7830 3150 8010 3330 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 8730 3150 8640 3330 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 8820 2700 8730 2880 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 7740 2700 7830 2880 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 8370 1890 8190 3330 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 8460 1890 8460 3330 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 7560 2160 7650 2430 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 7830 2160 7740 2430 -2 4 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 5 - 9180 3780 9180 2340 7290 2340 7290 3780 9180 3780 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 8100 3690 7920 3870 -2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 8550 3690 8730 4050 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 9270 1800 8820 1350 -2 4 0 1 0 7 50 -1 -1 4.000 0 0 7 0 0 5 - 9270 4500 9270 1350 7200 1350 7200 4500 9270 4500 -4 1 0 50 -1 0 12 0.0000 4 135 90 9090 1530 g\001 -4 1 0 50 -1 14 12 0.0000 4 180 1365 8370 1170 z = f(x+y,z);\001 -4 1 0 50 -1 0 12 0.0000 4 135 1245 4050 2610 Valeurs initiales\001 -4 1 0 50 -1 0 12 0.0000 4 135 975 4050 1980 D\351clarations\001 -4 1 0 50 -1 0 12 0.0000 4 135 540 4050 3690 Sorties\001 -4 1 0 50 -1 14 12 0.0000 4 165 1890 5580 1350 T1 f (T2 a, T3 b);\001 -4 1 0 50 -1 3 12 0.0000 4 150 1845 5580 4140 \\res From a , G.a, G.b;\001 -4 1 0 50 -1 3 12 0.0000 4 150 1050 5580 4410 G From b, G;\001 diff --git a/doc/pdg/pdg-call.pdf b/doc/pdg/pdg-call.pdf new file mode 100644 index 0000000000000000000000000000000000000000..178242b9e3a531020cfb94705e7e6c7a48f704b7 Binary files /dev/null and b/doc/pdg/pdg-call.pdf differ diff --git a/doc/pdg/pdg.tex b/doc/pdg/pdg.tex index 89b809edb11071f1c881b77e41fd6102a6e4cdf3..a1b7e43b88be91bfe61bb5f7bccd354770bf0cce 100644 --- a/doc/pdg/pdg.tex +++ b/doc/pdg/pdg.tex @@ -72,7 +72,7 @@ les autres sont à considérer comme des brouillons. %------------------------------------------------------------------------------- \cleardoublepage \bibliographystyle{abbrvnat} -\bibliography{../slicing/bib-slicing} +\bibliography{../slicing/design-fr/bib-slicing} %-------------------------------------- \cleardoublepage \printindex diff --git a/doc/release/.gitignore b/doc/release/.gitignore index 46cb0ea4796b3412350bfc6ae30a833dce3395d0..83a46ab116d3bf74b6080246fd061f79d54ad03f 100644 --- a/doc/release/.gitignore +++ b/doc/release/.gitignore @@ -4,4 +4,3 @@ /release.pdf /fc-macros.tex /logos -/frama-c-guy.png diff --git a/doc/rte/.gitignore b/doc/rte/.gitignore index 6ed782f7635f8c1e42ad04c22f3c776d4d8593f8..89a70250372e530d5e08302ff1de19d4cca9e839 100644 --- a/doc/rte/.gitignore +++ b/doc/rte/.gitignore @@ -5,4 +5,3 @@ /fc-macros.tex /logos /main.pdf -/frama-c-guy.png diff --git a/doc/slicing/design-fr/.gitignore b/doc/slicing/design-fr/.gitignore index 79c73e1bf2c9935341dde60db4efaa2855c7df3f..3371ae40ab88908a2d52fabbea364d7804434f53 100644 --- a/doc/slicing/design-fr/.gitignore +++ b/doc/slicing/design-fr/.gitignore @@ -9,7 +9,6 @@ /propagation.pdf /fc-macros.tex /logos -/frama-c-guy.png /main.aux /main.bbl /main.blg diff --git a/doc/slicing/design-fr/Makefile b/doc/slicing/design-fr/Makefile index efdaaf5991d98888477a046b3df91a14815f45fe..5ff50d1a0d10dc3c1b153abb9289c796f3f4d80b 100644 --- a/doc/slicing/design-fr/Makefile +++ b/doc/slicing/design-fr/Makefile @@ -25,7 +25,7 @@ all: main.pdf GENERATED=biblio.bib -GENERATED+=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf +GENERATED+=frama-c-book.cls FRAMAC_DOC_ROOT_DIR=../.. include $(FRAMAC_DOC_ROOT_DIR)/MakeLaTeXModern diff --git a/doc/slicing/user-manual-fr/.gitignore b/doc/slicing/user-manual-fr/.gitignore index ec3b9d5b447c1f1c891710a66a5c7da4050248c5..71cfd07ca8d6a1b28313ca3140937e4634567df4 100644 --- a/doc/slicing/user-manual-fr/.gitignore +++ b/doc/slicing/user-manual-fr/.gitignore @@ -4,7 +4,6 @@ /main.pdf /fc-macros.tex /logos -/frama-c-guy.png /main.aux /main.bbl /main.blg diff --git a/doc/slicing/user-manual-fr/Makefile b/doc/slicing/user-manual-fr/Makefile index 961cbb535f1a7d2628583d39ceeca7134e9b8757..2142f0c5ed496d57c5b7228506a1e63c09b6397a 100644 --- a/doc/slicing/user-manual-fr/Makefile +++ b/doc/slicing/user-manual-fr/Makefile @@ -25,7 +25,7 @@ all: main.pdf GENERATED= -GENERATED+=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf +GENERATED+=frama-c-book.cls FRAMAC_DOC_ROOT_DIR=../.. include $(FRAMAC_DOC_ROOT_DIR)/MakeLaTeXModern diff --git a/doc/userman/.gitignore b/doc/userman/.gitignore index 53489defd39f6961c7f5681f6e39462bc711a7a5..68d73f9e795bab5c3388735d975f1ab8a70c44c6 100644 --- a/doc/userman/.gitignore +++ b/doc/userman/.gitignore @@ -6,4 +6,3 @@ logos userman.idx userman.out userman.pdf -frama-c-guy.png diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore index cf93cfc14764d31ce92f0d2d1e0a15ec5b620244..2c3409db1fc39937576225fbc8ddd29fbde3e20c 100644 --- a/src/plugins/e-acsl/doc/refman/.gitignore +++ b/src/plugins/e-acsl/doc/refman/.gitignore @@ -7,4 +7,3 @@ fc-macros.tex logos *.fls *.fdb_latexmk -frama-c-guy.png diff --git a/src/plugins/e-acsl/doc/userman/.gitignore b/src/plugins/e-acsl/doc/userman/.gitignore index a06c223d2a6bb7ebf1efb63de47b1500b42db862..ec39318db7154382195f9c8c4372ff568b6c2c28 100644 --- a/src/plugins/e-acsl/doc/userman/.gitignore +++ b/src/plugins/e-acsl/doc/userman/.gitignore @@ -1,13 +1,9 @@ anr-logo.png 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 fc-macros.tex logos *.fls *.fdb_latexmk -frama-c-guy.png diff --git a/src/plugins/wp/doc/.gitignore b/src/plugins/wp/doc/.gitignore index 29d54294ae4a45e38bb133101ea89df7ff91d4dc..bfe2e4d25500d764b549b9e6dfd00ae71d137617 100644 --- a/src/plugins/wp/doc/.gitignore +++ b/src/plugins/wp/doc/.gitignore @@ -1,7 +1,4 @@ frama-c-book.cls -frama-c-cover.pdf -frama-c-left.pdf -frama-c-right.pdf frama-c-affiliation.tex cealistlogo.jpg feedback diff --git a/src/plugins/wp/doc/MakeDoc b/src/plugins/wp/doc/MakeDoc index 5c8ff34ce3d7d4e901e89ba5ddeed864a0b330af..18ff334ec7d37ed8df6f489835c62d033129c3df 100644 --- a/src/plugins/wp/doc/MakeDoc +++ b/src/plugins/wp/doc/MakeDoc @@ -25,7 +25,7 @@ # -------------------------------------------------------------------------- FRAMAC_DOC= .make-class .make-images .make-icons VERSION VERSION_CODENAME # -------------------------------------------------------------------------- -FRAMAC_CLASS=frama-c-book.cls fc-macros.tex logos anr-logo.png frama-c-guy.png +FRAMAC_CLASS=frama-c-book.cls fc-macros.tex logos anr-logo.png FRAMAC_BULLETS=never_tried.png unknown.png valid_under_hyp.png surely_valid.png FRAMAC_IMAGES=cealistlogo.jpg # -------------------------------------------------------------------------- diff --git a/src/plugins/wp/doc/manual/.gitignore b/src/plugins/wp/doc/manual/.gitignore index 42ebb7187bdffd9b76dbf84d347b1a46fe518073..ae43a86a634148a0a0314d6b19a1bf951803dae7 100644 --- a/src/plugins/wp/doc/manual/.gitignore +++ b/src/plugins/wp/doc/manual/.gitignore @@ -9,4 +9,3 @@ /macros.tex /anr-logo.png /fc-macros.tex -/frama-c-guy.png