xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/CMakeLists.txt (revision f7fd31bd4e8ded243be41470c43ddf6ce29e09e0) 
1list(APPEND cbmc_compile_options
2    -m32
3)
4
5list(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
16list(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)
27list(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
41