RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

cmake: TOPLEVELTYPES declared as target property

Browse Source 
TOPLEVELTYPES is not intended to be configurable by the user, rather is a reflection
on the types defined by the source. This changes the TOPLEVELTYPES argument to be
a property, allowing it to be constructed as a generator expression when generating
BF files. By being a property, and not something like a global property, it removes
the need to ensure that additions to TOPLEVELTYPES are done prior to any bitfield
target definitions.
This commit is contained in:
Adrian Danis
2017-11-15 10:50:20 +11:00
parent 9134ae3ee4
commit 9a89cbe4c6
2 changed files with 7 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
config.cmake
View File

@@ -20,16 +20,20 @@ config_set(KernelIsMaster KERNEL_MASTER ON)
# Proof based configuration variables # Proof based configuration variables
set(CSPEC_DIR "." CACHE PATH "") set(CSPEC_DIR "." CACHE PATH "")
set(SKIP_MODIFIES ON CACHE BOOL "") set(SKIP_MODIFIES ON CACHE BOOL "")
set(TOPLEVELTYPES "cte_C;tcb_C;endpoint_C;notification_C;asid_pool_C;pte_C;pde_C;user_data_C;user_data_device_C" CACHE STRING "")
set(SORRY_BITFIELD_PROOFS OFF CACHE BOOL "") set(SORRY_BITFIELD_PROOFS OFF CACHE BOOL "")
find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH) find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH)
set(force FORCE) set(force FORCE)
if(KernelVerificationBuild) if(KernelVerificationBuild)
set(force CLEAR) set(force CLEAR)
endif() endif()
mark_as_advanced(${force} CSPEC_DIR SKIP_MODIFIES TOPLEVELTYPES SORRY_BITFIELD_PROOFS UMM_TYPES) mark_as_advanced(${force} CSPEC_DIR SKIP_MODIFIES SORRY_BITFIELD_PROOFS UMM_TYPES)
# Use a custom target for collecting information during generation that we need during build # Use a custom target for collecting information during generation that we need during build
add_custom_target(kernel_config_target) add_custom_target(kernel_config_target)
# Put our common top level types in
set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES
cte_C tcb_C endpoint_C notification_C asid_pool_C pte_C pde_C user_data_C
user_data_device_C
)
######################## ########################
# Architecture selection # Architecture selection

4
tools/helpers.cmake
View File

@@ -151,9 +151,7 @@ function(GenProofsBFTarget target_name target_file pbf_path pbf_target prunes de
if(SORRY_BITFIELD_PROOFS) if(SORRY_BITFIELD_PROOFS)
list(APPEND args "--sorry_lemmas") list(APPEND args "--sorry_lemmas")
endif() endif()
foreach(type IN LISTS TOPLEVELTYPES) list(APPEND args "--toplevel;$<JOIN:$<TARGET_PROPERTY:kernel_config_target,TOPLEVELTYPES>,;--toplevel;>")
list(APPEND args "--toplevel" "${type}")
endforeach()
list(APPEND deps "${UMM_TYPES}") list(APPEND deps "${UMM_TYPES}")
GenThyBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${prunes}" "${deps}") GenThyBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${prunes}" "${deps}")
endfunction(GenProofsBFTarget) endfunction(GenProofsBFTarget)