Project

General

Profile

Download (512 Bytes)

Bug #10024 » is_successorless_vertex.c

Denis Efremov, 01/09/2020 07:23 PM

 
#include <stdbool.h>
#include "graph.h"

/*@ requires \valid(g);
requires \valid(g->adj_list_arr + (0..g->num_vertices-1));
requires 0 <= v < g->num_vertices;
*/
static inline bool is_successorless_vertex(const graph_t *g, int v)
{
return !g->adj_list_arr[v].head;
}

/*@ requires \valid(g);
requires \valid(g->adj_list_arr + (0..g->num_vertices-1));
requires 0 <= v < g->num_vertices;
*/
static inline bool is_successorful_vertex(const graph_t *g, int v)
{
return g->adj_list_arr[v].head;
}
(1-1/2)