From 9a89cbe4c6c1974e3e06b163e3dd2d708e95203f Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 15 Nov 2017 10:50:20 +1100 Subject: [PATCH] cmake: TOPLEVELTYPES declared as target property 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. --- config.cmake | 8 ++++++-- tools/helpers.cmake | 4 +--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/config.cmake b/config.cmake index 6d972430c..0e5aba9b2 100644 --- a/config.cmake +++ b/config.cmake @@ -20,16 +20,20 @@ config_set(KernelIsMaster KERNEL_MASTER ON) # Proof based configuration variables set(CSPEC_DIR "." CACHE PATH "") 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 "") find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH) set(force FORCE) if(KernelVerificationBuild) set(force CLEAR) 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 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 diff --git a/tools/helpers.cmake b/tools/helpers.cmake index 29b1f9f5c..c3b17c55b 100644 --- a/tools/helpers.cmake +++ b/tools/helpers.cmake @@ -151,9 +151,7 @@ function(GenProofsBFTarget target_name target_file pbf_path pbf_target prunes de if(SORRY_BITFIELD_PROOFS) list(APPEND args "--sorry_lemmas") endif() - foreach(type IN LISTS TOPLEVELTYPES) - list(APPEND args "--toplevel" "${type}") - endforeach() + list(APPEND args "--toplevel;$,;--toplevel;>") list(APPEND deps "${UMM_TYPES}") GenThyBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${prunes}" "${deps}") endfunction(GenProofsBFTarget)