| # You need to set COGENT_ROOT and AC_DIR, if different from the default. |
| |
| NAME=Trivial |
| SRC=$(NAME).cogent |
| |
| ifndef COGENT_ROOT |
| COGENT_ROOT=../../../ |
| endif |
| |
| ifndef AC_DIR |
| AC_DIR=$(COGENT_ROOT)/autocorres |
| endif |
| |
| |
| COGENT_FLAGS= -A \ |
| -Od --fno-static-inline --fno-fncall-as-macro --ffunc-purity-attr \ |
| --root-dir=$(COGENT_ROOT) \ |
| --dist-dir=build/ \ |
| --fake-header-dir=$(COGENT_ROOT)/cogent/lib |
| |
| .PHONY: default gen-c-proof verif clean |
| |
| default: gen-c-proof |
| |
| gen-c-proof: |
| cogent $(SRC) $(COGENT_FLAGS) |
| |
| verif: gen-c-proof |
| L4V_ARCH=ARM isabelle build -d ./build -d $(COGENT_ROOT)/cogent/isa -d $(AC_DIR) -v -b $(NAME)_AllRefine |
| |
| clean: |
| rm -rf build |
