framac.ast

/* Generated by Frama-C */
#include "assert.h"
#include "errno.h"
#include "inttypes.h"
#include "stdarg.h"
#include "stdint.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
struct __anonstruct_st_1 {
   int i ;
   float f ;
   int j ;
};
typedef struct __anonstruct_st_1 st;
/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: param3),
            (indirect: param2), (indirect: param1), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            param3, param2, param1, param0;
 */
int printf_va_1(char const * restrict format, int param0, double param1,
                int param2, double param3);

int main(void)
{
  int __retres;
  st s = {.i = 1, .f = (float)2.0, .j = 3};
  int *pj = & s.j;
  char *pcj = (char *)pj;
  char *pcst = pcj - (8U - 0U);
  st *ps = (st *)pcst;
  ps->f = (float)22.0;
  printf("s.i=%i s.f=%f s.j=%i ps->f=%f\n",s.i,(double)s.f,s.j,(double)ps->f); /* printf_va_1 */
  __retres = 0;
  return __retres;
}