1This is the memory safety proof for DHCPProcess function, which is the
2function that triggers the DHCP protocol.
3
4The main stubs in this proof deal with buffer management, which assume
5that the buffer is large enough to accomodate a DHCP message plus a
6few additional bytes for options (which is the last, variable-sized
7field in a DHCP message). We have abstracted away sockets, concurrency
8and third-party code. For more details, please check the comments on
9the harness file.
10
11This proof is a work-in-progress.  Proof assumptions are described in
12the harness.  The proof also assumes the following functions are
13memory safe and have no side effects relevant to the memory safety of
14this function:
15
16* FreeRTOS_sendto
17* FreeRTOS_setsockopt
18* FreeRTOS_socket
19* ulRand
20* vARPSendGratuitous
21* vApplicationIPNetworkEventHook
22* vLoggingPrintf
23* vPortEnterCritical
24* vPortExitCritical
25* vReleaseNetworkBufferAndDescriptor
26* vSocketBind
27* vSocketClose
28
29