diff --git a/doc/developer/Makefile b/doc/developer/Makefile index 0014db943d275e9b3ba4e805b4b129e5fd34b4a1..5af8def8a595a7c9824fe960aa03466ab56272b8 100644 --- a/doc/developer/Makefile +++ b/doc/developer/Makefile @@ -85,8 +85,7 @@ examples/generated/%.ml: examples/%.ml headache -r $@ archives: tutorial/hello/generated - cd tutorial/hello/generated/with_doc/; \ - tar -zcvf ../../../../hello.tar.gz * + cd tutorial/hello/generated/with_doc/ && tar -zcvf ../../../../hello.tar.gz * .PHONY: tutorial/hello/generated tutorial/viewcfg/generated diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex index d7c6431db9635f4cb969b4b36ebbabb49b6f6da5..76223c6ba9dee876603569a18ce7692ff5868d33 100644 --- a/doc/developer/tutorial.tex +++ b/doc/developer/tutorial.tex @@ -287,7 +287,7 @@ Visible results of the registration include: \begin{itemize} \item ``hello world'' appears in the list of available plug-ins (consultable with \texttt{frama-c -load-script - hello\_world.ml -help}); + hello\_world.ml -plugins}); \item default options for the plug-in work, including the inline help (available with \texttt{frama-c -load-script hello\_world.ml -hello-help}). diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile index 8c4ab461ad429d8713ecce004ca30a502fa06955..a4bad5fdb21cb7ffacf5e0eb13351a2436f212ab 100644 --- a/doc/developer/tutorial/hello/Makefile +++ b/doc/developer/tutorial/hello/Makefile @@ -33,6 +33,10 @@ generated/src/tests/hello/%.c: src/%.c cp $< $@ headache -r $< +generated/src/tests/hello/oracle/%.oracle: src/%.oracle + mkdir -p $(dir $@) + cp $< $@ + generated/%/Hello.mli: src/Hello.mli mkdir -p $(dir $@) cp $< $@ @@ -129,6 +133,8 @@ generated/with_doc: generated/src/help_msg.ml \ generated/src/hello_options.doc.ml \ generated/src/hello_print.doc.ml \ generated/src/hello_run.doc.ml \ + generated/src/tests/hello/oracle/hello_test.err.oracle \ + generated/src/tests/hello/oracle/hello_test.res.oracle \ generated/src/Makefile.test mkdir -p $@ cp generated/src/hello_options.doc.ml $@/hello_options.ml @@ -157,6 +163,9 @@ generated/with_doc: generated/src/help_msg.ml \ cat generated/src/extend_run.ml >> $@/hello_run.ml mkdir -p $@/tests/hello cp generated/src/tests/hello/hello_test.c $@/tests/hello/hello_test.c + mkdir -p $@/tests/hello/oracle + cp generated/src/tests/hello/oracle/hello_test.err.oracle $@/tests/hello/oracle/hello_test.err.oracle + cp generated/src/tests/hello/oracle/hello_test.res.oracle $@/tests/hello/oracle/hello_test.res.oracle cp generated/src/Makefile.test $@/Makefile tests: diff --git a/doc/developer/tutorial/hello/src/hello_test.err.oracle b/doc/developer/tutorial/hello/src/hello_test.err.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/doc/developer/tutorial/hello/src/hello_test.res.oracle b/doc/developer/tutorial/hello/src/hello_test.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..9f5bbff5c8f9930dcce578590a2418b8ce453665 --- /dev/null +++ b/doc/developer/tutorial/hello/src/hello_test.res.oracle @@ -0,0 +1,3 @@ +[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) +[kernel] Parsing tests/hello/hello_test.c (with preprocessing) +[hello] Hello, world! diff --git a/doc/developer/tutorial/hello/src/print.ml b/doc/developer/tutorial/hello/src/print.ml index 585498d13649bc6851a35d05a977145516ef81b2..66b338c1642fb16cc4b4a76afcdd906a4f6af6d8 100644 --- a/doc/developer/tutorial/hello/src/print.ml +++ b/doc/developer/tutorial/hello/src/print.ml @@ -8,7 +8,6 @@ let output msg = Printf.fprintf chan "%s\n" msg; flush chan; close_out chan - with exc -> - let msg = Printexc.to_string exc in - Printf.eprintf "There was an error: %s\n" msg; - raise exc + with Sys_error e -> + let msg = Printexc.to_string (Sys_error e) in + Printf.eprintf "There was an error: %s\n" msg diff --git a/doc/developer/tutorial/hello/src/run_print_to_file.ml b/doc/developer/tutorial/hello/src/run_print_to_file.ml index ae9f3c389835528a14e15113fc421860450a1202..9392afe31db56a24add4cacc86f64638d2680bc3 100644 --- a/doc/developer/tutorial/hello/src/run_print_to_file.ml +++ b/doc/developer/tutorial/hello/src/run_print_to_file.ml @@ -4,7 +4,6 @@ let run () = Printf.fprintf chan "Hello, world!\n"; flush chan; close_out chan - with exc -> - let msg = Printexc.to_string exc in - Printf.eprintf "There was an error: %s\n" msg; - raise exc + with Sys_error e -> + let msg = Printexc.to_string (Sys_error e) in + Printf.eprintf "There was an error: %s\n" msg diff --git a/doc/developer/tutorial/hello/src/run_with_options.ml b/doc/developer/tutorial/hello/src/run_with_options.ml index 79d9c8cb39146ea7617a1fa2c5ecb794af12cf1f..996503022e5ea46b3ee99a931899d4d70528e7bc 100644 --- a/doc/developer/tutorial/hello/src/run_with_options.ml +++ b/doc/developer/tutorial/hello/src/run_with_options.ml @@ -12,7 +12,6 @@ let run () = close_out chan; in output "Hello, world!" - with exc -> - let msg = Printexc.to_string exc in - Printf.eprintf "There was an error: %s\n" msg; - raise exc + with Sys_error e -> + let msg = Printexc.to_string (Sys_error e) in + Printf.eprintf "There was an error: %s\n" msg