Path	Lines of Code
test/Coverity/ConfigFiles/FreeRTOSConfig.h	58
test/Coverity/ConfigFiles/FreeRTOSIPConfig.h	67
test/Coverity/ConfigFiles/pack_struct_end.h	1
test/Coverity/ConfigFiles/pack_struct_start.h	1
test/Coverity/ConfigFiles/portmacro.h	73
test/Coverity/Portable.c	99
test/build-combination/AllDisable/FreeRTOSIPConfig.h	61
test/build-combination/AllEnable/FreeRTOSIPConfig.h	61
test/build-combination/Common/FreeRTOSConfig.h	102
test/build-combination/Common/main.c	209
test/build-combination/Common/winbase.h	1
test/build-combination/Common/windows.h	1
test/cbmc/cmake/compute-coverage.cmake	13
test/cbmc/cmake/compute-property.cmake	13
test/cbmc/cmake/model-check.cmake	13
test/cbmc/include/aws_freertos_ip_verification_access_ip_define.h	5
test/cbmc/include/aws_freertos_tcp_verification_access_tcp_define.h	18
test/cbmc/include/cbmc.h	53
test/cbmc/include/queue_init.h	124
test/cbmc/include/tasksStubs.h	8
test/cbmc/patches/FreeRTOSConfig.h	110
test/cbmc/patches/FreeRTOSIPConfig.h	74
test/cbmc/patches/__init__.py	1
test/cbmc/patches/compute_patch.py	142
test/cbmc/patches/patch.py	27
test/cbmc/patches/patches_constants.py	13
test/cbmc/patches/unpatch.py	16
test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c	19
test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c	17
test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c	11
test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c	11
test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c	28
test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c	11
test/cbmc/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c	8
test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c	8
test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c	31
test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c	10
test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c	54
test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c	44
test/cbmc/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c	10
test/cbmc/proofs/CBMCStubLibrary/tasksStubs.c	34
test/cbmc/proofs/CheckOptions/CheckOptions_harness.c	51
test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c	63
test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c	55
test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c	37
test/cbmc/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c	12
test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c	16
test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c	12
test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c	40
test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c	52
test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c	50
test/cbmc/proofs/DNS/DNSlookup/DNSlookup_harness.c	32
test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c	10
test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c	74
test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c	16
test/cbmc/proofs/ReadNameField/ReadNameField_harness.c	55
test/cbmc/proofs/SkipNameField/SkipNameField_harness.c	30
test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/vSocketBind_harness.c	51
test/cbmc/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c	50
test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c	51
test/cbmc/proofs/Socket/vSocketClose/vSocketClose_harness.c	86
test/cbmc/proofs/Socket/vSocketWakeUpUser/vSocketWakeUpUser_harness.c	103
test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c	49
test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c	41
test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c	68
test/cbmc/proofs/TCPWin/vTCPWindowDestroy/vTCPWindowDestroy_harness.c	37
test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c	54
test/cbmc/proofs/make_cbmc_batch_files.py	23
test/cbmc/proofs/make_common_makefile.py	153
test/cbmc/proofs/make_configuration_directories.py	61
test/cbmc/proofs/make_proof_makefiles.py	247
test/cbmc/proofs/make_remove_makefiles.py	16
test/cbmc/proofs/make_type_header_files.py	108
test/cbmc/proofs/ninja.py	70
test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c	45
test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c	74
test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c	46
test/cbmc/proofs/prepare.py	37
test/cbmc/proofs/prvProcessEthernetPacket/prvProcessEthernetPacket_harness.c	41
test/cbmc/proofs/run-cbmc-proofs.py	206
test/cbmc/proofs/utility/memory_assignments.c	21
test/cbmc/stubs/cbmc.c	6
test/cbmc/stubs/freertos_api.c	206
test/cbmc/windows/WinBase.h	1
test/cbmc/windows/Windows.h	1
test/cbmc/windows/direct.h	1
test/cbmc/windows2/winbase.h	1
test/cbmc/windows2/windows.h	1
test/unit-test/ConfigFiles/FreeRTOSConfig.h	62
test/unit-test/ConfigFiles/FreeRTOSIPConfig.h	72
test/unit-test/ConfigFiles/FreeRTOS_errno_TCP.h	47
test/unit-test/ConfigFiles/IPTraceMacroDefaults.h	123
test/unit-test/ConfigFiles/NetworkBufferManagement.h	27
test/unit-test/ConfigFiles/NetworkInterface.h	14
test/unit-test/ConfigFiles/WinBase.h	1
test/unit-test/ConfigFiles/Windows.h	1
test/unit-test/ConfigFiles/pack_struct_end.h	1
test/unit-test/ConfigFiles/pack_struct_start.h	1
test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_stubs.c	136
test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_utest.c	1111
test/unit-test/FreeRTOS_ARP/ut.cmake	75
test/unit-test/FreeRTOS_DHCP/FreeRTOS_DHCP_mock.h	3
test/unit-test/FreeRTOS_DHCP/FreeRTOS_DHCP_stubs.c	141
test/unit-test/FreeRTOS_DHCP/FreeRTOS_DHCP_utest.c	1886
test/unit-test/FreeRTOS_DHCP/ut.cmake	79
test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_stubs.c	65
test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_utest.c	98
test/unit-test/FreeRTOS_Sockets/Sockets_list_macros.h	33
test/unit-test/FreeRTOS_Sockets/ut.cmake	95
test/unit-test/FreeRTOS_Stream_Buffer/FreeRTOS_Stream_Buffer_utest.c	669
test/unit-test/FreeRTOS_Stream_Buffer/list_macros.h	33
test/unit-test/FreeRTOS_Stream_Buffer/ut.cmake	89
test/unit-test/FreeRTOS_UDP_IP/FreeRTOS_UDP_IP_stubs.c	23
test/unit-test/FreeRTOS_UDP_IP/FreeRTOS_UDP_IP_utest.c	509
test/unit-test/FreeRTOS_UDP_IP/list_macros.h	33
test/unit-test/FreeRTOS_UDP_IP/ut.cmake	94
test/unit-test/TCPFilePaths.cmake	28
test/unit-test/catch_assert.h	39
test/unit-test/cmock/coverage.cmake	92
test/unit-test/cmock/create_test.cmake	159
test/unit-test/cmock/project.yml	33
test/unit-test/cmock_build.cmake	49