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