Commit b2d3f506 authored by Thibault Martin's avatar Thibault Martin
Browse files

Adapt other IFM2020 benchs

parent a9a21f73
Pipeline #35538 failed with stage
in 2 minutes and 23 seconds
......@@ -49,38 +49,47 @@ frama-c/build/bin/frama-c:
};
echo "Local Frama-C (re-)installed."
# TARGETS=\
# 2048 \
# basic-cwe-examples \
# bench-moerman2018 \
# cerberus \
# chrony \
# debie1 \
# genann \
# gzip124 \
# hiredis \
# icpc \
# ioccc \
# itc-benchmarks \
# jsmn \
# kgflags \
# khash \
# kilo \
# libmodbus \
# libspng \
# libyaml \
# microstrain \
# mini-gmp \
# miniz \
# monocypher \
# papabench \
# polarssl \
# qlz \
# safestringlib \
# semver \
# solitaire \
# tweetnacl-usable \
# x509-parser \
TARGETS=\
2048 \
basic-cwe-examples \
bench-moerman2018 \
cerberus \
chrony \
debie1 \
genann \
gzip124 \
hiredis \
icpc \
ioccc \
itc-benchmarks \
jsmn \
kgflags \
khash \
kilo \
libmodbus \
libspng \
libyaml \
microstrain \
mini-gmp \
miniz \
monocypher \
papabench \
polarssl \
qlz \
safestringlib \
semver \
solitaire \
tweetnacl-usable \
x509-parser \
papabench
help::
@echo ""
......@@ -91,6 +100,7 @@ help::
QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGETS))
all: $(TARGETS)
all-nowp: $(TARGETS)
summary:
frama-c/share/analysis-scripts/summary.py
......
......@@ -49,4 +49,4 @@ ltest: $$(TARGETS)
ltest-nowp: $$(call filter-out-substring,_WP,$$(TARGETS))
clean::
rm -f *_labels.c *.labels *.hyperlabels *_NA *_Eq *_VA *_WP *_Candidate
rm -f *_labels.c *.labels *.hyperlabels *_NA *_Eq *_VA* *_WP* *_Candidate
......@@ -35,11 +35,11 @@ EVAFLAGS += \
# 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,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. #######################################
......
......@@ -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.
......@@ -37,26 +36,11 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = gzip124.eva
gzip124.parse: \
../gzip.c \
../zip.c \
../deflate.c \
../trees.c \
../bits.c \
../unzip.c \
../inflate.c \
../util.c \
../crypt.c \
../lzw.c \
../unlzw.c \
../unpack.c \
../unlzh.c \
../getopt.c \
$(shell $(FRAMAC)-config -print-share-path)/libc/stdlib.c \
fc_stubs.c \
# Targets for LTest
include ../../Makefile.ltest
$(eval $(call generate-rules,gzip,$(sort $(wildcard ../*.c)) $(shell $(FRAMAC)-config -print-share-path)/libc/stdlib.c fc_stubs.c))
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
......
......@@ -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.
......@@ -39,13 +38,8 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = 01_w_Defects.eva 02_wo_Defects.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
# NOTE: string.c is required due to the usage of strdup() in some tests,
# and also to avoid loss of precision when strcpy() is used.
# Both are related to tests in st_underrun.c
# Targets for LTest
include ../../Makefile.ltest
SUBDIR_SRCS=\
main.c \
......@@ -75,17 +69,13 @@ SUBDIR_SRCS=\
uninit_var.c \
zero_division.c \
01_w_Defects.parse: \
fc_stubs.c \
$(shell $(FRAMAC)-config -print-share-path)/libc/stdio.c \
$(shell $(FRAMAC)-config -print-share-path)/libc/string.c \
$(foreach file,$(SUBDIR_SRCS),$(wildcard ../01_w_Defects/$(file))) \
$(eval $(call generate-rules,itc-benchmarks,fc_stubs.c $(shell $(FRAMAC)-config -print-share-path)/libc/stdio.c $(shell $(FRAMAC)-config -print-share-path)/libc/string.c $(foreach file,$(SUBDIR_SRCS),$(wildcard ../01_w_Defects/$(file)))))
02_wo_Defects.parse: \
fc_stubs.c \
$(shell $(FRAMAC)-config -print-share-path)/libc/stdio.c \
$(shell $(FRAMAC)-config -print-share-path)/libc/string.c \
$(foreach file,$(SUBDIR_SRCS),$(wildcard ../02_wo_Defects/$(file))) \
# 02_wo_Defects.parse: \
# fc_stubs.c \
# $(shell $(FRAMAC)-config -print-share-path)/libc/stdio.c \
# $(shell $(FRAMAC)-config -print-share-path)/libc/string.c \
# $(foreach file,$(SUBDIR_SRCS),$(wildcard ../02_wo_Defects/$(file))) \
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
......
......@@ -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.
......@@ -36,14 +35,10 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = monocypher.eva
# Targets for LTest
include ../../Makefile.ltest
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
monocypher.parse: \
../src/monocypher.c \
../src/optional/sha512.c \
../tests/test.c \
$(eval $(call generate-rules,monocypher,../src/monocypher.c ../src/optional/sha512.c ../tests/test.c))
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
......
......@@ -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.
......@@ -37,16 +36,10 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = papabench.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
papabench.parse: \
$(sort $(wildcard ../sw/airborne/autopilot/*.c)) \
../sw/lib/c/math.c \
$(shell $(FRAMAC)-config -print-share-path)/libc/math.c \
fc_stubs.h \
# Targets for LTest
include ../../Makefile.ltest
$(eval $(call generate-rules,papabench,$(sort $(wildcard ../sw/airborne/autopilot/*.c)) ../sw/lib/c/math.c $(shell $(FRAMAC)-config -print-share-path)/libc/math.c fc_stubs.h))
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
......
......@@ -12,6 +12,8 @@ include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/analysis.mk
# Default target
all: ltest
all-nowp: ltest-nowp
# List available targets
help::
@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