xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c (revision 2d3f4daa567ffe71aeda2e0f6d0bc02850db0627) 
1 /*
2  * FreeRTOS memory safety proofs with CBMC.
3  * Copyright (C) 2022 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
4  *
5  * Permission is hereby granted, free of charge, to any person
6  * obtaining a copy of this software and associated documentation
7  * files (the "Software"), to deal in the Software without
8  * restriction, including without limitation the rights to use, copy,
9  * modify, merge, publish, distribute, sublicense, and/or sell copies
10  * of the Software, and to permit persons to whom the Software is
11  * furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be
14  * included in all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
17  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
18  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
19  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
20  * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
21  * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
22  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
23  * SOFTWARE.
24  *
25  * http://aws.amazon.com/freertos
26  * http://www.FreeRTOS.org
27  */
28 
29 /* FreeRTOS includes. */
30 #include "FreeRTOS.h"
31 #include "queue.h"
32 
33 /* FreeRTOS+TCP includes. */
34 #include "FreeRTOS_IP.h"
35 #include "FreeRTOS_IP_Private.h"
36 #include "FreeRTOS_ND.h"
37 
38 /* CBMC includes. */
39 #include "../../utility/memory_assignments.c"
40 #include "cbmc.h"
41 
harness()42 void harness()
43 {
44     NetworkInterface_t * pxNetworkInterface = safeMalloc( sizeof( NetworkInterface_t ) );
45     uint8_t * pcNetworkBuffer = safeMalloc( sizeof( ProtocolPacket_t ) + 4 );
46     ProtocolPacket_t * pxProtocolPacket;
47 
48     __CPROVER_assume( pcNetworkBuffer != NULL );
49 
50     pxProtocolPacket = ( ProtocolPacket_t * ) ( ( uintptr_t ) ( pcNetworkBuffer ) + 2U );
51     __CPROVER_assume( pxProtocolPacket != NULL );
52 
53     /* For this proof, its assumed that the endpoints and interfaces are correctly
54      * initialised and the pointers are set correctly. */
55 
56     pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
57     __CPROVER_assume( pxNetworkEndPoints != NULL );
58 
59     /* Interface init. */
60     pxNetworkEndPoints->pxNetworkInterface = pxNetworkInterface;
61     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
62 
63     if( nondet_bool() )
64     {
65         pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
66         __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
67         pxNetworkEndPoints->pxNext->pxNext = NULL;
68         pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
69     }
70     else
71     {
72         pxNetworkEndPoints->pxNext = NULL;
73     }
74 
75     FreeRTOS_MatchingEndpoint( pxNetworkInterface, ( const uint8_t * ) ( pxProtocolPacket ) );
76 }
77