gen_struct_initialized.c 6.32 KB
Newer Older
Basile Desloges 's avatar
Basile Desloges committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
/* Generated by Frama-C */
#include "stddef.h"
#include "stdint.h"
#include "stdio.h"
#include "stdlib.h"
struct __anonstruct_int32_pair_t_1 {
   int32_t a ;
   int32_t b ;
};
typedef struct __anonstruct_int32_pair_t_1 int32_pair_t;
int main(void)
{
  int __retres;
  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
  {
    int32_pair_t static_pair;
    __e_acsl_store_block((void *)(& static_pair),(size_t)8);
    {
      int __gen_e_acsl_initialized;
      __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& static_pair.a),
                                                      sizeof(int32_t));
      __e_acsl_assert(! __gen_e_acsl_initialized,"Assertion","main",
                      "!\\initialized(&static_pair.a)",
                      "tests/memory/struct_initialized.c",13);
    }
    /*@ assert ¬\initialized(&static_pair.a); */ ;
    {
      int __gen_e_acsl_initialized_2;
      __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& static_pair.b),
                                                        sizeof(int32_t));
      __e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main",
                      "!\\initialized(&static_pair.b)",
                      "tests/memory/struct_initialized.c",14);
    }
    /*@ assert ¬\initialized(&static_pair.b); */ ;
    __e_acsl_initialize((void *)(& static_pair.a),sizeof(int32_t));
    static_pair.a = 1;
    {
      int __gen_e_acsl_initialized_3;
      __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& static_pair.a),
                                                        sizeof(int32_t));
      __e_acsl_assert(__gen_e_acsl_initialized_3,"Assertion","main",
                      "\\initialized(&static_pair.a)",
                      "tests/memory/struct_initialized.c",16);
    }
    /*@ assert \initialized(&static_pair.a); */ ;
    {
      int __gen_e_acsl_initialized_4;
      __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& static_pair.b),
                                                        sizeof(int32_t));
      __e_acsl_assert(! __gen_e_acsl_initialized_4,"Assertion","main",
                      "!\\initialized(&static_pair.b)",
                      "tests/memory/struct_initialized.c",17);
    }
    /*@ assert ¬\initialized(&static_pair.b); */ ;
    __e_acsl_initialize((void *)(& static_pair.b),sizeof(int32_t));
    static_pair.b = 2;
    {
      int __gen_e_acsl_initialized_5;
      __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& static_pair.a),
                                                        sizeof(int32_t));
      __e_acsl_assert(__gen_e_acsl_initialized_5,"Assertion","main",
                      "\\initialized(&static_pair.a)",
                      "tests/memory/struct_initialized.c",19);
    }
    /*@ assert \initialized(&static_pair.a); */ ;
    {
      int __gen_e_acsl_initialized_6;
      __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& static_pair.b),
                                                        sizeof(int32_t));
      __e_acsl_assert(__gen_e_acsl_initialized_6,"Assertion","main",
                      "\\initialized(&static_pair.b)",
                      "tests/memory/struct_initialized.c",20);
    }
    /*@ assert \initialized(&static_pair.b); */ ;
    __e_acsl_delete_block((void *)(& static_pair));
  }
  {
    int32_pair_t *heap_pair = malloc(sizeof(int32_pair_t));
    __e_acsl_store_block((void *)(& heap_pair),(size_t)8);
    __e_acsl_full_init((void *)(& heap_pair));
    {
      int __gen_e_acsl_initialized_7;
      __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& heap_pair->a),
                                                        sizeof(int32_t));
      __e_acsl_assert(! __gen_e_acsl_initialized_7,"Assertion","main",
                      "!\\initialized(&heap_pair->a)",
                      "tests/memory/struct_initialized.c",26);
    }
    /*@ assert ¬\initialized(&heap_pair->a); */ ;
    {
      int __gen_e_acsl_initialized_8;
      __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(& heap_pair->b),
                                                        sizeof(int32_t));
      __e_acsl_assert(! __gen_e_acsl_initialized_8,"Assertion","main",
                      "!\\initialized(&heap_pair->b)",
                      "tests/memory/struct_initialized.c",27);
    }
    /*@ assert ¬\initialized(&heap_pair->b); */ ;
    __e_acsl_initialize((void *)(& heap_pair->a),sizeof(int32_t));
    heap_pair->a = 3;
    {
      int __gen_e_acsl_initialized_9;
      __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(& heap_pair->a),
                                                        sizeof(int32_t));
      __e_acsl_assert(__gen_e_acsl_initialized_9,"Assertion","main",
                      "\\initialized(&heap_pair->a)",
                      "tests/memory/struct_initialized.c",29);
    }
    /*@ assert \initialized(&heap_pair->a); */ ;
    {
      int __gen_e_acsl_initialized_10;
      __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& heap_pair->b),
                                                         sizeof(int32_t));
      __e_acsl_assert(! __gen_e_acsl_initialized_10,"Assertion","main",
                      "!\\initialized(&heap_pair->b)",
                      "tests/memory/struct_initialized.c",30);
    }
    /*@ assert ¬\initialized(&heap_pair->b); */ ;
    __e_acsl_initialize((void *)(& heap_pair->b),sizeof(int32_t));
    heap_pair->b = 4;
    {
      int __gen_e_acsl_initialized_11;
      __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(& heap_pair->a),
                                                         sizeof(int32_t));
      __e_acsl_assert(__gen_e_acsl_initialized_11,"Assertion","main",
                      "\\initialized(&heap_pair->a)",
                      "tests/memory/struct_initialized.c",32);
    }
    /*@ assert \initialized(&heap_pair->a); */ ;
    {
      int __gen_e_acsl_initialized_12;
      __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& heap_pair->b),
                                                         sizeof(int32_t));
      __e_acsl_assert(__gen_e_acsl_initialized_12,"Assertion","main",
                      "\\initialized(&heap_pair->b)",
                      "tests/memory/struct_initialized.c",33);
    }
    /*@ assert \initialized(&heap_pair->b); */ ;
    __e_acsl_delete_block((void *)(& heap_pair));
  }
  __retres = 0;
  __e_acsl_memory_clean();
  return __retres;
}