framac.ast

/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "errno.h"
#include "inttypes.h"
#include "netdb.h"
#include "netinet/in.h"
#include "signal.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
#include "sys/socket.h"
#include "sys/uio.h"
/*@ requires valid_read_string(format);
    assigns \result, stream->__fc_FILE_data;
    assigns \result
      \from (indirect: stream->__fc_FILE_id),
            (indirect: stream->__fc_FILE_data),
            (indirect: *(format + (0 ..)));
    assigns stream->__fc_FILE_data
      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
            (indirect: *(format + (0 ..)));
 */
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);

static void validate_addr_form(char *v)
{
  size_t tmp;
  size_t tmp_0;
  tmp = strspn((char const *)v,
               "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz-0123456789.");
  tmp_0 = strlen((char const *)v);
  if (tmp < tmp_0) {
    fprintf(__fc_stderr,"hostname contains invalid characters"); /* fprintf_va_1 */
    exit(1);
  }
  return;
}

static int my_strcmp(char const *s1, char const *s2)
{
  int __retres;
  size_t i;
  i = (unsigned int)0;
  while ((int)*(s1 + i) == (int)*(s2 + i)) {
    if ((int)*(s1 + i) == 0) {
      __retres = 0;
      goto return_label;
    }
    i += (size_t)1;
  }
  __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
  return_label: return __retres;
}

static in_addr_t my_inet_addr(char const *cp)
{
  in_addr_t __retres;
  int tmp_0;
  tmp_0 = my_strcmp(cp,"127.0.0.1");
  if (tmp_0 == 0) {
    __retres = (unsigned int)0;
    goto return_label;
  }
  else {
    int tmp;
    tmp = Frama_C_nondet(1,(int)4294967295U);
    __retres = (unsigned int)tmp;
    goto return_label;
  }
  return_label: return __retres;
}

static struct hostent my_gethostbyaddr_res;
static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
                                        int type)
{
  struct hostent *__retres;
  if ((in_addr_t *)addr == (in_addr_t *)0) my_gethostbyaddr_res.h_name = (char *)"www.example.com";
  else my_gethostbyaddr_res.h_name = (char *)"hypermegagigaterasupercalifragilisticexpialidocious2.example.com";
  __retres = & my_gethostbyaddr_res;
  return __retres;
}

void host_lookup(char *user_supplied_addr)
{
  struct hostent *hp;
  in_addr_t *addr;
  char hostname[64];
  in_addr_t tmp;
  validate_addr_form(user_supplied_addr);
  tmp = my_inet_addr((char const *)user_supplied_addr);
  addr = (in_addr_t *)tmp;
  hp = my_gethostbyaddr((void const *)addr,sizeof(struct in_addr),2);
  strcpy(hostname,(char const *)hp->h_name);
  return;
}

int main(void)
{
  int __retres;
  char *very_large_but_valid_hostname = (char *)"127.0.0.1";
  host_lookup(very_large_but_valid_hostname);
  char *overly_large_hostname = (char *)"127.0.0.2";
  host_lookup(overly_large_hostname);
  __retres = 0;
  return __retres;
}