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

[wookey] don't use an intermediate file, rely on a loader.meta dir

This looks more like analysis.mk does, and the intermediate file
(as opposed to the intermediate Frama-C state) does not retain the
status of deduced properties
parent 3a2b60b4
No related branches found
No related tags found
No related merge requests found
......@@ -78,36 +78,29 @@ WP_CUSTOM ?=
WP_FLAGS= -wp-par $(CORES) -wp-timeout 20 -wp-no-warn-memory-model -wp-cache update $(WP_CUSTOM)
META_FLAGS= #-meta-keep-proof-files
OUT_FILE= gen.c
IMPORT_FILE = spec-annots.acsl
ALL_FILES = $(filter-out $(EXCLUDE), $(wildcard $(SRCS)))
FRAMAC_EXEC := frama-c
FRAMAC = $(FRAMAC_EXEC) $(FCFLAGS)
META = -meta $(META_FLAGS)
IMPORT = -acsl-import $(IMPORT_FILE)
IMPORT = -acsl-import $(IMPORT_FILE)
parse: $(MAIN_TARGET).parse
gen_prove: $(MAIN_TARGET).parse
$(MAIN_TARGET).meta: $(MAIN_TARGET).parse
mkdir -p $@
$(FRAMAC) -load $^/framac.sav \
-then-on translation -set-project-as-default \
-then $(IMPORT) -then -wp $(WP_FLAGS)
gen: $(OUT_FILE)
$(OUT_FILE): $(MAIN_TARGET).parse
$(FRAMAC) -load $^/framac.sav \
-then-on translation -set-project-as-default \
-then $(IMPORT) -then -ocode $(OUT_FILE) -print
wp: $(OUT_FILE)
$(FRAMAC) $(OUT_FILE) -wp $(WP_FLAGS)
-then $(IMPORT) -then -wp $(WP_FLAGS) \
-then -save $@/framac.sav \
-then -ocode $@/result.c -print \
-then -report-csv $@/result.csv \
| tee $@/framac.log
prove_gui: $(OUT_FILE)
$(FRAMAC_EXEC)-gui $(OUT_FILE) -wp $(WP_FLAGS)
meta: $(MAIN_TARGET).meta
clean::
rm -f $(OUT_FILE)
rm -rf $(MAIN_TARGET).parse
rm -rf $(MAIN_TARGET).meta
include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk
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