diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 6cae8c5de9a412065c851c1594126c1f7eef65e1..d447287224411cd8161e2c84c8482ca47e0c4dd9 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -200,6 +200,24 @@ A minimal plugin's \verb|Makefile| can thus be the following: \listingname{Makefile} \makeinput{./tutorial/hello/src/Makefile} +\texttt{Makefile.testing} introduces various targets related to \framac's +testing infrastructure (see Section~\ref{adv:ptests}). This includes notably +\texttt{tests} to run all the tests of the plugin, after having taken care of +generating the corresponding \texttt{dune} files. + +\texttt{Makefile.installation} provides two targets, \texttt{install} and +\texttt{uninstall}. By default, installation will occur in the current +\texttt{opam} switch, but this can be modified by using the \texttt{PREFIX} +variable (note that if you install your plugin in a non-default place, you will +have to explicitly instruct \framac to load it through option +\texttt{-load-plugin}. + +Other Makefiles include \texttt{Makefile.documentation}, providing the +\texttt{doc} for generating the documentation (see Section~\ref{tut2:doc}), +and \texttt{Makefile.headers} and \texttt{Makefile.linting} which are used +by \framac itself to manage headers and perform various syntactic checks +(though, of course, you can reuse them at will). + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Testing}\label{adv:ptests}\index{Test|bfit} diff --git a/doc/developer/tutorial/hello/src/Makefile b/doc/developer/tutorial/hello/src/Makefile index 5c30410ff80d2b9977ae3b0b20d9bca11f39bc71..bfdef3c8367de27c5ec3c892320c60444ead1574 100644 --- a/doc/developer/tutorial/hello/src/Makefile +++ b/doc/developer/tutorial/hello/src/Makefile @@ -1,16 +1,13 @@ FRAMAC_SHARE:=$(shell frama-c-config -print-share-path) -sinclude ${FRAMAC_SHARE}/Makefile.common +## Common definitions -########################################################################## +include ${FRAMAC_SHARE}/Makefile.common -# Tests +## Tests-related targets include ${FRAMAC_SHARE}/Makefile.testing -########################################################################## - -# Install +## Installation-related targets include ${FRAMAC_SHARE}/Makefile.installation -