Path	Lines of Code
test/cbmc/include/FreeRTOSConfig.h	105
test/cbmc/include/stubs.h	44
test/cbmc/proofs/Free_FreeRTOS/Free_FreeRTOS_harness.c	12
test/cbmc/proofs/Malloc_FreeRTOS/Malloc_FreeRTOS_harness.c	12
test/cbmc/proofs/OTA_ActivateNewImage/OTA_ActivateNewImage_harness.c	19
test/cbmc/proofs/OTA_CBOR_Decode_GetStreamResponseMessage/OTA_CBOR_Decode_GetStreamResponseMessage_harness.c	80
test/cbmc/proofs/OTA_CBOR_Encode_GetStreamRequestMessage/OTA_CBOR_Encode_GetStreamRequestMessage_harness.c	74
test/cbmc/proofs/OTA_CheckForUpdate/OTA_CheckForUpdate_harness.c	8
test/cbmc/proofs/OTA_Err_strerror/OTA_Err_strerror_harness.c	9
test/cbmc/proofs/OTA_EventProcessingTask/OTA_EventProcessingTask_harness.c	21
test/cbmc/proofs/OTA_GetImageState/OTA_GetImageState_harness.c	8
test/cbmc/proofs/OTA_GetState/OTA_GetState_harness.c	10
test/cbmc/proofs/OTA_GetStatistics/OTA_GetStatistics_harness.c	10
test/cbmc/proofs/OTA_HTTP_strerror/OTA_HTTP_strerror_harness.c	9
test/cbmc/proofs/OTA_Init/OTA_Init_harness.c	26
test/cbmc/proofs/OTA_JobParse_strerror/OTA_JobParse_strerror_harness.c	9
test/cbmc/proofs/OTA_MQTT_strerror/OTA_MQTT_strerror_harness.c	9
test/cbmc/proofs/OTA_OsStatus_strerror/OTA_OsStatus_strerror_harness.c	9
test/cbmc/proofs/OTA_PalStatus_strerror/OTA_PalStatus_strerror_harness.c	9
test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c	15
test/cbmc/proofs/OTA_SetImageState/OTA_SetImageState_harness.c	17
test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c	19
test/cbmc/proofs/OTA_SignalEvent/OTA_SignalEvent_harness.c	17
test/cbmc/proofs/OTA_Suspend/OTA_Suspend_harness.c	23
test/cbmc/proofs/OtaDeinitEvent_FreeRTOS/OtaDeinitEvent_FreeRTOS_harness.c	9
test/cbmc/proofs/OtaDeleteTimer_FreeRTOS/OtaDeleteTimer_FreeRTOS_harness.c	9
test/cbmc/proofs/OtaInitEvent_FreeRTOS/OtaInitEvent_FreeRTOS_harness.c	9
test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c	15
test/cbmc/proofs/OtaSendEvent_FreeRTOS/OtaSendEvent_FreeRTOS_harness.c	12
test/cbmc/proofs/OtaStartTimer_FreeRTOS/OtaStartTimer_FreeRTOS_harness.c	26
test/cbmc/proofs/OtaStopTimer_FreeRTOS/OtaStopTimer_FreeRTOS_harness.c	10
test/cbmc/proofs/Posix_OtaDeinitEvent/Posix_OtaDeinitEvent_harness.c	6
test/cbmc/proofs/Posix_OtaDeleteTimer/Posix_OtaDeleteTimer_harness.c	12
test/cbmc/proofs/Posix_OtaInitEvent/Posix_OtaInitEvent_harness.c	6
test/cbmc/proofs/Posix_OtaReceiveEvent/Posix_OtaReceiveEvent_harness.c	13
test/cbmc/proofs/Posix_OtaSendEvent/Posix_OtaSendEvent_harness.c	8
test/cbmc/proofs/Posix_OtaStartTimer/Posix_OtaStartTimer_harness.c	25
test/cbmc/proofs/Posix_OtaStopTimer/Posix_OtaStopTimer_harness.c	15
test/cbmc/proofs/Posix_RequestTimerCallback/requestTimerCallback_harness.c	22
test/cbmc/proofs/Posix_selfTestTimerCallback/selfTestTimerCallback_harness.c	22
test/cbmc/proofs/STDC_FREE/STDC_Free_harness.c	8
test/cbmc/proofs/STDC_Malloc/STDC_Malloc_harness.c	6
test/cbmc/proofs/agentShutdownCleanup/agentShutdownCleanup_harness.c	13
test/cbmc/proofs/base64Decode/base64Decode_harness.c	50
test/cbmc/proofs/buildStatusMessageReceiving/buildStatusMessageReceiving_harness.c	42
test/cbmc/proofs/checkDataType/checkDataType_harness.c	13
test/cbmc/proofs/cleanupControl_Mqtt/cleanupControl_Mqtt_harness.c	13
test/cbmc/proofs/cleanupData_Http/cleanupData_Http_harness.c	24
test/cbmc/proofs/cleanupData_Mqtt/cleanupData_Mqtt_harness.c	14
test/cbmc/proofs/closeFileHandler/closeFileHandler_harness.c	12
test/cbmc/proofs/dataHandlerCleanup/dataHandlerCleanup_harness.c	13
test/cbmc/proofs/decodeAndStoreDataBlock/decodeAndStoreDataBlock_harness.c	40
test/cbmc/proofs/decodeAndStoreKey/decodeAndStoreKey_harness.c	22
test/cbmc/proofs/decodeBase64IndexBuffer/decodeBase64IndexBuffer_harness.c	29
test/cbmc/proofs/decodeFileBlock_Http/decodeFileBlock_Http_harness.c	34
test/cbmc/proofs/decodeFileBlock_Mqtt/decodeFileBlock_Mqtt_harness.c	38
test/cbmc/proofs/executeHandler/executeHandler_harness.c	13
test/cbmc/proofs/extractAndStoreArray/extractAndStoreArray_harness.c	34
test/cbmc/proofs/extractParameter/extractParameter_harness.c	59
test/cbmc/proofs/freeFileContextMem/freeFileContextMem_harness.c	97
test/cbmc/proofs/getFileContextFromJob/getFileContextFromJob_harness.c	54
test/cbmc/proofs/handleCustomJob/handleCustomJob_harness.c	51
test/cbmc/proofs/handleJobParsingError/handleJobParsingError_harness.c	22
test/cbmc/proofs/handleSelfTestJobDoc/handleSelfTestJobDoc_harness.c	22
test/cbmc/proofs/handleUnexpectedEvents/handleUnexpectedEvents_harness.c	14
test/cbmc/proofs/inSelfTestHandler/inSelfTestHandler_harness.c	19
test/cbmc/proofs/ingestDataBlock/ingestDataBlock_harness.c	66
test/cbmc/proofs/ingestDataBlockCleanup/ingestDataBlockCleanup_harness.c	27
test/cbmc/proofs/initDocModel/initDocModel_harness.c	23
test/cbmc/proofs/initFileHandler/initFileHandler_harness.c	20
test/cbmc/proofs/initFileTransfer_Http/initFileTransfer_Http_harness.c	24
test/cbmc/proofs/initFileTransfer_Mqtt/initFileTransfer_Mqtt_harness.c	31
test/cbmc/proofs/initializeAppBuffers/initializeAppBuffers_harness.c	7
test/cbmc/proofs/initializeLocalBuffers/initializeLocalBuffers_harness.c	18
test/cbmc/proofs/jobNotificationHandler/jobNotificationHandler_harness.c	23
test/cbmc/proofs/otaClose/otaClose_harness.c	26
test/cbmc/proofs/otaTimerCallback/otaTimerCallback_harness.c	15
test/cbmc/proofs/parseJSONbyModel/parseJSONbyModel_harness.c	83
test/cbmc/proofs/parseJobDoc/parseJobDoc_harness.c	68
test/cbmc/proofs/platformInSelftest/platformInSelftest_harness.c	15
test/cbmc/proofs/prepare.py	29
test/cbmc/proofs/preprocessBase64Index/preprocessBase64Index_harness.c	19
test/cbmc/proofs/processDataBlock/processDataBlock_harness.c	41
test/cbmc/proofs/processDataHandler/processDataHandler_harness.c	69
test/cbmc/proofs/processJobHandler/processJobHandler_harness.c	20
test/cbmc/proofs/processNullFileContext/processNullFileContext_harness.c	13
test/cbmc/proofs/processValidFileContext/processValidFileContext_harness.c	23
test/cbmc/proofs/prvBuildStatusMessageFinish/prvBuildStatusMessageFinish_harness.c	49
test/cbmc/proofs/prvBuildStatusMessageSelfTest/prvBuildStatusMessageSelfTest_harness.c	38
test/cbmc/proofs/publishStatusMessage/publishStatusMessage_harness.c	39
test/cbmc/proofs/receiveAndProcessOtaEvent/receiveAndProcessOtaEvent_harness.c	22
test/cbmc/proofs/requestDataBlock_Http/requestDataBlock_Http_harness.c	25
test/cbmc/proofs/requestDataHandler/requestDataHandler_harness.c	21
test/cbmc/proofs/requestFileBlock_Mqtt/requestFileBlock_Mqtt_harness.c	49
test/cbmc/proofs/requestJobHandler/requestJobHandler_harness.c	23
test/cbmc/proofs/requestJob_Mqtt/requestJob_Mqtt_harness.c	44
test/cbmc/proofs/requestTimerCallback/requestTimerCallback_harness.c	27
test/cbmc/proofs/resumeHandler/resumeHandler_harness.c	9
test/cbmc/proofs/searchTransition/searchTransition_harness.c	15
test/cbmc/proofs/selfTestTimerCallback/selfTestTimerCallback_harness.c	27
test/cbmc/proofs/setControlInterface/setControlInterface_harness.c	8
test/cbmc/proofs/setDataInterface/setDataInterface_harness.c	12
test/cbmc/proofs/setImageStateWithReason/setImageStateWithReason_harness.c	39
test/cbmc/proofs/shutdownHandler/shutdownHandler_harness.c	12
test/cbmc/proofs/startHandler/startHandler_harness.c	19
test/cbmc/proofs/stringBuilder/stringBuilder_harness.c	35
test/cbmc/proofs/stringBuilderUInt32Decimal/stringBuilderUInt32Decimal_harness.c	17
test/cbmc/proofs/stringBuilderUInt32Hex/stringBuilderUInt32Hex_harness.c	17
test/cbmc/proofs/subscribeToJobNotificationTopics/subscribeToJobNotificationTopics_harness.c	32
test/cbmc/proofs/suspendHandler/suspendHandler_harness.c	11
test/cbmc/proofs/unsubscribeFromDataStream/unsubscribeFromDataStream_harness.c	30
test/cbmc/proofs/unsubscribeFromJobNotificationTopic/unsubscribeFromJobNotificationTopic_harness.c	30
test/cbmc/proofs/updateBase64DecodingBuffer/updateBase64DecodingBuffer_harness.c	18
test/cbmc/proofs/updateJobStatusFromImageState/updateJobStatusFromImageState_harness.c	18
test/cbmc/proofs/updateJobStatus_Mqtt/updateJobStatus_Mqtt_harness.c	57
test/cbmc/proofs/userAbortHandler/userAbortHandler_harness.c	26
test/cbmc/proofs/validateAndStartJob/validateAndStartJob_harness.c	28
test/cbmc/proofs/validateDataBlock/validateDataBlock_harness.c	13
test/cbmc/proofs/validateJSON/validateJSON_harness.c	24
test/cbmc/proofs/validateUpdateVersion/validateUpdateVersion_harness.c	14
test/cbmc/proofs/verifyActiveJobStatus/verifyActiveJobStatus_harness.c	55
test/cbmc/proofs/verifyRequiredParamsExtracted/verifyRequiredParamsExtracted_harness.c	15
test/cbmc/source/stubs.c	186
test/unit-test/cmock_build.cmake	49
test/unit-test/ota_base64_utest.c	407
test/unit-test/ota_cbor_utest.c	277
test/unit-test/ota_config.h	26
test/unit-test/ota_os_posix_utest.c	106
test/unit-test/ota_utest.c	2277
test/unit-test/utest_helpers.c	130
test/unit-test/utest_helpers.h	18
tools/cmock/create_test.cmake	158