From bb79d5eb914a1fa227ef4026b79531da87658fa8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 28 Sep 2022 18:20:18 +0200
Subject: [PATCH] [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
---
case_studies/wookey/loader/GNUmakefile | 27 ++++++++++----------------
1 file changed, 10 insertions(+), 17 deletions(-)
diff --git a/case_studies/wookey/loader/GNUmakefile b/case_studies/wookey/loader/GNUmakefile
index 35c5c48..937c27b 100644
--- a/case_studies/wookey/loader/GNUmakefile
+++ b/case_studies/wookey/loader/GNUmakefile
@@ -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
--
GitLab