Project

General

Profile

Download (955 Bytes)

Bug #10027 » nlist.h

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

 
#ifndef _NLIST_H
#define _NLIST_H_

#define INT_MAX 2147483647
#define MAX_SIZE (INT_MAX-1)
#define NULL ((void*) 0)

struct list {
struct list *next;
unsigned int size;
struct list *val[];
};

typedef struct list ** list_t;

#ifndef SEPARATE
#include "logic_defs.h"
#include "lemmas.h"

#include "lemma_functions_linked_n.h"
#include "lemma_functions_linked_n.c"
#include "lemma_functions_index_of.h"
#include "lemma_functions_index_of.c"

#include "array_pop.c"
#include "array_push.c"
#endif

void
list_init( list_t list,
/* ghost: */ struct list **array);

struct list *
list_head( list_t list,
/* ghost: */ struct list **array, int index, int n);

int
list_length( list_t list,
/* ghost: */ struct list **array, int index, int n);

void
list_copy( list_t dest, list_t src,
/* ghost: */ struct list **array, int index, int n);

struct list *
list_item_next(struct list *item,
/* ghost: */ struct list **array, int index, int n);

#endif
(9-9/10)