[wookey] update FC's makefile to new version of analysis scripts

case_studies/wookey/loader/GNUmakefile

@@ -6,18 +6,14 @@
 # Improves analysis time, at the cost of extra memory usage
 export FRAMA_C_MEMORY_FOOTPRINT = 8
 #
-# frama-c-path.mk contains variables which are specific to each
+# path.mk contains variables which are specific to each
 # user and should not be versioned, such as the path to the
 # frama-c binaries (e.g. FRAMAC and FRAMAC_GUI).
 # It is an optional include, unnecessary if frama-c is in the PATH
--include frama-c-path.mk
-#
-# FRAMAC_CONFIG is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
-FRAMAC_CONFIG ?= frama-c-config
-#
-# frama-c.mk contains the main rules and targets
--include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk
+-include path.mk
+FRAMAC?=frama-c
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
+
 #
 ###############################################################################
 
@@ -40,20 +36,23 @@ src/arch/socs/stm32f439/soc-rcc.c \
 src/arch/socs/stm32f439/soc-init.c \
 src/arch/socs/stm32f439/soc-gpio.c \
 src/arch/socs/stm32f439/soc-dwt.c \
-specification.h
+specification.h \
 
 EXCLUDE =\
 
+MACHDEP=x86_32
+
 # (Optional) preprocessing flags, usually handled by -json-compilation-database
-CPPFLAGS    +=
+CPPFLAGS    += -Isrc -I../include/generated -I../loader/src/arch/cores/armv7-m/ -I../loader/src/arch/socs/stm32f407/
 
 # (Optional) Frama-C general flags (parsing and kernel)
 FCFLAGS     += \
   -json-compilation-database ./compile_commands.json \
   -kernel-warn-key typing:incompatible-types-call=inactive \
   -kernel-warn-key annot:missing-spec=inactive \
-  -machdep x86_32 -no-frama-c-stdlib \
-  -c11 -no-asm-contracts
+  -no-frama-c-stdlib \
+  -c11 -no-asm-contracts \
+  $(META)
 
 # (Optional) Eva-specific flags
 EVAFLAGS    += \
@@ -89,14 +88,19 @@ META = -meta $(META_FLAGS)
 IMPORT = -acsl-import $(IMPORT_FILE) 
 
 parse: $(MAIN_TARGET).parse
-gen_prove:
-	$(FRAMAC) $(IMPORT) -then $(META) $(ALL_FILES) -then-last -wp $(WP_FLAGS)
-gen:
-	$(FRAMAC) $(IMPORT) -then $(META) $(ALL_FILES) -then-last -ocode $(OUT_FILE) -print
-wp:
+gen_prove: $(MAIN_TARGET).parse
+	$(FRAMAC) -load $^/framac.sav -then-last $(IMPORT) -then-last -wp $(WP_FLAGS)
+gen: $(OUT_FILE)
+
+$(OUT_FILE): $(MAIN_TARGET).parse
+	$(FRAMAC) -load $^/framac.sav -then-last $(IMPORT) -then-last -ocode $(OUT_FILE) -print
+
+wp: $(OUT_FILE)
 	$(FRAMAC) $(OUT_FILE) -wp $(WP_FLAGS)
 
 clean::
 	rm -f $(OUT_FILE)
 	rm -rf .frama-c
 	rm -rf $(MAIN_TARGET).parse
+
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk