Line data    Source code

       1             : /*
       2             :  *
       3             :  */
       4             : 
       5             : #pragma once
       6             : 
       7             : #include <aws/common/common.h>
       8             : #include <nondet.h>
       9             : #include <stdlib.h>
      10             : 
      11      136579 : #define OBJECT_BITS 8
      12     1983554 : #define MAX_MALLOC (SIZE_MAX >> (OBJECT_BITS + 1))
      13             : 
      14             : #define MEM_BLOCK 4096
      15             : 
      16             : void *realloc(void *ptr, size_t new_size);
      17             : 
      18             : /**
      19             :  * Deterministically allocates [size] bytes and returns a pointer;
      20             :  * memory allocated will be marked as containing non-det content using memhavoc
      21             :  */
      22             : void *bounded_malloc(size_t size);
      23             : 
      24             : /**
      25             :  * Can non-deterministically fail;
      26             :  * if successful, allocate [size] bytes and returns a pointer;
      27             :  * memory allocated will be marked as containing non-det content using memhavoc
      28             :  */
      29             : void *can_fail_malloc(size_t size);
      30             : 
      31             : /**
      32             :  * Pointer to SeaHorn-based allocator
      33             :  */
      34             : struct aws_allocator *sea_allocator(void);