# 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
include ../../prologue-ltest.mk
###############################################################################

# Edit below as needed. Suggested flags are optional.

MACHDEP = x86_32

## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS    += \
  -include$(shell $(FRAMAC)-config -print-share-path)/libc/string.h \
  -DSTDC_HEADERS=1 \
  -DHAVE_UNISTD_H=1 \
  -DDIRENT=1 \
  -DNO_UTIME=1 \
  -I$(shell $(FRAMAC)-config -print-share-path)/libc \
  -I$(DIR) \

## General flags
FCFLAGS  += \
  -load-module=nonterm \
  -add-symbolic-path=..:. \
  -nonterm-ignore do_exit \
  -main eva_main \

## Eva-specific flags
EVAFLAGS += \
  -eva-slevel 4 \
  -eva-no-alloc-returns-null \
  -eva-no-builtins-auto \
  -eva-widening-delay 3 \
  -eva-widening-period 3 \

## GUI-only flags
FCGUIFLAGS += \

# 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
###############################################################################

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