begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/CMakeLists.txt

   1 list(APPEND cbmc_compile_options
   2     -m32
   3 )
   4
   5 list(APPEND cbmc_compile_definitions
   6     CBMC
   7     WINVER=0x400
   8     _CONSOLE
   9     _CRT_SECURE_NO_WARNINGS
  10     _DEBUG
  11     _WIN32_WINNT=0x0500
  12     __PRETTY_FUNCTION__=__FUNCTION__
  13     __free_rtos__
  14 )
  15
  16 list(APPEND cbmc_compile_includes
  17     ${CMAKE_SOURCE_DIR}/Source/include
  18     ${CMAKE_SOURCE_DIR}/Source/portable/MSVC-MingW
  19         ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement
  20         ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include
  21     ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC
  22     ${cbmc_dir}/include
  23     ${cbmc_dir}/windows
  24 )
  25
  26 # Remove --flag for a specific proof with list(REMOVE_ITEM cbmc_flags --flag)
  27 list(APPEND cbmc_flags
  28     --32
  29     --bounds-check
  30     --pointer-check
  31     --div-by-zero-check
  32     --float-overflow-check
  33     --nan-check
  34     --nondet-static
  35     --pointer-overflow-check
  36     --signed-overflow-check
  37     --undefined-shift-check
  38     --unsigned-overflow-check
  39 )
  40