Project

General

Profile

Download (771 Bytes)

Bug #10021 » list_init.c

Denis Efremov, 12/30/2019 08:27 PM

 
#include "list.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)));
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
\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;
}

(1-1/4)