Project

General

Profile

Download (714 Bytes)

Bug #10021 » list.h

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

 
#ifndef _LIST_H_
#define _LIST_H_

#define INT_MAX 2147483647
#define MAX_SIZE INT_MAX-1

#ifndef NULL
#define NULL ((void*) 0)
#endif

struct list {
struct list *next;
int k;
};

typedef struct list ** list_t;

#include "logic_defs.h"
#include "lemmas.h"

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);

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);

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

#endif
(2-2/4)