GNUmakefile 1.64 KB
Newer Older
Andre Maroneze's avatar
Andre Maroneze committed
1
2
3
4
5
6
# 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
Andre Maroneze's avatar
Andre Maroneze committed
7
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
Andre Maroneze's avatar
Andre Maroneze committed
8
9
###############################################################################

10
# Edit below as needed. Suggested flags are optional.
Andre Maroneze's avatar
Andre Maroneze committed
11
12
13
14
15
16
17
18
19

MACHDEP = x86_32

## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS    += -I ../code/harness -I ../code -I ../code/intel/linux \
               -DTRACE_HARNESS -DTRACE_TARGET

## General flags
FCFLAGS     += \
Andre Maroneze's avatar
Andre Maroneze committed
20
  -add-symbolic-path=..:. \
Andre Maroneze's avatar
Andre Maroneze committed
21
22
23
24
25
26
27
  -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 \
  -eva-domains equality \
28
29
30
31
32
  -eva-auto-loop-unroll 128 \
  -eva-slevel 11 \

# -eva-slevel 10 seems insufficient to remove the 5th alarm
# -eva-auto-loop-unroll is also necessary to avoid a 5th alarm
Andre Maroneze's avatar
Andre Maroneze committed
33
34
35
36
37
38
39
40
41
42
43
44
45
46

## GUI-only flags
FCGUIFLAGS += \

## Analysis targets (suffixed with .eva)
TARGETS = debie1.eva

### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
debie1.parse: \
  $(sort $(wildcard ../code/*.c)) \
  ../code/harness/harness.c \
  ../code/intel/linux/target.c \

### Epilogue. Do not modify this block. #######################################
Andre Maroneze's avatar
Andre Maroneze committed
47
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
Andre Maroneze's avatar
Andre Maroneze committed
48
49
50
51
###############################################################################

# optional, for OSCS
-include ../../Makefile.common