blob: 5d509a7e838edc4e13bdc17f6bf7c852b93aca6a (
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
This is the memory safety proof for FreeRTOS_OutputARPRequest
method combined with the BufferAllocation_2.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
* pvPortMalloc
* pvPortFree
* xNetworkInterfaceOutput
* vNetworkInterfaceAllocateRAMToBuffers
This proof disables the tracing library in the header.
This proof checks FreeRTOS_OutputARPRequest in multiple configuration:
* The proof in the directory config_minimal_configuration guarantees
that the implementation and interaction between
FreeRTOS_OutputARPRequest and
FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c
are memory save. This proof depends entirely of the implementation
correctness of vNetworkInterfaceAllocateRAMToBuffers.
* The proof in directory minimal_configuration_minimal_packet_size
guarantees that using
FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c
along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save
as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and
ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ).
* The directory minimal_configuration_minimal_packet_size_no_tcp
reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used
if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the
FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c
allocator.
* The proof in directory
config_minimal_configuration_linked_rx_messages guarantees that the
ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the
memory safety claim.
All harnesses include the queue.c file, but test only for the happy path.
|
