Project

General

Profile

Download (701 Bytes)

Bug #10025 » is_successorless_vertex.c

Denis Efremov, 01/09/2020 07:29 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;

assigns \nothing;

ensures \result <==> (g->adj_list_arr[v].num_members == 0);
*/
static inline bool is_successorless_vertex(const graph_t *g, int v)
{
return !g->adj_list_arr[v].num_members;
}

/*@ requires \valid(g);
requires \valid(g->adj_list_arr + (0..g->num_vertices-1));
requires 0 <= v < g->num_vertices;

assigns \nothing;

ensures \result <==> (g->adj_list_arr[v].num_members > 0);
*/
static inline bool is_successorful_vertex(const graph_t *g, int v)
{
return g->adj_list_arr[v].num_members;
}
(2-2/2)