Project

General

Profile

Download (643 Bytes)

Bug #10027 » nlist_init.c

Denis Efremov, 01/10/2020 01:44 AM

 
#include "nlist.h"

/*@
requires \valid(list);
requires ValidArray : \valid( array + (0 .. MAX_SIZE - 1) );

requires GhostSeparation:
\separated(list, array + (0 .. MAX_SIZE - 1));
requires
\separated(*list, array + (0 .. MAX_SIZE - 1));

assigns *list;

ensures ValidArray : \valid( array + (0 .. MAX_SIZE - 1) );

ensures GhostSeparation:
\separated(list, array + (0 .. MAX_SIZE - 1));
ensures
\separated(*list, array + (0 .. MAX_SIZE - 1));

ensures linked_n(*list, array, 0, 0, *list);
ensures *list == NULL;
*/
void
list_init( list_t list,
/* ghost: */ struct list **array)
{
*list = NULL;
}
(10-10/10)