diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 1dc23e29441d9800afd829ce47e35968df45db79..49e246def29f97011ea115817f52d9963ac082d7 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -192,16 +192,13 @@ Note that \verb|camlp5| is not among the dependencies declared in Since the adoption of Dune, \framac's \texttt{Makefile}s were largely simplified. They are still used for some tasks, partially due to conciseness (\verb|make| is shorter than \verb|dune build|), partially because some tasks -are better suited for them. +are better suited for them. Some standards targets are defined in various +Makefiles that are installed in \framac's shared directory. -Plug-in developers usually just need to copy and paste the existing Makefile -template and rename the opam file name (\verb|frama-c-<plugin>.opam|). +A minimal plugin's \verb|Makefile| can thus be the following: -This Makefile reuses code from other Makefiles, distributed in Frama-C's -{\em share} directory, such as \verb|Makefile.testing|, -\verb|Makefile.installation|, etc. Their names indicate the kinds of features -they provide. Many are shortcuts for specific dune targets, but they also -provide linting and copyright headers-related features. +\listingname{Makefile} +\makeinput{./tutorial/hello/src/Makefile} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/doc/developer/tutorial/hello/src/Makefile b/doc/developer/tutorial/hello/src/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..61d832e1315f7b9b5e6db9ab2fce266c26aea87b --- /dev/null +++ b/doc/developer/tutorial/hello/src/Makefile @@ -0,0 +1,16 @@ +FRAMAC_SHARE:=$(shell frama-c -print-share-path) + +sinclude ${FRAMAC_SHARE}/Makefile.common + +########################################################################## + +# Tests + +include ${FRAMAC_SHARE}/Makefile.testing + +########################################################################## + +# Install + +include ${FRAMAC_SHARE}/Makefile.installation + diff --git a/doc/developer/tutorial/hello/src/Makefile.test b/doc/developer/tutorial/hello/src/Makefile.test deleted file mode 100644 index 7ff38b3f00bd36c277dd4f889afb323b8ceeec55..0000000000000000000000000000000000000000 --- a/doc/developer/tutorial/hello/src/Makefile.test +++ /dev/null @@ -1,27 +0,0 @@ -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# CEA (Commissariat à l'énergie atomique et aux énergies # -# 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). # -# # -########################################################################## - -FRAMAC_SHARE := $(shell frama-c-config -print-share-path) -PLUGIN_NAME = Hello -PLUGIN_CMO = hello_options hello_print hello_run -PLUGIN_TESTS_DIRS := hello -include $(FRAMAC_SHARE)/Makefile.dynamic diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls index cb6f16df585f0055b0b0148fd16f6fd2b68d9daa..532f4dbfe195a431caee09d1893dee36a612cbfa 100644 --- a/doc/frama-c-book.cls +++ b/doc/frama-c-book.cls @@ -391,10 +391,18 @@ literate=% basicstyle=\lp@inline,% } +\lstdefinestyle{make-basic}{% + language=Makefile,% + style=framac-code-style,% + basicstyle=\lp@inline,% +} + \newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}} \lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{} \newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}} \lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{} +\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}} +\lstnewenvironment{makecode}[1][]{\lstset{style=make-basic,#1}}{} % -------------------------------------------------------------------------- \lstdefinelanguage{Why}{% morekeywords={