From 44e964e87c69ae64edc7ff4fd5774fa13641b1fb Mon Sep 17 00:00:00 2001 From: Ubuntu Date: Mon, 29 Nov 2021 06:57:33 +0000 Subject: [PATCH 01/11] fix cbmc warning --- .../Cellular_ATGetSpecificNextTok/Makefile | 1 + .../proofs/Cellular_ATHexStrToHex/Makefile | 1 + .../Cellular_ATIsPrefixPresent/Makefile | 1 + .../proofs/Cellular_ATIsStrDigit/Makefile | 1 + .../Cellular_ATRemoveAllDoubleQuote/Makefile | 1 + .../Cellular_ATRemoveAllWhiteSpaces/Makefile | 1 + .../Makefile | 1 + .../Makefile | 1 + .../proofs/Cellular_ATRemovePrefix/Makefile | 1 + .../Makefile | 1 + test/cbmc/proofs/Cellular_ATStrDup/Makefile | 1 + .../proofs/Cellular_ATStrStartWith/Makefile | 1 + test/cbmc/proofs/Cellular_ATStrtoi/Makefile | 1 + .../proofs/Cellular_ATcheckErrorCode/Makefile | 1 + .../Cellular_CommonATCommandRaw/Makefile | 4 ++ .../proofs/Cellular_CommonCleanup/Makefile | 4 ++ .../Cellular_CommonCreateSocket/Makefile | 4 ++ .../Cellular_CommonGetEidrxSettings/Makefile | 3 + .../Cellular_CommonGetIPAddress/Makefile | 3 + .../Cellular_CommonGetModemInfo/Makefile | 3 + .../Cellular_CommonGetNetworkTime/Makefile | 3 + .../Cellular_CommonGetPsmSettings/Makefile | 3 + .../Makefile | 3 + .../Cellular_CommonGetServiceStatus/Makefile | 3 + .../Cellular_CommonGetSimCardInfo/Makefile | 3 + .../Makefile | 3 + test/cbmc/proofs/Cellular_CommonInit/Makefile | 4 ++ .../Makefile | 4 ++ .../Makefile | 4 ++ .../Makefile | 4 ++ .../Makefile | 4 ++ .../Makefile | 4 ++ .../cbmc/proofs/Cellular_CommonRfOff/Makefile | 3 + test/cbmc/proofs/Cellular_CommonRfOn/Makefile | 3 + .../Cellular_CommonSetEidrxSettings/Makefile | 3 + .../Cellular_CommonSetPdnConfig/Makefile | 3 + .../Cellular_CommonSetPsmSettings/Makefile | 3 + .../Makefile | 4 ++ .../Makefile | 4 ++ .../Makefile | 4 ++ .../Cellular_CommonSocketSetSockOpt/Makefile | 4 ++ .../Cellular_CommonUrcProcessCereg/Makefile | 4 ++ .../Cellular_CommonUrcProcessCgreg/Makefile | 4 ++ .../Cellular_CommonUrcProcessCreg/Makefile | 4 ++ .../proofs/_Cellular_GenericCallback/Makefile | 4 ++ .../proofs/_Cellular_GetCurrentRat/Makefile | 2 + .../_Cellular_GetModuleContext/Makefile | 4 ++ .../proofs/_Cellular_GetSocketData/Makefile | 3 + .../proofs/_Cellular_IsValidSocket/Makefile | 5 ++ .../cbmc/proofs/_Cellular_LibCleanup/Makefile | 4 ++ .../_Cellular_ModemEventCallback/Makefile | 4 ++ .../Makefile | 4 ++ .../_Cellular_PdnEventCallback/Makefile | 4 ++ .../_Cellular_RemoveSocketData/Makefile | 4 ++ .../Makefile | 4 ++ .../Makefile | 4 +- .../Makefile | 3 + .../Makefile | 4 ++ test/cbmc/sources/cellular_modules.c | 67 +++++++++++++++++++ test/cbmc/sources/cellular_platform.c | 57 ++++++++++++++++ test/cbmc/stubs/strchr.c | 8 +-- test/cbmc/stubs/strnlen.c | 42 ++++++++++++ test/cbmc/stubs/strtok.c | 4 +- 63 files changed, 344 insertions(+), 7 deletions(-) create mode 100644 test/cbmc/sources/cellular_modules.c create mode 100644 test/cbmc/sources/cellular_platform.c create mode 100644 test/cbmc/stubs/strnlen.c diff --git a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile index 93959ec1..58e4eb4c 100755 --- a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile +++ b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile @@ -39,6 +39,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c diff --git a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile index 6d823f7a..a2879aa0 100755 --- a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile +++ b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile @@ -39,6 +39,7 @@ UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile b/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile index a9282ce5..8ede9fa7 100755 --- a/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile +++ b/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile @@ -41,6 +41,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile index 69f5f741..5bd957d0 100755 --- a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile +++ b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile @@ -39,6 +39,7 @@ UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile index d5dbc6cc..91d8478e 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile @@ -39,6 +39,7 @@ UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile index 2b966431..091560f3 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile @@ -39,6 +39,7 @@ UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile index ae467499..92e0e3bd 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile @@ -38,6 +38,7 @@ UNWINDSET += Cellular_ATRemoveLeadingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile index c328ff3a..de0bbebd 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile @@ -39,6 +39,7 @@ UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile index 6d9aa7ea..7f834332 100755 --- a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile @@ -37,6 +37,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile index c7f586a5..239e5b7b 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile @@ -39,6 +39,7 @@ UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATStrDup/Makefile b/test/cbmc/proofs/Cellular_ATStrDup/Makefile index 91398d3e..af04eced 100755 --- a/test/cbmc/proofs/Cellular_ATStrDup/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrDup/Makefile @@ -39,6 +39,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c diff --git a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile index 708d6539..e766157c 100755 --- a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile @@ -39,6 +39,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile index 9bbf9a2f..a6a3ec33 100755 --- a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile @@ -37,6 +37,7 @@ UNWINDSET += strtol.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c PROJECT_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtol.c diff --git a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile index 70f7bf11..4421dfd7 100755 --- a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile +++ b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile @@ -43,6 +43,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile b/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile index 9bf6c0f5..3e686d86 100755 --- a/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile +++ b/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile @@ -30,7 +30,11 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonCleanup/Makefile b/test/cbmc/proofs/Cellular_CommonCleanup/Makefile index d0408b20..ac45095c 100755 --- a/test/cbmc/proofs/Cellular_CommonCleanup/Makefile +++ b/test/cbmc/proofs/Cellular_CommonCleanup/Makefile @@ -38,7 +38,11 @@ UNWINDSET += __CPROVER_file_local_cellular_common_c__Cellular_FreeContext.0:$(CB PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile index d2b47bb6..aa33d9ed 100755 --- a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile +++ b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile @@ -41,7 +41,11 @@ UNWINDSET += harness.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile index 2e492525..a6777eab 100755 --- a/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile index 64e1567f..249ca3d8 100755 --- a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile b/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile index f46b10c2..b0827cd0 100755 --- a/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile @@ -29,6 +29,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile b/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile index 6aeeaf33..84889121 100755 --- a/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile index 1e44b0d8..af19e607 100755 --- a/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile @@ -31,6 +31,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile b/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile index 45fb8c17..c6344558 100755 --- a/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile b/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile index 93ef185a..4cfde5e6 100755 --- a/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile @@ -31,6 +31,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile b/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile index abb47096..f989468c 100755 --- a/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile @@ -31,6 +31,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile b/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile index aeb1d61e..28aab7a1 100755 --- a/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile @@ -31,6 +31,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonInit/Makefile b/test/cbmc/proofs/Cellular_CommonInit/Makefile index e6271632..5ae9cd86 100755 --- a/test/cbmc/proofs/Cellular_CommonInit/Makefile +++ b/test/cbmc/proofs/Cellular_CommonInit/Makefile @@ -30,6 +30,10 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile index c4f68f14..30946650 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile index 0f981a0e..7d369e7d 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile index d889c675..60226e58 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile index a91087d0..307c1e16 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile index d0ec43a5..37e5fe98 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRfOff/Makefile b/test/cbmc/proofs/Cellular_CommonRfOff/Makefile index a8a8b3e8..c47810fd 100755 --- a/test/cbmc/proofs/Cellular_CommonRfOff/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRfOff/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonRfOn/Makefile b/test/cbmc/proofs/Cellular_CommonRfOn/Makefile index 17c1038b..1e1f65c2 100755 --- a/test/cbmc/proofs/Cellular_CommonRfOn/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRfOn/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile index 613b5b1d..b44be21a 100755 --- a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile @@ -30,6 +30,9 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile index b2e25749..9e2659d8 100755 --- a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile @@ -31,6 +31,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile index dc2a955c..bd74d0bd 100755 --- a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile @@ -31,6 +31,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile index a6967772..d320703a 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile index 310cc86b..687dacbb 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile index 9af13958..4012b6ae 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile b/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile index 331c9dd1..323aab9b 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile @@ -41,6 +41,10 @@ UNWINDSET += harness.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile index e615b096..822b5225 100755 --- a/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile +++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile @@ -48,6 +48,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile index c5750747..1fd45f28 100755 --- a/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile +++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile @@ -48,6 +48,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile index c3035a17..d6b32011 100755 --- a/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile +++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile @@ -40,6 +40,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_GenericCallback/Makefile b/test/cbmc/proofs/_Cellular_GenericCallback/Makefile index f55898fc..27a89549 100755 --- a/test/cbmc/proofs/_Cellular_GenericCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_GenericCallback/Makefile @@ -31,6 +31,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile b/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile index b8f3897a..f7c50835 100755 --- a/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile +++ b/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile @@ -30,6 +30,8 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile b/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile index 05e29115..4aec13c7 100755 --- a/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile +++ b/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile @@ -40,6 +40,10 @@ UNWINDSET += _Cellular_CreateSocketData.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_GetSocketData/Makefile b/test/cbmc/proofs/_Cellular_GetSocketData/Makefile index 33dc0c49..9ebb6887 100755 --- a/test/cbmc/proofs/_Cellular_GetSocketData/Makefile +++ b/test/cbmc/proofs/_Cellular_GetSocketData/Makefile @@ -38,6 +38,9 @@ UNWINDSET += allocateSocket.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile b/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile index a58e83f9..f0630d37 100755 --- a/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile +++ b/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile @@ -40,6 +40,11 @@ UNWINDSET += _Cellular_CreateSocketData.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +OOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c + PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_LibCleanup/Makefile b/test/cbmc/proofs/_Cellular_LibCleanup/Makefile index eabbcbad..b85390e4 100755 --- a/test/cbmc/proofs/_Cellular_LibCleanup/Makefile +++ b/test/cbmc/proofs/_Cellular_LibCleanup/Makefile @@ -39,6 +39,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile b/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile index 30e9fe7b..27679012 100755 --- a/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile @@ -39,6 +39,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile b/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile index 3ace40cf..48c52573 100755 --- a/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile @@ -39,6 +39,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile b/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile index 05fe6342..24a8aa57 100755 --- a/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile @@ -39,6 +39,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile index ba46854c..f3d8aeb7 100755 --- a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile +++ b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile @@ -42,6 +42,10 @@ UNWINDSET += _Cellular_RemoveSocketData.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile b/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile index 37ab6d5d..e234a044 100755 --- a/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile @@ -39,6 +39,10 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile index 2833c687..2c73cf76 100755 --- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile @@ -41,9 +41,11 @@ UNWINDSET += __builtin___strncpy_chk.0:$(CBMC_MAX_BUFSIZE) PROJECT_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +ROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pktio.c include ../Makefile.common diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile index 9d0b7079..fa084dfd 100755 --- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile @@ -42,8 +42,11 @@ UNWINDSET += __builtin___strncpy_chk.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pktio.c include ../Makefile.common diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile index a627efae..686bdca0 100755 --- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile +++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile @@ -35,6 +35,10 @@ INCLUDES += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c +PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/sources/cellular_modules.c b/test/cbmc/sources/cellular_modules.c new file mode 100644 index 00000000..a68d872f --- /dev/null +++ b/test/cbmc/sources/cellular_modules.c @@ -0,0 +1,67 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file cellular_modules.h + * @brief cbmc wrapper functions in cellular_common_portable.h. + */ + +/* Include paths for public enums, structures, and macros. */ +#include "cellular_common_portable.h" + +CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext, + void ** ppModuleContext ) +{ + CellularError_t ret=nondet_int(); + __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + return ret; +} + + +CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext ) +{ + CellularError_t ret=nondet_int(); + __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + return ret; +} + + +CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext ) +{ + CellularError_t ret=nondet_int(); + __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + return ret; +} + + +CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext ) +{ + CellularError_t ret=nondet_int(); + __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + return ret; +} + + +/* ========================================================================== */ diff --git a/test/cbmc/sources/cellular_platform.c b/test/cbmc/sources/cellular_platform.c new file mode 100644 index 00000000..19a09458 --- /dev/null +++ b/test/cbmc/sources/cellular_platform.c @@ -0,0 +1,57 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file cellular_platform.c + * @brief cbmc wrapper functions in cellular_platform.h. + */ + +/* Include paths for public enums, structures, and macros. */ +#include "cellular_platform.h" + +void MockPlatformMutex_Unlock( PlatformMutex_t * pMutex ) +{ + ( void ) pMutex; +} + +void MockPlatformMutex_Lock( PlatformMutex_t * pMutex ) +{ + ( void ) pMutex; +} + +void MockPlatformMutex_Destroy( PlatformMutex_t * pMutex ) +{ + pMutex->created = false; +} + +bool MockPlatformMutex_Create( PlatformMutex_t * pNewMutex, + bool recursive ) +{ + ( void ) recursive; + pNewMutex->created = true; + return true; +} + +/* ========================================================================== */ diff --git a/test/cbmc/stubs/strchr.c b/test/cbmc/stubs/strchr.c index 51568ed3..0ef77f4a 100644 --- a/test/cbmc/stubs/strchr.c +++ b/test/cbmc/stubs/strchr.c @@ -40,7 +40,7 @@ char * __builtin___strchr_chk( const char * s, int c ) { - if( ( __CPROVER_w_ok( s, 1 ), "write" ) && ( __CPROVER_r_ok( s, 1 ), "read" ) ) + if( __CPROVER_w_ok( s, 1 ) && __CPROVER_r_ok( s, 1 ) ) { while( *s != '\0' ) { @@ -49,7 +49,7 @@ return s; } - if( ( __CPROVER_w_ok( s + 1, 1 ), "write" ) && ( __CPROVER_r_ok( s + 1, 1 ), "read" ) ) + if( __CPROVER_w_ok( s + 1, 1 ) && __CPROVER_r_ok( s + 1, 1 ) ) { s++; } @@ -62,7 +62,7 @@ char * strchr( const char * s, int c ) { - if( ( __CPROVER_w_ok( s, 1 ), "write" ) && ( __CPROVER_r_ok( s, 1 ), "read" ) ) + if( __CPROVER_w_ok( s, 1 ) && __CPROVER_r_ok( s, 1 ) ) { while( *s != '\0' ) { @@ -71,7 +71,7 @@ return s; } - if( ( __CPROVER_w_ok( s + 1, 1 ), "write" ) && ( __CPROVER_r_ok( s + 1, 1 ), "read" ) ) + if( __CPROVER_w_ok( s + 1, 1 ) && __CPROVER_r_ok( s + 1, 1 ) ) { s++; } diff --git a/test/cbmc/stubs/strnlen.c b/test/cbmc/stubs/strnlen.c new file mode 100644 index 00000000..a351133a --- /dev/null +++ b/test/cbmc/stubs/strnlen.c @@ -0,0 +1,42 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file strnlen.c + * @brief Creates a stub for strnlen. This stub checks if, for the input copy + * length, the destination and source are valid accessible memory. + */ + +#include + +size_t strnlen( const char *s, + size_t n ) +{ + size_t ret=nondet_size_t(); + __CPROVER_assume( ret <= n ); + __CPROVER_assert( __CPROVER_w_ok( s, n ), "write" ); + __CPROVER_assert( __CPROVER_r_ok( s, n ), "read" ); + return ret; +} diff --git a/test/cbmc/stubs/strtok.c b/test/cbmc/stubs/strtok.c index 53bfcf89..3a82e41e 100644 --- a/test/cbmc/stubs/strtok.c +++ b/test/cbmc/stubs/strtok.c @@ -40,7 +40,7 @@ char * __builtin___strtok( char * s, const char * delim ) { - if( ( __CPROVER_w_ok( s, 1 ), "write" ) && ( __CPROVER_r_ok( s, 1 ), "read" ) ) + if( __CPROVER_w_ok( s, 1 ) && __CPROVER_r_ok( s, 1 ) ) { while( *s != '\0' ) { @@ -49,7 +49,7 @@ return s; } - if( ( __CPROVER_w_ok( s + 1, 1 ), "write" ) && ( __CPROVER_r_ok( s + 1, 1 ), "read" ) ) + if( __CPROVER_w_ok( s + 1, 1 ) && __CPROVER_r_ok( s + 1, 1 ) ) { s++; } From 844368d9c19781b04036e04299057419e822ce81 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Tue, 30 Nov 2021 08:13:15 +0000 Subject: [PATCH 02/11] revert useless .c files in Makefile --- test/cbmc/include/cellular_platform.h | 47 +++++-- .../Cellular_CommonATCommandRaw/Makefile | 2 - .../proofs/Cellular_CommonCleanup/Makefile | 2 - .../Cellular_CommonCreateSocket/Makefile | 2 - .../Cellular_CommonGetEidrxSettings/Makefile | 1 - .../Cellular_CommonGetIPAddress/Makefile | 1 - .../Cellular_CommonGetModemInfo/Makefile | 1 - .../Cellular_CommonGetNetworkTime/Makefile | 1 - .../Cellular_CommonGetPsmSettings/Makefile | 1 - .../Makefile | 1 - .../Cellular_CommonGetServiceStatus/Makefile | 1 - .../Cellular_CommonGetSimCardInfo/Makefile | 1 - .../Makefile | 1 - test/cbmc/proofs/Cellular_CommonInit/Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../cbmc/proofs/Cellular_CommonRfOff/Makefile | 1 - test/cbmc/proofs/Cellular_CommonRfOn/Makefile | 1 - .../Cellular_CommonSetEidrxSettings/Makefile | 1 - .../Cellular_CommonSetPdnConfig/Makefile | 1 - .../Cellular_CommonSetPsmSettings/Makefile | 1 - .../Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../Cellular_CommonSocketSetSockOpt/Makefile | 2 - .../Cellular_CommonUrcProcessCereg/Makefile | 2 - .../Cellular_CommonUrcProcessCgreg/Makefile | 2 - .../Cellular_CommonUrcProcessCreg/Makefile | 2 - .../proofs/_Cellular_GenericCallback/Makefile | 2 - .../proofs/_Cellular_GetCurrentRat/Makefile | 1 - .../_Cellular_GetModuleContext/Makefile | 2 - .../proofs/_Cellular_GetSocketData/Makefile | 1 - .../proofs/_Cellular_IsValidSocket/Makefile | 5 +- .../_Cellular_IsValidSocket_harness.c | 1 + .../cbmc/proofs/_Cellular_LibCleanup/Makefile | 2 - .../_Cellular_ModemEventCallback/Makefile | 2 - .../Makefile | 2 - .../_Cellular_PdnEventCallback/Makefile | 2 - .../_Cellular_RemoveSocketData/Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - .../Makefile | 2 - test/cbmc/proofs/cbmc_build.sh | 14 +++ test/cbmc/proofs/cbmc_clean.sh | 14 +++ test/cbmc/sources/cellular_platform.c | 117 ++++++++++++++++++ test/cbmc/stubs/bsearch.c | 52 ++++++++ test/cbmc/stubs/snprintf.c | 42 +++++++ test/cbmc/stubs/strnlen.c | 15 ++- test/cbmc/stubs/strstr.c | 48 +++++++ test/cbmc/stubs/strtok.c | 22 ++++ 54 files changed, 359 insertions(+), 88 deletions(-) create mode 100755 test/cbmc/proofs/cbmc_build.sh create mode 100755 test/cbmc/proofs/cbmc_clean.sh create mode 100644 test/cbmc/stubs/bsearch.c create mode 100644 test/cbmc/stubs/snprintf.c create mode 100644 test/cbmc/stubs/strstr.c diff --git a/test/cbmc/include/cellular_platform.h b/test/cbmc/include/cellular_platform.h index 7e9e4ca3..b459c013 100644 --- a/test/cbmc/include/cellular_platform.h +++ b/test/cbmc/include/cellular_platform.h @@ -75,6 +75,8 @@ typedef void * PVOID; #define PlatformMutex_TryLock MockPlatformMutex_TryLock #define PlatformMutex_Unlock MockPlatformMutex_Unlock +#define Platform_CreateDetachedThread MockPlatform_CreateDetachedThread + #define taskENTER_CRITICAL() PVOID #define taskEXIT_CRITICAL() PVOID @@ -97,6 +99,24 @@ typedef void * PVOID; #define CELLULAR_URC_TOKEN_WO_PREFIX_TABLE_SIZE ( sizeof( CellularUrcTokenWoPrefixTable ) / sizeof( char * ) ) #define CELLULAR_SRC_EXTRA_TOKEN_SUCCESS_TABLE_SIZE ( sizeof( CellularSrcExtraTokenSuccessTable ) / sizeof( char * ) ) +#if ( configUSE_16_BIT_TICKS == 1 ) + typedef uint16_t TickType_t; + #define portMAX_DELAY ( TickType_t ) 0xffff +#else + typedef uint64_t TickType_t; + #define portMAX_DELAY ( TickType_t ) 0xffffffffUL +#endif + +/* + * The type that holds event bits always matches TickType_t - therefore the + * number of bits it holds is set by configUSE_16_BIT_TICKS (16 bits if set to 1, + * 32 bits if set to 0. + * + * \defgroup EventBits_t EventBits_t + * \ingroup EventGroup + */ +typedef TickType_t EventBits_t; + /** * @brief Cellular library platform thread API and configuration. * @@ -107,9 +127,9 @@ typedef void * PVOID; * the platform related stack size and priority. */ -bool Platform_CreateDetachedThread( void ( * threadRoutine )( void * ), +bool Platform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ), void * pArgument, - int32_t priority, + size_t priority, size_t stackSize ); #define PLATFORM_THREAD_DEFAULT_STACK_SIZE ( 2048U ) @@ -180,6 +200,9 @@ void PlatformMutex_Destroy( PlatformMutex_t * pMutex ); void PlatformMutex_Lock( PlatformMutex_t * pMutex ); bool PlatformMutex_TryLock( PlatformMutex_t * pMutex ); void PlatformMutex_Unlock( PlatformMutex_t * pMutex ); +int32_t PlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupEvent, + EventBits_t event, + BaseType_t * pHigherPriorityTaskWoken ); void * safeMalloc( size_t xWantedSize ); void allocateSocket( void * pCellularHandle ); bool MockxQueueReceive( int32_t * queue, @@ -188,6 +211,18 @@ bool MockxQueueReceive( int32_t * queue, uint16_t MockPlatformEventGroup_Create(); uint16_t MockPlatformEventGroup_WaitBits(); +QueueHandle_t xQueueCreate( int32_t uxQueueLength, + uint32_t uxItemSize ); +uint16_t vQueueDelete( QueueHandle_t queue ); +BaseType_t xQueueSend( QueueHandle_t queue, + void * data, + uint32_t time ); + +uint16_t PlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup, + TickType_t uxBitsToClear ); +uint16_t PlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent ); +uint16_t PlatformEventGroup_GetBits( PlatformEventGroupHandle_t groupEvent ); + /*-----------------------------------------------------------*/ /** @@ -202,12 +237,4 @@ uint16_t MockPlatformEventGroup_WaitBits(); #define Platform_Malloc safeMalloc #define Platform_Free free -#if ( configUSE_16_BIT_TICKS == 1 ) - typedef uint16_t TickType_t; - #define portMAX_DELAY ( TickType_t ) 0xffff -#else - typedef uint64_t TickType_t; - #define portMAX_DELAY ( TickType_t ) 0xffffffffUL -#endif - #endif /* __CELLULAR_PLATFORM_H__ */ diff --git a/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile b/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile index 3e686d86..73cb36f5 100755 --- a/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile +++ b/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile @@ -34,7 +34,5 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonCleanup/Makefile b/test/cbmc/proofs/Cellular_CommonCleanup/Makefile index ac45095c..d4849ef0 100755 --- a/test/cbmc/proofs/Cellular_CommonCleanup/Makefile +++ b/test/cbmc/proofs/Cellular_CommonCleanup/Makefile @@ -42,7 +42,5 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile index aa33d9ed..a436623d 100755 --- a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile +++ b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile @@ -45,7 +45,5 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile index a6777eab..d0d272a6 100755 --- a/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile index 249ca3d8..b14714dd 100755 --- a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile b/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile index b0827cd0..b011ab25 100755 --- a/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile b/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile index 84889121..5084547b 100755 --- a/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile index af19e607..71b9e780 100755 --- a/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile @@ -33,7 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile b/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile index c6344558..a3a562be 100755 --- a/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile b/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile index 4cfde5e6..ead1c4e2 100755 --- a/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile @@ -33,7 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile b/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile index f989468c..e504c6b8 100755 --- a/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile @@ -33,7 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile b/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile index 28aab7a1..175a6594 100755 --- a/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile @@ -33,7 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonInit/Makefile b/test/cbmc/proofs/Cellular_CommonInit/Makefile index 5ae9cd86..956dd779 100755 --- a/test/cbmc/proofs/Cellular_CommonInit/Makefile +++ b/test/cbmc/proofs/Cellular_CommonInit/Makefile @@ -32,8 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile index 30946650..fd2d13c7 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile index 7d369e7d..490b9d8b 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile index 60226e58..082e9fe5 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile index 307c1e16..41368897 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile index 37e5fe98..1930c260 100755 --- a/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonRfOff/Makefile b/test/cbmc/proofs/Cellular_CommonRfOff/Makefile index c47810fd..66429427 100755 --- a/test/cbmc/proofs/Cellular_CommonRfOff/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRfOff/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonRfOn/Makefile b/test/cbmc/proofs/Cellular_CommonRfOn/Makefile index 1e1f65c2..29c950c6 100755 --- a/test/cbmc/proofs/Cellular_CommonRfOn/Makefile +++ b/test/cbmc/proofs/Cellular_CommonRfOn/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile index b44be21a..2a2eb9f6 100755 --- a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile @@ -32,7 +32,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile index 9e2659d8..796281e9 100755 --- a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile @@ -33,7 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile index bd74d0bd..3a3ae5fb 100755 --- a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile @@ -33,7 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile index d320703a..37a23512 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile index 687dacbb..0e940312 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile index 4012b6ae..e7ade9bb 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile b/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile index 323aab9b..47699524 100755 --- a/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile @@ -43,8 +43,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile index 822b5225..4ff2b620 100755 --- a/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile +++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile @@ -50,8 +50,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile index 1fd45f28..8665f417 100755 --- a/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile +++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile @@ -50,8 +50,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile index d6b32011..09a28aff 100755 --- a/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile +++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile @@ -42,8 +42,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_GenericCallback/Makefile b/test/cbmc/proofs/_Cellular_GenericCallback/Makefile index 27a89549..6f9f6b4a 100755 --- a/test/cbmc/proofs/_Cellular_GenericCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_GenericCallback/Makefile @@ -33,8 +33,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile b/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile index f7c50835..391cb389 100755 --- a/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile +++ b/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile b/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile index 4aec13c7..cb8c66cc 100755 --- a/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile +++ b/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile @@ -42,8 +42,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_GetSocketData/Makefile b/test/cbmc/proofs/_Cellular_GetSocketData/Makefile index 9ebb6887..32b7b90e 100755 --- a/test/cbmc/proofs/_Cellular_GetSocketData/Makefile +++ b/test/cbmc/proofs/_Cellular_GetSocketData/Makefile @@ -40,7 +40,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile b/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile index f0630d37..dcdbd640 100755 --- a/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile +++ b/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile @@ -40,11 +40,8 @@ UNWINDSET += _Cellular_CreateSocketData.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -OOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c - PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c b/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c index 708059e4..0d7c21c8 100644 --- a/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c +++ b/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c @@ -26,6 +26,7 @@ #include /* Cellular APIs includes. */ +#include "cellular_platform.h" #include "cellular_config_defaults.h" #include "cellular_types.h" #include "cellular_common_internal.h" diff --git a/test/cbmc/proofs/_Cellular_LibCleanup/Makefile b/test/cbmc/proofs/_Cellular_LibCleanup/Makefile index b85390e4..2a98bd73 100755 --- a/test/cbmc/proofs/_Cellular_LibCleanup/Makefile +++ b/test/cbmc/proofs/_Cellular_LibCleanup/Makefile @@ -41,8 +41,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile b/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile index 27679012..65f93510 100755 --- a/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile @@ -41,8 +41,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile b/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile index 48c52573..b29481ce 100755 --- a/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile @@ -41,8 +41,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile b/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile index 24a8aa57..262e6501 100755 --- a/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile @@ -41,8 +41,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile index f3d8aeb7..f92eee4f 100755 --- a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile +++ b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile @@ -44,8 +44,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile b/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile index e234a044..0cc3c594 100755 --- a/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile @@ -41,8 +41,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_urc_handler.c diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile index 2c73cf76..30d86fbf 100755 --- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile @@ -42,10 +42,8 @@ PROJECT_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c -ROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pktio.c include ../Makefile.common diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile index fa084dfd..ff8ea82c 100755 --- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile +++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile @@ -43,10 +43,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pktio.c include ../Makefile.common diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile index 686bdca0..8820fe63 100755 --- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile +++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile @@ -37,8 +37,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c -PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c diff --git a/test/cbmc/proofs/cbmc_build.sh b/test/cbmc/proofs/cbmc_build.sh new file mode 100755 index 00000000..43333f35 --- /dev/null +++ b/test/cbmc/proofs/cbmc_build.sh @@ -0,0 +1,14 @@ +#!/bin/bash +PWD=$(/usr/bin/pwd) +# dir=$(find . -mindepth 1 -maxdepth 1 -type d) +# $echo dir +echo $PWD +for D in *; do + if [ -d "${D}" ]; then + echo "process folder ${D}" # your processing here + cd ${D} + make clean && make report + cd .. + fi +done +cd $PWD diff --git a/test/cbmc/proofs/cbmc_clean.sh b/test/cbmc/proofs/cbmc_clean.sh new file mode 100755 index 00000000..32ee039b --- /dev/null +++ b/test/cbmc/proofs/cbmc_clean.sh @@ -0,0 +1,14 @@ +#!/bin/bash +PWD=$(/usr/bin/pwd) +# dir=$(find . -mindepth 1 -maxdepth 1 -type d) +# $echo dir +echo $PWD +for D in *; do + if [ -d "${D}" ]; then + echo "process folder ${D}" # your processing here + cd ${D} + make clean + cd .. + fi +done +cd $PWD diff --git a/test/cbmc/sources/cellular_platform.c b/test/cbmc/sources/cellular_platform.c index 19a09458..b9d53c7f 100644 --- a/test/cbmc/sources/cellular_platform.c +++ b/test/cbmc/sources/cellular_platform.c @@ -54,4 +54,121 @@ bool MockPlatformMutex_Create( PlatformMutex_t * pNewMutex, return true; } +int32_t MockPlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupEvent, + EventBits_t event, + BaseType_t * pHigherPriorityTaskWoken ) +{ + bool flag = nondet_bool(); + int32_t ret; + + ( void ) groupEvent; + ( void ) event; + ( void ) pHigherPriorityTaskWoken; + + + if( flag ){ + if( nondet_bool() ) + { + *pHigherPriorityTaskWoken = pdTRUE; + } + else + { + *pHigherPriorityTaskWoken = pdFALSE; + } + + ret = pdPASS; + } + else + { + ret = pdFALSE; + } + + return ret; +} + /* ========================================================================== */ + +QueueHandle_t MockxQueueCreate( int32_t uxQueueLength, + uint32_t uxItemSize ) +{ + ( void ) uxQueueLength; + ( void ) uxItemSize; + + if( nondet_bool() ) + { + QueueHandle_t test = malloc( sizeof( struct QueueDefinition ) ); + return test; + } + + return NULL; +} + + +uint16_t MockvQueueDelete( QueueHandle_t queue ) +{ + free( queue ); + queue = 0; + return 1; +} + +BaseType_t MockxQueueSend( QueueHandle_t queue, + void * data, + uint32_t time ) +{ + ( void ) queue; + ( void ) time; + + if( nondet_bool() ) + { + return true; + } + else + { + return false; + } +} + +/* ========================================================================== */ + + +uint16_t MockPlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup, + TickType_t uxBitsToClear ) +{ + ( void ) xEventGroup; + ( void ) uxBitsToClear; + return 0; +} + +bool MockPlatform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ), + void * pArgument, + size_t priority, + size_t stackSize ) +{ + ( void ) pArgument; + ( void ) priority; + ( void ) stackSize; + + bool threadReturn = nondet_bool(); + + if( threadReturn ) + { + threadRoutine( pArgument ); + } + + return threadReturn; +} + +uint16_t MockPlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent ) +{ + ( void ) groupEvent; + return 0U; +} + +uint16_t MockPlatformEventGroup_GetBits( PlatformEventGroupHandle_t groupEvent ) +{ + ( void ) groupEvent; + + uint16_t ret = nondet_unsigned_int(); + + return ret; +} diff --git a/test/cbmc/stubs/bsearch.c b/test/cbmc/stubs/bsearch.c new file mode 100644 index 00000000..4731bd06 --- /dev/null +++ b/test/cbmc/stubs/bsearch.c @@ -0,0 +1,52 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file bsearch.c + * @brief Creates a stub for bsearch. This stub checks if, for the input copy + * length, the destination and source are valid accessible memory. + */ + +#include + +void * bsearch ( const void *key, + const void *base, + size_t num, + size_t size, + int (*compar)(const void*,const void*) ) +{ + int offset = nondet_size_t(); + char *p = (char*) base; + + (void) key; + (void) base; + + if( offset >=0 && offset < num ) + { + return (void*) (p+(offset*size)); + } + + return NULL; +} diff --git a/test/cbmc/stubs/snprintf.c b/test/cbmc/stubs/snprintf.c new file mode 100644 index 00000000..23973ac4 --- /dev/null +++ b/test/cbmc/stubs/snprintf.c @@ -0,0 +1,42 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file snprintf.c + * @brief Creates a stub for snprintf. This stub checks if, for the input copy + * length, the destination and source are valid accessible memory. + */ + +#include + +int snprintf ( char * s, + size_t n, + const char * format, + ... ) +{ + __CPROVER_assert( __CPROVER_w_ok( s, n ), "write" ); + __CPROVER_assert( __CPROVER_r_ok( s, n ), "read" ); + return n; +} diff --git a/test/cbmc/stubs/strnlen.c b/test/cbmc/stubs/strnlen.c index a351133a..aa69cdf0 100644 --- a/test/cbmc/stubs/strnlen.c +++ b/test/cbmc/stubs/strnlen.c @@ -34,9 +34,16 @@ size_t strnlen( const char *s, size_t n ) { - size_t ret=nondet_size_t(); - __CPROVER_assume( ret <= n ); - __CPROVER_assert( __CPROVER_w_ok( s, n ), "write" ); - __CPROVER_assert( __CPROVER_r_ok( s, n ), "read" ); + size_t ret=0; + char *pS=s; + + while( *pS && ret < n ){ + pS++; + ret++; + + __CPROVER_assert( __CPROVER_w_ok( pS, 1 ), "write" ); + __CPROVER_assert( __CPROVER_r_ok( pS, 1 ), "read" ); + } + return ret; } diff --git a/test/cbmc/stubs/strstr.c b/test/cbmc/stubs/strstr.c new file mode 100644 index 00000000..d81297c0 --- /dev/null +++ b/test/cbmc/stubs/strstr.c @@ -0,0 +1,48 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file strstr.c + * @brief Creates a stub for strstr. This stub checks if, for the input copy + * length, the destination and source are valid accessible memory. + */ + +#include + +char *strstr( const char *s1, + const char *s2 ) +{ + size_t offset = nondet_size_t(); + __CPROVER_assert( __CPROVER_w_ok( s1, strlen( s1 ) ), "s1 write" ); + __CPROVER_assert( __CPROVER_r_ok( s1, strlen( s1 ) ), "s1 read" ); + + __CPROVER_assert( __CPROVER_w_ok( s2, strlen( s2 ) ), "s2 write" ); + __CPROVER_assert( __CPROVER_r_ok( s2, strlen( s2 ) ), "s2 read" ); + + if( offset >= 0 && offset < strlen(s1) ){ + return s1+offset; + } + return NULL; +} diff --git a/test/cbmc/stubs/strtok.c b/test/cbmc/stubs/strtok.c index 3a82e41e..4e17ce61 100644 --- a/test/cbmc/stubs/strtok.c +++ b/test/cbmc/stubs/strtok.c @@ -29,6 +29,7 @@ * length, the destination and source are valid accessible memory. */ +#include #include /* This is a clang macro not available on linux */ @@ -67,3 +68,24 @@ return s; } #endif /* if __has_builtin( __builtin___strchr ) */ + +char *strtok_r( char *restrict s, + const char *restrict sep, + char **restrict lasts ) +{ + size_t offset = nondet_size_t(); + + (void) s; + (void) sep; + (void) lasts; + + __CPROVER_assert( __CPROVER_w_ok( s, strlen( s ) ), "write" ); + __CPROVER_assert( __CPROVER_r_ok( s, strlen( s ) ), "read" ); + + if( offset>=0 && offset < strlen(s) ) + { + return s+offset; + } + + return NULL; +} From 5bfde81b4aed0edf7db1a695bb0ae68b0b1f94a1 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Wed, 1 Dec 2021 02:59:10 +0000 Subject: [PATCH 03/11] all verification pass --- test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile | 1 + test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile | 1 + test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile | 1 + test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile | 1 + test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile | 1 + test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile | 1 + test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile | 1 + test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile | 1 + test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile | 1 + test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile | 1 + test/cbmc/proofs/Cellular_ATStrDup/Makefile | 1 + test/cbmc/proofs/Cellular_ATStrStartWith/Makefile | 1 + test/cbmc/proofs/Cellular_ATStrtoi/Makefile | 1 + test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile | 1 + 14 files changed, 14 insertions(+) diff --git a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile index 58e4eb4c..0ced0201 100755 --- a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile +++ b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATGetSpecificNextTok.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c diff --git a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile index a2879aa0..e8201dca 100755 --- a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile +++ b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATHexStrToHex.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile b/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile index 8ede9fa7..e1bafa2b 100755 --- a/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile +++ b/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile @@ -35,6 +35,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATIsPrefixPresent.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile index 5bd957d0..87bd886c 100755 --- a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile +++ b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATIsStrDigit.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile index 91d8478e..9b9abd8f 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveAllDoubleQuote.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile index 091560f3..778037fe 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveAllWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile index 92e0e3bd..2d1f0709 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile @@ -33,6 +33,7 @@ CBMC_MAX_BUFSIZE=128 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveLeadingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile index de0bbebd..3f315deb 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveOutermostDoubleQuote.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile index 7f834332..759bc8c4 100755 --- a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile @@ -31,6 +31,7 @@ INCLUDES += CBMC_MAX_BUFSIZE=256 UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile index 239e5b7b..a59ab0a1 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveTrailingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATStrDup/Makefile b/test/cbmc/proofs/Cellular_ATStrDup/Makefile index af04eced..0c496102 100755 --- a/test/cbmc/proofs/Cellular_ATStrDup/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrDup/Makefile @@ -34,6 +34,7 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATStrDup.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c diff --git a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile index e766157c..bd5bb0cb 100755 --- a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile @@ -33,6 +33,7 @@ CBMC_MAX_BUFSIZE=256 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATStrStartWith.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c diff --git a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile index a6a3ec33..f214bfa3 100755 --- a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile @@ -33,6 +33,7 @@ CBMC_MAX_BUFSIZE=32 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += strtol.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c diff --git a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile index 4421dfd7..43fa213b 100755 --- a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile +++ b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile @@ -35,6 +35,7 @@ KEY_LIST_SIZE=16 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) -DKEY_LIST_SIZE=$(KEY_LIST_SIZE) UNWINDSET += Cellular_ATcheckErrorCode.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) # This API has its own CBMC test case. REMOVE_FUNCTION_BODY += Cellular_ATStrStartWith From 298289a7d0d905e2381049d86902c3a3612c8b52 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Thu, 2 Dec 2021 02:39:25 +0000 Subject: [PATCH 04/11] fix snprintf warning --- test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile | 1 + test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile | 1 + test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile | 1 + test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile | 1 + 4 files changed, 4 insertions(+) diff --git a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile index b14714dd..c5d33ae1 100755 --- a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile +++ b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile @@ -32,6 +32,7 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/snprintf.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile index 2a2eb9f6..54401a96 100755 --- a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile @@ -32,6 +32,7 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/snprintf.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile index 796281e9..2e224e29 100755 --- a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile @@ -31,6 +31,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/snprintf.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c diff --git a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile index 3a3ae5fb..cb7c34a2 100755 --- a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile +++ b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile @@ -31,6 +31,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/snprintf.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c From 7451c45daf6099275e13a1b51c16ce8ea05cae65 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Fri, 3 Dec 2021 05:22:35 +0000 Subject: [PATCH 05/11] replace strnlen with memchr --- .../Cellular_ATGetSpecificNextTok/Makefile | 4 +- .../proofs/Cellular_ATHexStrToHex/Makefile | 4 +- .../proofs/Cellular_ATIsStrDigit/Makefile | 4 +- .../Cellular_ATRemoveAllDoubleQuote/Makefile | 4 +- .../Cellular_ATRemoveAllWhiteSpaces/Makefile | 4 +- .../Makefile | 4 +- .../Makefile | 4 +- .../proofs/Cellular_ATRemovePrefix/Makefile | 4 +- .../Makefile | 4 +- test/cbmc/proofs/Cellular_ATStrDup/Makefile | 4 +- .../proofs/Cellular_ATStrStartWith/Makefile | 4 +- test/cbmc/proofs/Cellular_ATStrtoi/Makefile | 4 +- .../proofs/Cellular_ATcheckErrorCode/Makefile | 4 +- test/cbmc/stubs/memchr.c | 53 +++++++++++++++++++ 14 files changed, 79 insertions(+), 26 deletions(-) create mode 100644 test/cbmc/stubs/memchr.c diff --git a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile index 0ced0201..ac03fc07 100755 --- a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile +++ b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATGetSpecificNextTok.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c diff --git a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile index e8201dca..cf369c9e 100755 --- a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile +++ b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATHexStrToHex.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile index 87bd886c..65c33ba4 100755 --- a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile +++ b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATIsStrDigit.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile index 9b9abd8f..dfaaad08 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveAllDoubleQuote.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile index 778037fe..4bf70091 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveAllWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile index 2d1f0709..3a712570 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile @@ -33,13 +33,13 @@ CBMC_MAX_BUFSIZE=128 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveLeadingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile index 3f315deb..3c785b20 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveOutermostDoubleQuote.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile index 759bc8c4..7b6c0957 100755 --- a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile @@ -31,14 +31,14 @@ INCLUDES += CBMC_MAX_BUFSIZE=256 UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile index a59ab0a1..92c1b24d 100755 --- a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATRemoveTrailingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATStrDup/Makefile b/test/cbmc/proofs/Cellular_ATStrDup/Makefile index 0c496102..fa235f45 100755 --- a/test/cbmc/proofs/Cellular_ATStrDup/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrDup/Makefile @@ -34,13 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATStrDup.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c diff --git a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile index bd5bb0cb..8eedfc7d 100755 --- a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile @@ -33,14 +33,14 @@ CBMC_MAX_BUFSIZE=256 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += Cellular_ATStrStartWith.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile index f214bfa3..82bbd7c7 100755 --- a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile +++ b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile @@ -33,12 +33,12 @@ CBMC_MAX_BUFSIZE=32 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) UNWINDSET += strtol.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c PROJECT_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtol.c diff --git a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile index 43fa213b..bb327fe0 100755 --- a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile +++ b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile @@ -35,7 +35,7 @@ KEY_LIST_SIZE=16 DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) -DKEY_LIST_SIZE=$(KEY_LIST_SIZE) UNWINDSET += Cellular_ATcheckErrorCode.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE) +UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) # This API has its own CBMC test case. REMOVE_FUNCTION_BODY += Cellular_ATStrStartWith @@ -44,7 +44,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c -PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c include ../Makefile.common diff --git a/test/cbmc/stubs/memchr.c b/test/cbmc/stubs/memchr.c new file mode 100644 index 00000000..3e82da7a --- /dev/null +++ b/test/cbmc/stubs/memchr.c @@ -0,0 +1,53 @@ +/* + * FreeRTOS-Cellular-Interface v1.1.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + */ + +/** + * @file strtok.c + * @brief Creates a stub for strtok. This stub checks if, for the input copy + * length, the destination and source are valid accessible memory. + */ + +#include + +void *memchr( void * ptr, + int value, + size_t num ) +{ + //to avoid unwind assertion on CBMC, use a constant loop time to enhance CBMC performance + int n = CBMC_MAX_BUFSIZE; + char *p = (char*)ptr; + + while( n-- && p!=NULL ) + { + if( *p == (char)value ) + { + return p; + } + p++; + } + + return NULL; +} + From 4ec1f2fbfa934c95f63fec413c50ba1f44956725 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Fri, 3 Dec 2021 05:42:17 +0000 Subject: [PATCH 06/11] wrap useless input --- test/cbmc/stubs/memchr.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/cbmc/stubs/memchr.c b/test/cbmc/stubs/memchr.c index 3e82da7a..93f44222 100644 --- a/test/cbmc/stubs/memchr.c +++ b/test/cbmc/stubs/memchr.c @@ -39,6 +39,8 @@ void *memchr( void * ptr, int n = CBMC_MAX_BUFSIZE; char *p = (char*)ptr; + ( void ) num; + while( n-- && p!=NULL ) { if( *p == (char)value ) From ec7c5d59a031f241b94d72a659a8584793cba3ad Mon Sep 17 00:00:00 2001 From: ActoryOu Date: Fri, 3 Dec 2021 06:43:41 +0000 Subject: [PATCH 07/11] fix format check --- test/cbmc/include/cellular_platform.h | 12 ++++++------ test/cbmc/sources/cellular_modules.c | 20 ++++++++++++-------- test/cbmc/sources/cellular_platform.c | 24 ++++++++++++------------ test/cbmc/stubs/bsearch.c | 20 ++++++++++---------- test/cbmc/stubs/memchr.c | 16 ++++++++-------- test/cbmc/stubs/snprintf.c | 10 +++++----- test/cbmc/stubs/strnlen.c | 13 +++++++------ test/cbmc/stubs/strstr.c | 11 +++++++---- test/cbmc/stubs/strtok.c | 16 ++++++++-------- 9 files changed, 75 insertions(+), 67 deletions(-) diff --git a/test/cbmc/include/cellular_platform.h b/test/cbmc/include/cellular_platform.h index b459c013..7b620c57 100644 --- a/test/cbmc/include/cellular_platform.h +++ b/test/cbmc/include/cellular_platform.h @@ -114,8 +114,8 @@ typedef void * PVOID; * * \defgroup EventBits_t EventBits_t * \ingroup EventGroup - */ -typedef TickType_t EventBits_t; + */ +typedef TickType_t EventBits_t; /** * @brief Cellular library platform thread API and configuration. @@ -215,11 +215,11 @@ QueueHandle_t xQueueCreate( int32_t uxQueueLength, uint32_t uxItemSize ); uint16_t vQueueDelete( QueueHandle_t queue ); BaseType_t xQueueSend( QueueHandle_t queue, - void * data, - uint32_t time ); + void * data, + uint32_t time ); -uint16_t PlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup, - TickType_t uxBitsToClear ); +uint16_t PlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup, + TickType_t uxBitsToClear ); uint16_t PlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent ); uint16_t PlatformEventGroup_GetBits( PlatformEventGroupHandle_t groupEvent ); diff --git a/test/cbmc/sources/cellular_modules.c b/test/cbmc/sources/cellular_modules.c index a68d872f..7fab419a 100644 --- a/test/cbmc/sources/cellular_modules.c +++ b/test/cbmc/sources/cellular_modules.c @@ -34,32 +34,36 @@ CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext, void ** ppModuleContext ) { - CellularError_t ret=nondet_int(); - __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + CellularError_t ret = nondet_int(); + + __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN ); return ret; } CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext ) { - CellularError_t ret=nondet_int(); - __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + CellularError_t ret = nondet_int(); + + __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN ); return ret; } CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext ) { - CellularError_t ret=nondet_int(); - __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + CellularError_t ret = nondet_int(); + + __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN ); return ret; } CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext ) { - CellularError_t ret=nondet_int(); - __CPROVER_assume( ret>=CELLULAR_SUCCESS && ret<=CELLULAR_UNKNOWN ); + CellularError_t ret = nondet_int(); + + __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN ); return ret; } diff --git a/test/cbmc/sources/cellular_platform.c b/test/cbmc/sources/cellular_platform.c index b9d53c7f..52b5bd05 100644 --- a/test/cbmc/sources/cellular_platform.c +++ b/test/cbmc/sources/cellular_platform.c @@ -65,8 +65,8 @@ int32_t MockPlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupE ( void ) event; ( void ) pHigherPriorityTaskWoken; - - if( flag ){ + if( flag ) + { if( nondet_bool() ) { *pHigherPriorityTaskWoken = pdTRUE; @@ -77,7 +77,7 @@ int32_t MockPlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupE } ret = pdPASS; - } + } else { ret = pdFALSE; @@ -99,7 +99,7 @@ QueueHandle_t MockxQueueCreate( int32_t uxQueueLength, QueueHandle_t test = malloc( sizeof( struct QueueDefinition ) ); return test; } - + return NULL; } @@ -131,18 +131,18 @@ BaseType_t MockxQueueSend( QueueHandle_t queue, /* ========================================================================== */ -uint16_t MockPlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup, - TickType_t uxBitsToClear ) +uint16_t MockPlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup, + TickType_t uxBitsToClear ) { ( void ) xEventGroup; ( void ) uxBitsToClear; return 0; } -bool MockPlatform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ), - void * pArgument, - size_t priority, - size_t stackSize ) +bool MockPlatform_CreateDetachedThread( void ( *threadRoutine )( void * pArgument ), + void * pArgument, + size_t priority, + size_t stackSize ) { ( void ) pArgument; ( void ) priority; @@ -156,8 +156,8 @@ bool MockPlatform_CreateDetachedThread( void ( * threadRoutine )( void * pArgume } return threadReturn; -} - +} + uint16_t MockPlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent ) { ( void ) groupEvent; diff --git a/test/cbmc/stubs/bsearch.c b/test/cbmc/stubs/bsearch.c index 4731bd06..caa2dac5 100644 --- a/test/cbmc/stubs/bsearch.c +++ b/test/cbmc/stubs/bsearch.c @@ -31,21 +31,21 @@ #include -void * bsearch ( const void *key, - const void *base, - size_t num, - size_t size, - int (*compar)(const void*,const void*) ) +void * bsearch( const void * key, + const void * base, + size_t num, + size_t size, + int ( *compar )( const void *, const void * ) ) { int offset = nondet_size_t(); - char *p = (char*) base; + char * p = ( char * ) base; - (void) key; - (void) base; + ( void ) key; + ( void ) base; - if( offset >=0 && offset < num ) + if( ( offset >= 0 ) && ( offset < num ) ) { - return (void*) (p+(offset*size)); + return ( void * ) ( p + ( offset * size ) ); } return NULL; diff --git a/test/cbmc/stubs/memchr.c b/test/cbmc/stubs/memchr.c index 93f44222..7a32b99d 100644 --- a/test/cbmc/stubs/memchr.c +++ b/test/cbmc/stubs/memchr.c @@ -31,25 +31,25 @@ #include -void *memchr( void * ptr, - int value, - size_t num ) +void * memchr( void * ptr, + int value, + size_t num ) { - //to avoid unwind assertion on CBMC, use a constant loop time to enhance CBMC performance + /*to avoid unwind assertion on CBMC, use a constant loop time to enhance CBMC performance */ int n = CBMC_MAX_BUFSIZE; - char *p = (char*)ptr; + char * p = ( char * ) ptr; ( void ) num; - while( n-- && p!=NULL ) + while( n-- && p != NULL ) { - if( *p == (char)value ) + if( *p == ( char ) value ) { return p; } + p++; } return NULL; } - diff --git a/test/cbmc/stubs/snprintf.c b/test/cbmc/stubs/snprintf.c index 23973ac4..bfb992e2 100644 --- a/test/cbmc/stubs/snprintf.c +++ b/test/cbmc/stubs/snprintf.c @@ -29,12 +29,12 @@ * length, the destination and source are valid accessible memory. */ -#include +#include -int snprintf ( char * s, - size_t n, - const char * format, - ... ) +int snprintf( char * s, + size_t n, + const char * format, + ... ) { __CPROVER_assert( __CPROVER_w_ok( s, n ), "write" ); __CPROVER_assert( __CPROVER_r_ok( s, n ), "read" ); diff --git a/test/cbmc/stubs/strnlen.c b/test/cbmc/stubs/strnlen.c index aa69cdf0..fa6436aa 100644 --- a/test/cbmc/stubs/strnlen.c +++ b/test/cbmc/stubs/strnlen.c @@ -31,16 +31,17 @@ #include -size_t strnlen( const char *s, - size_t n ) +size_t strnlen( const char * s, + size_t n ) { - size_t ret=0; - char *pS=s; + size_t ret = 0; + char * pS = s; - while( *pS && ret < n ){ + while( *pS && ret < n ) + { pS++; ret++; - + __CPROVER_assert( __CPROVER_w_ok( pS, 1 ), "write" ); __CPROVER_assert( __CPROVER_r_ok( pS, 1 ), "read" ); } diff --git a/test/cbmc/stubs/strstr.c b/test/cbmc/stubs/strstr.c index d81297c0..01303d0d 100644 --- a/test/cbmc/stubs/strstr.c +++ b/test/cbmc/stubs/strstr.c @@ -31,18 +31,21 @@ #include -char *strstr( const char *s1, - const char *s2 ) +char * strstr( const char * s1, + const char * s2 ) { size_t offset = nondet_size_t(); + __CPROVER_assert( __CPROVER_w_ok( s1, strlen( s1 ) ), "s1 write" ); __CPROVER_assert( __CPROVER_r_ok( s1, strlen( s1 ) ), "s1 read" ); __CPROVER_assert( __CPROVER_w_ok( s2, strlen( s2 ) ), "s2 write" ); __CPROVER_assert( __CPROVER_r_ok( s2, strlen( s2 ) ), "s2 read" ); - if( offset >= 0 && offset < strlen(s1) ){ - return s1+offset; + if( ( offset >= 0 ) && ( offset < strlen( s1 ) ) ) + { + return s1 + offset; } + return NULL; } diff --git a/test/cbmc/stubs/strtok.c b/test/cbmc/stubs/strtok.c index 4e17ce61..b81350fe 100644 --- a/test/cbmc/stubs/strtok.c +++ b/test/cbmc/stubs/strtok.c @@ -69,22 +69,22 @@ } #endif /* if __has_builtin( __builtin___strchr ) */ -char *strtok_r( char *restrict s, - const char *restrict sep, - char **restrict lasts ) +char * strtok_r( char * restrict s, + const char * restrict sep, + char ** restrict lasts ) { size_t offset = nondet_size_t(); - (void) s; - (void) sep; - (void) lasts; + ( void ) s; + ( void ) sep; + ( void ) lasts; __CPROVER_assert( __CPROVER_w_ok( s, strlen( s ) ), "write" ); __CPROVER_assert( __CPROVER_r_ok( s, strlen( s ) ), "read" ); - if( offset>=0 && offset < strlen(s) ) + if( ( offset >= 0 ) && ( offset < strlen( s ) ) ) { - return s+offset; + return s + offset; } return NULL; From 42951eacd93c0eeab71849cf67c1b3557cfd7deb Mon Sep 17 00:00:00 2001 From: ActoryOu Date: Fri, 3 Dec 2021 06:45:46 +0000 Subject: [PATCH 08/11] add strstr to avoid spelling check --- lexicon.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/lexicon.txt b/lexicon.txt index b4572209..64462cad 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -774,6 +774,7 @@ stringlength strlen strncpy strnlen +strstr strtok strtol struct From 7cca5cf8758006ffc59719cba5ad102d51ebdf91 Mon Sep 17 00:00:00 2001 From: ActoryOu Date: Fri, 3 Dec 2021 07:23:26 +0000 Subject: [PATCH 09/11] fix 0.69 uncrustify --- test/cbmc/sources/cellular_platform.c | 2 +- test/cbmc/stubs/bsearch.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test/cbmc/sources/cellular_platform.c b/test/cbmc/sources/cellular_platform.c index 52b5bd05..c9e1adb0 100644 --- a/test/cbmc/sources/cellular_platform.c +++ b/test/cbmc/sources/cellular_platform.c @@ -139,7 +139,7 @@ uint16_t MockPlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGrou return 0; } -bool MockPlatform_CreateDetachedThread( void ( *threadRoutine )( void * pArgument ), +bool MockPlatform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ), void * pArgument, size_t priority, size_t stackSize ) diff --git a/test/cbmc/stubs/bsearch.c b/test/cbmc/stubs/bsearch.c index caa2dac5..b3ef36e1 100644 --- a/test/cbmc/stubs/bsearch.c +++ b/test/cbmc/stubs/bsearch.c @@ -35,7 +35,7 @@ void * bsearch( const void * key, const void * base, size_t num, size_t size, - int ( *compar )( const void *, const void * ) ) + int ( * compar )( const void *, const void * ) ) { int offset = nondet_size_t(); char * p = ( char * ) base; From bcb35f650c73ee0b977c4dd1e5070570743395e4 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Fri, 3 Dec 2021 08:23:50 +0000 Subject: [PATCH 10/11] fix CBMC build error --- test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile index 7b6c0957..98520cf2 100755 --- a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile +++ b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile @@ -30,6 +30,8 @@ INCLUDES += # without tripping unwinding assertions and without exhausting memory. CBMC_MAX_BUFSIZE=256 +DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) + UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE) UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE) From be0f2c0d81c6bf0f73deb86e55bf53f2ef869451 Mon Sep 17 00:00:00 2001 From: Actory Ou Date: Mon, 6 Dec 2021 04:17:03 +0000 Subject: [PATCH 11/11] remove test scripts --- test/cbmc/proofs/cbmc_build.sh | 14 -------------- test/cbmc/proofs/cbmc_clean.sh | 14 -------------- 2 files changed, 28 deletions(-) delete mode 100755 test/cbmc/proofs/cbmc_build.sh delete mode 100755 test/cbmc/proofs/cbmc_clean.sh diff --git a/test/cbmc/proofs/cbmc_build.sh b/test/cbmc/proofs/cbmc_build.sh deleted file mode 100755 index 43333f35..00000000 --- a/test/cbmc/proofs/cbmc_build.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/bash -PWD=$(/usr/bin/pwd) -# dir=$(find . -mindepth 1 -maxdepth 1 -type d) -# $echo dir -echo $PWD -for D in *; do - if [ -d "${D}" ]; then - echo "process folder ${D}" # your processing here - cd ${D} - make clean && make report - cd .. - fi -done -cd $PWD diff --git a/test/cbmc/proofs/cbmc_clean.sh b/test/cbmc/proofs/cbmc_clean.sh deleted file mode 100755 index 32ee039b..00000000 --- a/test/cbmc/proofs/cbmc_clean.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/bash -PWD=$(/usr/bin/pwd) -# dir=$(find . -mindepth 1 -maxdepth 1 -type d) -# $echo dir -echo $PWD -for D in *; do - if [ -d "${D}" ]; then - echo "process folder ${D}" # your processing here - cd ${D} - make clean - cd .. - fi -done -cd $PWD