diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c')
-rw-r--r-- | FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c new file mode 100644 index 000000000..ec2fb1c8c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -0,0 +1,37 @@ +/* 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 ); +} |