mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
64 lines
2.4 KiB
Makefile
64 lines
2.4 KiB
Makefile
# This Makefile compiles the GNAT standard library to .mlw files for GNATprove
|
|
|
|
PWD_COMMAND=$${PWDCMD-pwd}
|
|
GNAT2WHY = gnat2why
|
|
CC = gcc
|
|
AR = ar
|
|
|
|
ifeq ($(strip $(filter-out %sh,$(SHELL))),)
|
|
GNAT_ROOT = $(shell cd $(ROOT);${PWD_COMMAND})/
|
|
else
|
|
GNAT_ROOT = $(ROOT)/
|
|
endif
|
|
|
|
target = $(shell $(CC) -dumpmachine)
|
|
version = $(shell $(CC) -dumpversion)
|
|
ADA_INCLUDE_PATH = $(GNAT_ROOT)lib/gcc/$(target)/$(version)/adainclude
|
|
ADA_OBJECTS_PATH = $(GNAT_ROOT)lib/gcc/$(target)/$(version)/adalib
|
|
|
|
vpath %.adb $(ADA_INCLUDE_PATH)
|
|
vpath %.ads $(ADA_INCLUDE_PATH)
|
|
|
|
GNAT_OBJS:=$(filter-out __% SORTED,$(shell $(AR) t $(ADA_OBJECTS_PATH)/libgnat.a))
|
|
GNARL_OBJS:=$(filter-out __% SORTED,$(shell $(AR) t $(ADA_OBJECTS_PATH)/libgnarl.a))
|
|
EXCLUDE_OBJ:= \
|
|
adaint.o argv.o cio.o cstreams.o ctrl_c.o errno.o exit.o env.o raise.o \
|
|
sysdep.o aux-io.o init.o initialize.o locales.o seh_init.o cal.o \
|
|
arit64.o final.o tracebak.o expect.o mkdir.o socket.o \
|
|
targext.o raise-gcc.o adadecode.o terminals.o thread.o
|
|
|
|
ALL_OBJS := $(filter-out $(EXCLUDE_OBJ), $(GNARL_OBJS) $(GNAT_OBJS))
|
|
ALL_ALIS:=$(ALL_OBJS:.o=.ali)
|
|
ALL_WHYPACK:=$(ALL_ALIS:.ali=__package.mlw)
|
|
GLOBAL_GEN_ARG_FILE:= global_args.tmp
|
|
|
|
all: $(ALL_ALIS)
|
|
|
|
check: $(ALL_WHYPACK:__package.mlw=.check)
|
|
|
|
%__package.mlw: %.adb $(ALL_ALIS)
|
|
$(GNAT2WHY) -gnatpg -gnatws -I. $<
|
|
|
|
%__package.mlw: %.ads $(ALL_ALIS)
|
|
$(GNAT2WHY) -gnatpg -gnatws -I. $<
|
|
|
|
.PHONY: force
|
|
|
|
$(GLOBAL_GEN_ARG_FILE): force
|
|
@echo "global_gen_mode" > $@
|
|
|
|
%.ali: %.adb $(GLOBAL_GEN_ARG_FILE)
|
|
$(GNAT2WHY) -c -gnatc -gnatpg -gnatws -gnates=$(GLOBAL_GEN_ARG_FILE) $<
|
|
|
|
%.ali: %.ads $(GLOBAL_GEN_ARG_FILE)
|
|
$(GNAT2WHY) -c -gnatc -gnatpg -gnatws -gnates=$(GLOBAL_GEN_ARG_FILE) $<
|
|
|
|
%.check: %__package.mlw $(ALL_WHYPACK) $(WHY_STANDARD)
|
|
if [ -f $*__types_in_spec.mlw ] ; then why3 -L ../share/gnatprove/theories --type-only -L . $*__types_in_spec.mlw > /dev/null ; fi
|
|
if [ -f $*__types_in_body.mlw ] ; then why3 -L ../share/gnatprove/theories --type-only -L . $*__types_in_body.mlw > /dev/null ; fi
|
|
if [ -f $*__variables.mlw ] ; then why3 -L ../share/gnatprove/theories --type-only -L . $*__variables.mlw > /dev/null ; fi
|
|
if [ -f $*__context_in_spec.mlw ] ; then why3 -L ../share/gnatprove/theories --type-only -L . $*__context_in_spec.mlw > /dev/null ; fi
|
|
if [ -f $*__context_in_body.mlw ] ; then why3 -L ../share/gnatprove/theories --type-only -L . $*__context_in_body.mlw > /dev/null ; fi
|
|
why3 -L ../share/gnatprove/theories --type-only -L . $*__package.mlw > /dev/null
|
|
touch $@
|