mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-16 09:47:44 -04:00
cb7edd2323
* AFR sync * AFR sync: CBMC * AFR sync: CBMC: remove .bak files * AFR sync: CBMC: more cleanup * Corrected CBMC proofs * Corrected CBMC patches * Corrected CBMC patches-1 * Corrected CBMC patches-2 * remove .bak files (3) Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
37 lines
1 KiB
C
37 lines
1 KiB
C
/* Standard includes. */
|
|
#include <stdint.h>
|
|
|
|
/* FreeRTOS includes. */
|
|
#include "FreeRTOS.h"
|
|
#include "task.h"
|
|
#include "semphr.h"
|
|
|
|
/* FreeRTOS+TCP includes. */
|
|
#include "FreeRTOS_IP.h"
|
|
#include "FreeRTOS_Sockets.h"
|
|
#include "FreeRTOS_IP_Private.h"
|
|
#include "FreeRTOS_UDP_IP.h"
|
|
#include "FreeRTOS_DHCP.h"
|
|
#include "FreeRTOS_ARP.h"
|
|
|
|
|
|
/****************************************************************
|
|
* Signature of function under test
|
|
****************************************************************/
|
|
|
|
BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
|
|
|
|
/****************************************************************
|
|
* 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;
|
|
|
|
prvProcessDHCPReplies( xExpectedMessageType );
|
|
}
|