Commit db4361c7 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

WIP: support for LTest

parent 2a502eab
Pipeline #33081 failed with stage
in 15 seconds
......@@ -3,13 +3,12 @@
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
include ../../prologue-ltest.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
MACHDEP = x86_32
MACHDEP = x86_64
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
......@@ -23,17 +22,24 @@ FCFLAGS += \
## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
-eva \
-eva-no-print \
-eva-no-show-progress \
-eva-msg-key=-initial-state \
-eva-print-callstacks \
-eva-warn-key alarm=inactive \
-no-deps-print \
-no-calldeps-print \
-eva-warn-key garbled-mix \
-from-verbose 0 \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = 2048.eva
# Targets for LTest
include ../../Makefile.ltest
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
2048.parse: \
../2048.c \
$(eval $(call generate-rules,2048,../2048.c))
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
......
# eva is loaded due to 'unroll' annotations
LANNOTFLAGS=-no-autoload-plugins -load-module eva,variadic,postdominators,lannotate -lannot=DUC
RUN_FC=$(FRAMAC) $(FCFLAGS) $(if $(value MACHDEP),-machdep $(MACHDEP),) -cpp-extra-args="$(CPPFLAGS)"
# generate-ltest-rules <prefix> <sources>: generates LTest rules <prefix>_*.txt
# for the given sources
define generate-rules =
$(1)_Candidate_Obj_Gen.txt: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-no-clean-equiv -lannot-no-clean -lannot-log a:$$@
$(1)_M_NA.txt: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-no-clean-equiv -lannot-log a:$$@
$(1)_M_NA_Eq.txt: ../$(1).c
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-log a:$$@
$(1)_M_Eq.txt: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-no-clean -lannot-log a:$$@
$(1)_M_VA.txt: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-no-clean -lannot-no-clean-equiv -lannot-log a:$(1)_Candidate_Obj_Gen.txt
$(RUN_FC) $$(notdir $$(basename $$<))_labels.c $(LOADEVA) $(EVAFLAGS) -luncov-eva -luncov-log a:$$@ || rm $$@
$(1)_M_WP.txt: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-no-clean -lannot-no-clean-equiv -lannot-log a:$(1)_Candidate_Obj_Gen.txt
$(RUN_FC) $$(notdir $$(basename $$<))_labels.c $(LOADWP) -luncov-wp -wp-prover qed -luncov-log a:$$@ || rm $$@
TARGETS+=$(1)_M_NA.txt $(1)_M_NA_Eq.txt $(1)_M_Eq.txt $(1)_M_VA.txt $(1)_M_WP.txt
endef
filter-out-substring = $(foreach v,$(2),$(if $(findstring $(1),$(v)),,$(v)))
ltest: $$(TARGETS)
ltest-nowp: $$(call filter-out-substring,_M_WP.txt,$$(TARGETS))
clean::
rm -f *_labels.c *.labels *.hyperlabels *.txt
......@@ -3,8 +3,7 @@
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
include ../../prologue-ltest.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
......@@ -22,41 +21,26 @@ FCFLAGS += \
## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## Analysis targets (suffixed with .eva)
IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe787.eva
PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
OTHER_TARGETS = cwe190-unsigned.parse
TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS) $(OTHER_TARGETS)
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
cwe20.parse: ../cwe20.c
cwe20-2.parse: ../cwe20-2.c
cwe119.parse: ../cwe119.c
cwe190.parse: ../cwe190.c
cwe416.parse: ../cwe416.c
cwe787.parse: ../cwe787.c
cwe20-precise.parse: ../cwe20.c
cwe20-2-precise.parse: ../cwe20-2.c
cwe119-precise.parse: ../cwe119.c
cwe190-precise.parse: ../cwe190.c
cwe416-precise.parse: ../cwe416.c
cwe787-precise.parse: ../cwe787.c
cwe190-unsigned.parse: ../cwe190-unsigned.c
cwe20-precise.eva: EVAFLAGS +=
cwe20-2-precise.eva: EVAFLAGS += -eva-precision 5
cwe119-precise.eva: EVAFLAGS +=
cwe190-precise.eva: EVAFLAGS +=
cwe416-precise.eva: EVAFLAGS +=
cwe787-precise.eva: EVAFLAGS += -eva-precision 2
cwe190-unsigned.eva: EVAFLAGS += -warn-unsigned-overflow
-eva \
-eva-no-print \
-eva-no-show-progress \
-eva-msg-key=-initial-state \
-eva-print-callstacks \
-eva-warn-key alarm=inactive \
-no-deps-print \
-no-calldeps-print \
-eva-warn-key garbled-mix \
-from-verbose 0 \
# Targets for LTest
include ../../Makefile.ltest
$(eval $(call generate-rules,cwe20,../cwe20.c))
$(eval $(call generate-rules,cwe20-2,../cwe20-2.c))
$(eval $(call generate-rules,cwe119,../cwe119.c))
$(eval $(call generate-rules,cwe190,../cwe190.c))
$(eval $(call generate-rules,cwe416,../cwe416.c))
$(eval $(call generate-rules,cwe787,../cwe787.c))
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
......
# Makefile template prologue for LTest
# Must be in the same directory as path.mk
# Improves analysis time, at the cost of extra memory usage
export FRAMA_C_MEMORY_FOOTPRINT = 8
FRAMAC ?= frama-c
# analysis.mk contains the main rules and targets
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/analysis.mk
# Default target
all: ltest
# List available targets
help::
@echo ""
@echo "LTest targets:"
@echo "$(sort $(TARGETS))"
@echo ""
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment