Commit 3ac423f1 authored by Andre Maroneze's avatar Andre Maroneze Committed by Andre Maroneze
Browse files

use new Makefile structure

parent 4ef431af
......@@ -2,7 +2,6 @@
*.sav
*.o
*~
.frama-c
config.status
lia.cache
......@@ -13,9 +12,6 @@ eva.log
stats.txt
flamegraph.txt
# ignore timestamped versions
*_20*-*.eva
*_20*-*.parse
*.error
benchs-value.csv
......
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -scripts)/prologue.mk
###############################################################################
# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
MACHDEP = x86_32
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
-CC
## General flags
FCFLAGS += \
-add-symbolic-path=.:.. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:.. \
## Analysis targets (suffixed with .eva)
TARGETS = 2048.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
2048.parse: \
../2048.c \
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
###############################################################################
# optional, for OSCS
-include ../../Makefile.common
../../path.mk
\ No newline at end of file
# TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
# DO NOT EDIT THE LINES BETWEEN THE '#'S
###############################################################################
# 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
# 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
#
###############################################################################
# EDIT VARIABLES AND TARGETS BELOW AS NEEDED
# The flags below are only suggestions to use with Eva, and can be removed
# (Optional) preprocessing flags, usually handled by -json-compilation-database
CPPFLAGS += -CC
# (Optional) Frama-C general flags (parsing and kernel)
FCFLAGS += \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
# (Optional) Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
# (MANDATORY) Name of the main target
MAIN_TARGET := 2048
# Add other targets if needed
TARGETS = $(MAIN_TARGET).eva
# Default target
all: $(TARGETS)
help:
@echo "targets: $(TARGETS)"
display-targets:
@echo "$(TARGETS)"
# (MANDATORY) List of source files used by MAIN_TARGET.
# If there is a JSON compilation database,
# 'frama-c-script list-files' can help obtain it
$(MAIN_TARGET).parse: 2048.c
# The following targets are optional and provided for convenience only
parse: $(TARGETS:%.eva=%.parse)
gui: $(MAIN_TARGET).eva.gui
stats: $(TARGETS:%.eva=%.parse) $(TARGETS)
../show_stats.sh "$(notdir $(CURDIR))" $^
# optional, for OSCS
-include ../Makefile.common
../frama-c-path.mk
\ No newline at end of file
......@@ -86,29 +86,29 @@ QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGET
all: $(TARGETS)
$(TARGETS):
+$(MAKE) -C $@
+$(MAKE) -C $@/.frama-c
quick: $(QUICK_TARGETS)
%.clean:
$(MAKE) -C $* clean
$(MAKE) -C $*/.frama-c clean
clean: $(addsuffix .clean,$(TARGETS))
%.parse:
$(MAKE) -C $* parse
$(MAKE) -C $*/.frama-c parse
parse: $(addsuffix .parse,$(TARGETS))
%.stats:
$(MAKE) -C $* stats
$(MAKE) -C $*/.frama-c stats
stats: $(addsuffix .stats,$(TARGETS))
display-targets:
@echo $(foreach target,$(TARGETS),\
$(addprefix $(target)/,\
$(shell $(MAKE) --quiet -C $(target) display-targets)))
$(shell $(MAKE) --quiet -C $(target)/.frama-c display-targets)))
.PHONY: $(TARGETS) frama-c/build/bin/frama-c clean-all help stats-all
......
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -scripts)/prologue.mk
###############################################################################
# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
MACHDEP = x86_32
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=.:.. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
# (Optional) Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## Analysis targets (suffixed with .eva)
IMPRECISE_TARGETS = cwe20.eva cwe119.eva cwe190.eva cwe416.eva cwe787.eva
PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS)
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
cwe20.parse: ../cwe20.c
cwe119.parse: ../cwe119.c
cwe190.parse: ../cwe190.c
cwe416.parse: ../cwe416.c
cwe787.parse: ../cwe787.c
cwe20-precise.parse: ../cwe20.c
cwe119-precise.parse: ../cwe119.c
cwe190-precise.parse: ../cwe190.c
cwe416-precise.parse: ../cwe416.c
cwe787-precise.parse: ../cwe787.c
cwe20-precise.eva: EVAFLAGS +=
cwe119-precise.eva: EVAFLAGS += -eva-precision 1
cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow -eva-no-alloc-returns-null
cwe416-precise.eva: EVAFLAGS += -eva-precision 1
cwe787-precise.eva: EVAFLAGS += -eva-precision 2 -eva-no-alloc-returns-null
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
###############################################################################
# optional, for OSCS
-include ../../Makefile.common
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