README.md
1This is the memory safety proof for ```FreeRTOS_OutputARPRequest```
2method combined with the BufferAllocation_1.c allocation strategy.
3
4This proof is a work-in-progress. Proof assumptions are described in
5the harness. The proof also assumes the following functions are
6memory safe and have no side effects relevant to the memory safety of
7this function:
8
9* vPortEnterCritical
10* vPortExitCritical
11* vPortGenerateSimulatedInterrupt
12* vAssertCalled
13* xTaskGetSchedulerState
14* pvTaskIncrementMutexHeldCount
15* xTaskRemoveFromEventList
16* xTaskPriorityDisinherit
17
18This proof checks ```FreeRTOS_OutputARPRequest``` in multiple configurations.
19All assume the memory safety of vNetworkInterfaceAllocateRAMToBuffers.
20* The ```config_minimal_configuration``` proof sets
21 ```ipconfigUSE_LINKED_RX_MESSAGES=0```.
22* The ```config_minimal_configuration_linked_rx_messages``` proof sets
23 ```ipconfigUSE_LINKED_RX_MESSAGES=1```.
24* The ```minimal_configuration_minimal_packet_size``` proof sets
25 ```ipconfigETHERNET_MINIMUM_PACKET_BYTES``` to 50.
26
27All harnesses include the queue.c file, but test only for the happy path.
28
