[kernel] Parsing tests/spec/acsl_basic_allocator.c (with preprocessing)
/* Generated by Frama-C */
#include "stdlib.h"
enum _bool {
    false = 0,
    true = 1
};
typedef enum _bool bool;
struct _memory_block {
   size_t size ;
   bool free ;
   char *data ;
};
typedef struct _memory_block memory_block;
struct _memory_block_list {
   memory_block *block ;
   struct _memory_block_list *next ;
};
typedef struct _memory_block_list memory_block_list;
typedef memory_block_list *memory_pool;
/*@
type invariant inv_memory_block(memory_block mb) =
  0 < mb.size ∧ \offset(mb.data) ≡ 0 ∧
  \block_length(mb.data) ≡ mb.size;
 */
/*@
predicate used_memory_block{L}(memory_block mb) =
  mb.free ≡ false ∧ inv_memory_block(mb);
 */
/*@
predicate freed_memory_block{L}(memory_block mb) =
  mb.free ≡ true ∧ inv_memory_block(mb);
 */
/*@
predicate valid_memory_block{L}(memory_block *mb) =
  \valid(mb) ∧ inv_memory_block(*mb);
 */
/*@
predicate valid_used_memory_block{L}(memory_block *mb) =
  \valid(mb) ∧ used_memory_block(*mb);
 */
/*@
predicate valid_freed_memory_block{L}(memory_block *mb) =
  \valid(mb) ∧ freed_memory_block(*mb);
 */
/*@
predicate valid_memory_block_list{L}(memory_block_list *mbl) =
  \valid(mbl) ∧ valid_memory_block(mbl->block) ∧
  (mbl->next ≡ \null ∨ valid_memory_block_list(mbl->next));
 */
/*@
predicate valid_memory_pool{L}(memory_pool *mp) =
  \valid(mp) ∧ valid_memory_block_list(*mp);

*/
/*@ requires valid_memory_pool(arena) ∧ 0 < s;
    ensures valid_used_memory_block(\result);
 */
memory_block *memory_alloc(memory_pool *arena, size_t s)
{
  memory_block *__retres;
  memory_block *mb;
  size_t mb_size;
  char *mb_data;
  memory_block_list *mbl = *arena;
  while (mbl != (memory_block_list *)0) {
    mb = mbl->block;
    if (mb->free) 
      if (s <= mb->size) {
        mb->free = false;
        __retres = mb;
        goto return_label;
      }
    mbl = mbl->next;
  }
  if ((size_t)1000 < s) mb_size = s; else mb_size = (unsigned int)1000;
  mb_data = (char *)malloc(mb_size);
  mb = (memory_block *)malloc(sizeof(memory_block));
  mb->size = mb_size;
  mb->free = false;
  mb->data = mb_data;
  mbl = (memory_block_list *)malloc(sizeof(memory_block_list));
  mbl->block = mb;
  mbl->next = *arena;
  *arena = mbl;
  __retres = mb;
  return_label: return __retres;
}

/*@ requires valid_memory_pool(arena) ∧ valid_used_memory_block(block);
    ensures valid_freed_memory_block(\old(block));
 */
void memory_free(memory_pool *arena, memory_block *block)
{
  block->free = true;
  return;
}