adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

regression: remove forceful build options from CSpec makefiles. They don't seem to be needed.

This commit is contained in:
Japheth Lim 2015-12-10 18:22:22 +11:00
parent 194b2db850
commit d92666bc30
2 changed files with 6 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
spec/Makefile
View File

@ -36,7 +36,7 @@ spec-check: .FORCE
# Preprocess the kernel's source code and bitfield theory files. # Preprocess the kernel's source code and bitfield theory files.
c-kernel: .FORCE c-kernel: .FORCE
cd cspec/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) -B kernel_all.c_pp theories cd cspec/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) cspec
.PHONY: c-kernel .PHONY: c-kernel
# Produce the input data for the binary verification problem at -O1 # Produce the input data for the binary verification problem at -O1
@ -50,5 +50,6 @@ clean:
rm -rf abstract/generated rm -rf abstract/generated
cd cspec/c && $(MAKE) clean SKIP_PATH_CHECKS=1 cd cspec/c && $(MAKE) clean SKIP_PATH_CHECKS=1
rm -f umm_types.txt rm -f umm_types.txt
.PHONY: clean
include ../misc/isa-common.mk include ../misc/isa-common.mk

7
spec/cspec/c/Makefile
View File

@ -33,9 +33,10 @@ FASTPATH=yes
CSPEC_DIR=.. CSPEC_DIR=..
CONFIG_DOMAIN_SCHEDULE=config.c CONFIG_DOMAIN_SCHEDULE=config.c
.PHONY: newdefault # called by ../../spec/Makefile
cspec: kernel_all.c_pp ${UMM_TYPES} theories
newdefault: kernel_all.c_pp theories # theories is defined in seL4 makefile
.PHONY: cspec
# Create "umm_types" if necessary. # Create "umm_types" if necessary.
${UMM_TYPES}: kernel_all.c_pp ${UMM_TYPES}: kernel_all.c_pp