⚲
Project
General
Profile
Sign in
Home
Projects
Help
Search
:
Deductive Verification Tools for Linux Kernel
All Projects
AstraVer Toolset
»
Deductive Verification Tools for Linux Kernel
Overview
Activity
Issues
News
Wiki
Files
Repository
Download (1.05 KB)
Bug #10025
» graph.h
Denis Efremov
, 01/09/2020 07:29 PM
#ifndef _GRAPH_H_
#define _GRAPH_H_
#include
<stddef.h>
#include
<stdint.h>
typedef
enum
{
UNDIRECTED
,
DIRECTED
}
graph_type_e
;
/* Adjacency list node*/
typedef
struct
adjlist_node
{
int
vertex
;
/*Index to adjacency list array*/
struct
adjlist_node
*
next
;
/*Pointer to the next node*/
}
adjlist_node_t
;
/* Adjacency list */
typedef
struct
adjlist
{
size_t
num_members
;
/*number of members in the list (for future use)*/
adjlist_node_t
*
head
;
/*head of the adjacency linked list*/
}
adjlist_t
;
/* Graph structure. A graph is an array of adjacency lists.
Size of array will be number of vertices in graph*/
typedef
struct
graph
{
graph_type_e
type
;
/*Directed or undirected graph */
size_t
num_vertices
;
/*Number of vertices*/
adjlist_t
*
adj_list_arr
;
/*Adjacency lists' array*/
}
graph_t
;
/*@ requires \true;
allocates \result;
assigns \nothing;
ensures \valid(\result);
ensures \result->vertex == v;
ensures \result->next == \null;
*/
extern
adjlist_node_t
*
create_node
(
int
v
);
#endif
« Previous
1
2
Next »
(1-1/2)
Loading...