Makefile.libprove

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