Skip to content

Fix CBMC proof of ProcessDHCPReplies #177

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
Jan 26, 2021
Merged

Fix CBMC proof of ProcessDHCPReplies #177

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
09f77de
Merge pull request #1 from FreeRTOS/labs/ipv6_multi
AniruddhaKanhere Jan 14, 2021
7174bb7
Merge pull request #2 from FreeRTOS/labs/ipv6_multi
AniruddhaKanhere Jan 20, 2021
83d1d8b
Merge pull request #3 from FreeRTOS/labs/ipv6_multi
AniruddhaKanhere Jan 22, 2021
c7f655f
Update Proof
AniruddhaKanhere Jan 26, 2021
177a0f7
Merge branch 'labs/ipv6_multi' into ProcessDHCPReplies
AniruddhaKanhere Jan 26, 2021
37fd23e
Uncrustify and fix one broken proof due to removal of _static
AniruddhaKanhere Jan 26, 2021
f8a870d
Merge branch 'ProcessDHCPReplies' of https://github.com/AniruddhaKanh…
AniruddhaKanhere Jan 26, 2021
5d33b7d
Uncrustify
AniruddhaKanhere Jan 26, 2021
215bfad
Update the comments
AniruddhaKanhere Jan 26, 2021
62aa7a8
Merge branch 'labs/ipv6_multi' into ProcessDHCPReplies
AniruddhaKanhere Jan 26, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions FreeRTOS_DHCP.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,8 +217,8 @@
/*
* Interpret message received on the DHCP socket.
*/
_static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint );
static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint );

/*
* Generate a DHCP request packet, and send it on the DHCP socket.
Expand Down Expand Up @@ -966,8 +966,8 @@
*
* @return pdPASS: if DHCP options are received correctly; pdFAIL: Otherwise.
*/
_static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint )
static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint )
{
uint8_t * pucUDPPayload;
int32_t lBytes;
Expand Down
4 changes: 2 additions & 2 deletions test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,8 +97,8 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
* Function Abstraction:
* prvProcessDHCPReplies has been proved memory safe in ProcessDHCPReplies.
****************************************************************/
BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint )
BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint )
{
return nondet_BaseType();
}
Expand Down
8 changes: 7 additions & 1 deletion test/cbmc/proofs/ProcessDHCPReplies/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
"CBMCFLAGS": [
# "--nondet-static",
"--unwind 1",
"--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
"--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
],

"OBJS":
Expand All @@ -44,5 +44,11 @@
[
"CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",
"CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}"
],

"OPT":
[
# Flag to access the static function of a file
"--export-file-local-symbols"
]
}
19 changes: 14 additions & 5 deletions test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,25 +13,34 @@
#include "FreeRTOS_UDP_IP.h"
#include "FreeRTOS_DHCP.h"
#include "FreeRTOS_ARP.h"

#include "FreeRTOS_Routing.h"

/****************************************************************
* Signature of function under test
* The function name (prvProcessDHCPReplies) is mangled due to the
* use of a CBMC flag (--export-file-local-symbols) which allows us
* to access this static function outside the source file in which
* it is defined.
****************************************************************/

BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
NetworkEndPoint_t * pxEndPoint );

/****************************************************************
* The proof for FreeRTOS_gethostbyname.
****************************************************************/

void harness()
{
/* Omitting model of an unconstrained xDHCPData because xDHCPData is */
/* the source of uninitialized data only on line 647 to set a */
/* transaction id is an outgoing message */

BaseType_t xExpectedMessageType;
NetworkEndPoint_t xEndPoint;

/* The function under test is a private (static) function called only by
* the TCP stack. The stack asserts that the endpoint cannot be NULL
* before the function under test is invoked. */
NetworkEndPoint_t * pxEndPoint = &xEndPoint;
Copy link
Member

@markrtuttle markrtuttle Jan 26, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure this must be nonnull?

Copy link
Member Author

@AniruddhaKanhere AniruddhaKanhere Jan 26, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it must be Non-NULL. I added some comments to make that clear to the reader.


prvProcessDHCPReplies( xExpectedMessageType );
__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxEndPoint );
}