solidity_array.c File Reference

#include <stddef.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <assert.h>
#include "solidity_types.h"

Include dependency graph for solidity_array.c:

Functions
	__attribute__ ((annotate("__ESBMC_inf_size")))
void	_ESBMC_element_null_check (int ok)
void	_ESBMC_zero_size_check (int ok)
void	_ESBMC_pop_empty_check (int ok)
void	_ESBMC_store_array (void *array, size_t length)
unsigned int	_ESBMC_array_length (void *array)
void *	_ESBMC_arrcpy (void *from_array, size_t from_size, size_t size_of)
void *	_ESBMC_array_push (void *array, void *element, size_t size_of_element)
void	_ESBMC_array_pop (void *array, size_t size_of_element)

Function Documentation

__attribute__()

__attribute__

(

(annotate("__ESBMC_inf_size"))

)

_ESBMC_array_length()

unsigned int _ESBMC_array_length

(

void *

array

)

_ESBMC_array_pop()

void _ESBMC_array_pop	(	void *	array,
		size_t	size_of_element )

_ESBMC_array_push()

void * _ESBMC_array_push	(	void *	array,
		void *	element,
		size_t	size_of_element )

_ESBMC_arrcpy()

void * _ESBMC_arrcpy	(	void *	from_array,
		size_t	from_size,
		size_t	size_of )

_ESBMC_element_null_check()

void _ESBMC_element_null_check

(

int

ok

)

_ESBMC_pop_empty_check()

void _ESBMC_pop_empty_check

(

int

ok

)

_ESBMC_store_array()

void _ESBMC_store_array	(	void *	array,
		size_t	length )

_ESBMC_zero_size_check()

void _ESBMC_zero_size_check

(

int

ok

)