Project

General

Profile

Bug #10024 » graph.h

Denis Efremov, 01/09/2020 07:23 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
(2-2/2)