Skip to content
Snippets Groups Projects
Commit 9aa9421c authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[devguide] more robust target for checking tutorial

- clean up plugin files generated into lib/plugins after each run
- do not compile in dev mode (tutorial is not targeting a Frama-C dev env)
- ask ptests to abort in case of error, to make errors more visible
parent 77831828
No related branches found
No related tags found
No related merge requests found
...@@ -36,8 +36,14 @@ all: developer.pdf check ...@@ -36,8 +36,14 @@ all: developer.pdf check
FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
.PHONY: clean-tuto
clean-tuto:
$(RM) ../../lib/plugins/META.frama-c-hello ../../lib/plugins/META.frama-c-viewcfg
$(RM) ../../lib/plugins/top/Hello.* ../../lib/plugins/top/Viewcfg.*
# local plugin.cmi (if any) is in conflict with the one of Frama-C # local plugin.cmi (if any) is in conflict with the one of Frama-C
check: $(GENERATED) check: $(GENERATED)
$(MAKE) clean-tuto
$(ECHO) Checking compilation of example scripts $(ECHO) Checking compilation of example scripts
$(FC_BINDIR)/frama-c \ $(FC_BINDIR)/frama-c \
-load-script ./examples/syntactic_check \ -load-script ./examples/syntactic_check \
...@@ -59,10 +65,15 @@ check: $(GENERATED) ...@@ -59,10 +65,15 @@ check: $(GENERATED)
do $(FC_BINDIR)/frama-c -load-script ./tutorial/hello/generated/$$i/hello_world.ml ; \ do $(FC_BINDIR)/frama-c -load-script ./tutorial/hello/generated/$$i/hello_world.ml ; \
done done
$(ECHO) compilation ok $(ECHO) compilation ok
PATH=$(FC_BINDIR):$$PATH; $(MAKE) -C tutorial/hello/generated/with_test $(MAKE) clean-tuto
PATH=$(FC_BINDIR):$$PATH; $(MAKE) -C tutorial/hello/generated/makefile_multiple PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/hello/generated/with_test byte opt tests
PATH=$(FC_BINDIR):$$PATH; $(MAKE) -C tutorial/hello/generated/makefile_single $(MAKE) clean-tuto
PATH=$(FC_BINDIR):$$PATH; $(MAKE) -C tutorial/viewcfg/generated/split PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/hello/generated/makefile_multiple opt
$(MAKE) clean-tuto
PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/hello/generated/makefile_single opt
$(MAKE) clean-tuto
PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/viewcfg/generated/split opt
$(MAKE) clean-tuto
check-all: developer.pdf check-all: developer.pdf
$(MAKE) -C ../.. check-devguide $(MAKE) -C ../.. check-devguide
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment