gen_stdout.c

/* Generated by Frama-C */
char *__e_acsl_literal_string_2;
char *__e_acsl_literal_string;
struct __anonstruct___mpz_struct_1 {
   int _mp_alloc ;
   int _mp_size ;
   unsigned long *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned long size_t;
typedef unsigned int ino_t;
typedef unsigned int gid_t;
typedef unsigned int uid_t;
typedef long time_t;
typedef unsigned int blkcnt_t;
typedef unsigned int blksize_t;
typedef unsigned int dev_t;
typedef unsigned int mode_t;
typedef unsigned int nlink_t;
typedef long off_t;
struct stat {
   dev_t st_dev ;
   ino_t st_ino ;
   mode_t st_mode ;
   nlink_t st_nlink ;
   uid_t st_uid ;
   gid_t st_gid ;
   dev_t st_rdev ;
   off_t st_size ;
   time_t st_atime ;
   time_t st_mtime ;
   time_t st_ctime ;
   blksize_t st_blksize ;
   blkcnt_t st_blocks ;
};
struct __fc_pos_t {
   unsigned long __fc_stdio_position ;
};
typedef struct __fc_pos_t fpos_t;
struct __fc_FILE {
   unsigned int __fc_stdio_id ;
   fpos_t __fc_position ;
   char __fc_error ;
   char __fc_eof ;
   int __fc_flags ;
   struct stat *__fc_inode ;
   unsigned char *__fc_real_data ;
   int __fc_real_data_max_size ;
};
typedef struct __fc_FILE FILE;
/*@ requires predicate ≢ 0;
    assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
                                                           char *kind,
                                                           char *fct,
                                                           char *pred_txt,
                                                           int line);

/*@
model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;
  
  }
 */
/*@ ghost extern int __e_acsl_init; */

/*@ assigns \result;
    assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
                                                            size_t size);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);

/*@ ghost extern int __e_acsl_internal_heap; */

/*@ assigns __e_acsl_internal_heap;
    assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
 */
extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);

extern size_t __memory_size;

/*@
predicate diffSize{L1, L2}(ℤ i) =
  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
 */
extern FILE *stdout;

FILE __fc_fopen[512];
FILE * const __p_fc_fopen = __fc_fopen;
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
    assigns \result;
    assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
 */
extern FILE *fopen(char const *filename, char const *mode);

/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
    assigns \result;
    assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
 */
FILE *__e_acsl_fopen(char const *filename, char const *mode)
{
  FILE *__retres;
  __retres = fopen(filename,mode);
  return __retres;
}

void __e_acsl_memory_init(void)
{
  __e_acsl_literal_string_2 = "wb";
  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
  __full_init((void *)__e_acsl_literal_string_2);
  __literal_string((void *)__e_acsl_literal_string_2);
  __e_acsl_literal_string = "foo";
  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
  __full_init((void *)__e_acsl_literal_string);
  __literal_string((void *)__e_acsl_literal_string);
  __store_block((void *)(& stdout),8UL);
  __full_init((void *)(& stdout));
  return;
}

int main(void)
{
  int __retres;
  FILE *f;
  FILE *f2;
  __e_acsl_memory_init();
  __store_block((void *)(& f),8UL);
  __full_init((void *)(& f));
  f = stdout;
  f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
  /*@ assert f ≡ __fc_stdout; */
  e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
                (char *)"f == __fc_stdout",13);
  __retres = 0;
  __delete_block((void *)(& stdout));
  __delete_block((void *)(& f));
  __e_acsl_memory_clean();
  return __retres;
}