diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex index e8ed8ee41390d5190dc379857bb6cb1ffc05b68b..907ae9806ad95e715d0019a620490d640f0a78a3 100644 --- a/doc/developer/changes.tex +++ b/doc/developer/changes.tex @@ -8,8 +8,8 @@ This chapter summarizes the major changes in this documentation between each \section*{\framacversion} \begin{itemize} -\item \textbf{Tutorial}: Update and completion of the Hello plug-in section -along with the ability to generate the plug-in by \texttt{make archives}. +\item \textbf{Tutorial}: Update and complete the Hello plug-in section +along with making it available online. \item \textbf{Testing}: Explain the appropriate way to handle compilation of \texttt{.ml} scripts during tests \item \textbf{Makefiles}: Remove any reference to obsolete diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex index 9fe1c2603ea5428bed744c290b925277fc70c8d8..2484fcdfb4e15a7ab9fdfab1e24cb13ab5edb8e7 100644 --- a/doc/developer/developer.tex +++ b/doc/developer/developer.tex @@ -44,8 +44,8 @@ \vfill \title{Plug-in Development Guide}% {Release \framacversion} -\author{Julien~Signoles with Loïc Correnson, Matthieu Lemerre and Virgile -Prevosto} +\author{Julien~Signoles with Thibaud~Antignac, Loïc~Correnson, Matthieu~Lemerre +and Virgile~Prevosto} \begin{center} CEA LIST, Software Security Laboratory, Saclay,F-91191 \end{center} diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex index e182b1dd80ab07c9fb8c60bd993969e68ad40342..8e0227a4f2b5ee119bb8a49dabbe42bdca27e2ce 100644 --- a/doc/developer/tutorial.tex +++ b/doc/developer/tutorial.tex @@ -508,9 +508,9 @@ presents how to properly test plug-ins. \subsection{Testing your Plug-in}\label{tut2:testing} \index{Plug-in!Testing}\index{Test} -Frama-C supports non-regression testing of plug-ins. This is useful for -non-regression and test-driven development purposes. The tool allowing to -perform the tests is called \ptests\index{Ptests}. +Frama-C supports non-regression testing of plug-ins. This is useful to check +that further plug-in modifications do not introduce new bugs. The tool allowing +to perform the tests is called \ptests\index{Ptests}. To build these tests, the location of the subdirectories containing them must be indicated in the \texttt{Makefile} through the variable @@ -586,7 +586,7 @@ Then, \texttt{Command} shows the executed command for this test case followed by bash pipes to control the dataflow. (Note the \texttt{-hello} option which has been passed to \framac as requested by \texttt{OPT: -hello} in the \texttt{run.config}.) -Two outputs are considered for each tests: +Two outputs are considered as results for each test: an \emph{error} output and a \emph{result} output. These outputs are logged in the two following files: \texttt{./tests/hello/result/hello\_test.err.log} and diff --git a/doc/developer/tutorial/hello/src/run_with_options.ml b/doc/developer/tutorial/hello/src/run_with_options.ml index fa07e2086a54d6887b95770296aa1f087606017c..e3ab8d9b4edda2a252f4855e5a6e27471c6b8d1e 100644 --- a/doc/developer/tutorial/hello/src/run_with_options.ml +++ b/doc/developer/tutorial/hello/src/run_with_options.ml @@ -6,7 +6,7 @@ let run () = Self.result "%s" msg else let chan = open_out filename in - Printf.fprintf chan "%s\n" msg; + Format.fprintf chan "%s@." msg; close_out chan in output_fun "Hello, world!"