stl_algorithm.res.oracle

[kernel] Parsing tests/stl/stl_algorithm.cpp (external front-end)
Now output intermediate result
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function initializer_list<int>::Ctor can't throw any exception
[kernel] Warning: Assuming declared function initializer_list<int>::Ctor can't throw any exception
[kernel] Warning: Assuming declared function initializer_list<int>::Ctor can't throw any exception
/* Generated by Frama-C */
struct _frama_c_vmt_content {
   void (*method_ptr)() ;
   int shift_this ;
};
struct _frama_c_rtti_name_info_node;
struct _frama_c_vmt {
   struct _frama_c_vmt_content *table ;
   int table_size ;
   struct _frama_c_rtti_name_info_node *rtti_info ;
};
struct _frama_c_rtti_name_info_content {
   struct _frama_c_rtti_name_info_node *value ;
   int shift_object ;
   int shift_vmt ;
};
struct _frama_c_rtti_name_info_node {
   char const *name ;
   struct _frama_c_rtti_name_info_content *base_classes ;
   int number_of_base_classes ;
   struct _frama_c_vmt *pvmt ;
};
typedef int ptrdiff_t;
typedef unsigned int size_t;
typedef size_t size_t;
typedef ptrdiff_t ptrdiff_t;
typedef int const *iterator;
struct initializer_list<int> {
   int const *base ;
   size_t length ;
};
typedef _Bool value_type;
struct integral_constant<bool,0>;
struct integral_constant<bool,0> {
   
};
typedef _Bool value_type;
struct integral_constant<bool,1>;
struct integral_constant<bool,1> {
   
};
typedef int *type;
typedef type *type;
typedef int *type;
typedef type *type;
typedef int *type;
typedef type *type;
typedef int type;
typedef void (*type)(int );
struct piecewise_construct_t;
struct piecewise_construct_t {
   
};
struct pair<int*,int*> {
   int *first ;
   int *second ;
};
struct exception;
struct bad_exception;
struct nested_exception;
struct exception {
   struct _frama_c_vmt *pvmt ;
};
struct bad_exception {
   struct exception _frama_c__ZN3stdE9exception ;
};
typedef void *exception_ptr;
struct nested_exception {
   struct _frama_c_vmt *pvmt ;
};
struct type_info;
struct bad_cast;
struct bad_typeid;
struct type_info {
   struct _frama_c_vmt *pvmt ;
};
struct bad_cast {
   struct exception _frama_c__ZN3stdE9exception ;
};
struct bad_typeid {
   struct exception _frama_c__ZN3stdE9exception ;
};
typedef _Bool (*type)(int );
typedef int argument_type;
struct reference_wrapper<bool*,<abst>> {
   _Bool (*obj)(int ) ;
};
typedef _Bool (*type)(int );
typedef int argument_type;
struct reference_wrapper<bool&,<abst>> {
   _Bool (*obj)(int ) ;
};
typedef _Bool (*__funtype)(int const *, int const *);
struct __bool_binop<int,std::__less> {
   
};
typedef _Bool (*__funtype)(int const *, int const *);
struct __bool_binop<int,std::__equal_to> {
   
};
struct equal_to<int> {
   struct __bool_binop<int,std::__equal_to> _frama_c__ZN3stdE12__bool_binopIiN3stdE10__equal_toE ;
};
struct less<int> {
   struct __bool_binop<int,std::__less> _frama_c__ZN3stdE12__bool_binopIiN3stdE6__lessE ;
};
struct unary_negate<bool*,<abst>> {
   _Bool (* const *__predicate)(int ) ;
};
struct unary_negate<std::reference_wrapper<bool&,<abst>>> {
   struct reference_wrapper<bool&,<abst>> const *__predicate ;
};
struct bad_function_call;
struct bad_function_call {
   struct exception _frama_c__ZN3stdE9exception ;
};
typedef ptrdiff_t difference_type;
typedef int value_type;
struct reverse_iterator<int*>;
struct reverse_iterator<int*>;
struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_;
struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ {
   _Bool (*__fc_lambda_apply)(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *,
                              value_type ) ;
   struct equal_to<int> pred ;
   int *it1 ;
};
typedef int *reference;
typedef int const *const_reference;
typedef int *iterator;
typedef int const *const_iterator;
typedef size_t size_type;
typedef struct reverse_iterator<int*> reverse_iterator;
typedef struct reverse_iterator<int*> const_reverse_iterator;
struct array<int,5> {
   int elems[5] ;
};
typedef int *reference;
typedef int const *const_reference;
typedef int *iterator;
typedef int const *const_iterator;
typedef size_t size_type;
typedef struct reverse_iterator<int*> reverse_iterator;
typedef struct reverse_iterator<int*> const_reverse_iterator;
struct array<int,2> {
   int elems[2] ;
};
void initializer_list<int>::Dtor(struct initializer_list<int> const *this);

struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void initializer_list<int>::Ctor(struct initializer_list<int> const *this)
{
  this->base = (int const *)0;
  this->length = (unsigned int)0;
  return;
}

/*@ requires \valid_read(this); */
void initializer_list<int>::Ctor(struct initializer_list<int> const *this,
                                 int const *b, size_t s);

/*@ requires \valid_read(this); */
size_t size(struct initializer_list<int> const *this)
{
  size_t __retres;
  __retres = this->length;
  return __retres;
}

/*@ requires \valid_read(this); */
int const *begin(struct initializer_list<int> const *this)
{
  int const *__retres;
  __retres = this->base;
  return __retres;
}

/*@ requires \valid_read(this); */
int const *end(struct initializer_list<int> const *this);

/*@ requires \valid_read(this); */
void initializer_list<int>::Dtor(struct initializer_list<int> const *this)
{
  return;
}

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "initializer_list",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
_Bool const value;
/*@ requires \valid_read(this); */
value_type value_type)(struct integral_constant<bool,0> const *this);

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "integral_constant",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
_Bool const value;
/*@ requires \valid_read(this); */
value_type value_type)(struct integral_constant<bool,1> const *this);

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "integral_constant",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "__boolean",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "__boolean",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "__and",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "_is_void",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "add_rvalue_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "add_rvalue_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "add_rvalue_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ ensures \valid(\result); */
type declval<int*&>(void);

/*@ ensures \valid(\result); */
type declval<int*&&>(void);

/*@ ensures \valid(\result); */
type declval<int*&>(void);

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "ok_type",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "ko_type",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_constructible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_constructible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_constructible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_copy_constructible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_assignable",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_assignable",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_copy_assignable",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_move_assignable",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_nothrow_constructible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_convertible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "is_convertible",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "remove_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "remove_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "remove_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "remove_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "remove_reference",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "enable_if",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
/*@ requires \valid(t);
    ensures \valid(\result); */
int **forward<int*&>(type *t)
{
  return t;
}

/*@ requires \valid(t);
    ensures \valid(\result); */
type *move<int&>(int *t)
{
  return t;
}

/*@ requires \valid(t);
    ensures \valid(\result); */
type *move<void*&,<abst>>(void (**t)(int ))
{
  return t;
}

void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this);

void piecewise_construct_t::Dtor(struct piecewise_construct_t const *this);

struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this)
{
  return;
}

/*@ requires \valid_read(this); */
void piecewise_construct_t::Dtor(struct piecewise_construct_t const *this)
{
  return;
}

struct piecewise_construct_t piecewise_construct;
void __fc_init_ZN3stdE19piecewise_construct(void) __attribute__((__constructor__));
void __fc_init_ZN3stdE19piecewise_construct(void)
{
  struct piecewise_construct_t __fc_tmp_0;
  piecewise_construct_t::Ctor(& __fc_tmp_0);
  piecewise_construct = __fc_tmp_0;
  piecewise_construct_t::Dtor((struct piecewise_construct_t const *)(& __fc_tmp_0));
  return;
}

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "piecewise_construct_t",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
void pair<int*,int*>::Dtor(struct pair<int*,int*> const *this);

struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this);
    requires \valid_read(y);
    requires \valid_read(x);
 */
void pair<int*,int*>::Ctor(struct pair<int*,int*> const *this,
                           int * const *x, int * const *y)
{
  this->first = *x;
  this->second = *y;
  return;
}

/*@ requires \valid(this);
    requires \valid(p); */
void swap(struct pair<int*,int*> *this, struct pair<int*,int*> *p);

/*@ requires \valid_read(this); */
void pair<int*,int*>::Dtor(struct pair<int*,int*> const *this)
{
  return;
}

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "pair",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
/*@ requires \valid(y);
    requires \valid(x); */
struct pair<int*,int*> make_pair<int*&,int*&>(int **x, int **y)
{
  int **tmp;
  int **tmp_0;
  tmp = forward<int*&>(y);
  tmp_0 = forward<int*&>(x);
  struct pair<int*,int*> __fc_tmp_1;
  pair<int*,int*>::Ctor(& __fc_tmp_1,(int * const *)tmp_0,(int * const *)tmp);
  return __fc_tmp_1;
}

/*@
axiomatic MemCmp {
  logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n) 
    reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
  
  axiom memcmp_zero{L1, L2}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
      (∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
  
  }
 */
/*@
axiomatic MemChr {
  logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  axiom memchr_def{L}:
    ∀ char *s;
    ∀ ℤ c;
    ∀ ℤ n;
      memchr(s, c, n) ≢ (0 ≢ 0) ⇔
      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
  
  }
 */
/*@
axiomatic MemSet {
  logic 𝔹 memset{L}(char *s, ℤ c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  axiom memset_def{L}:
    ∀ char *s;
    ∀ ℤ c;
    ∀ ℤ n;
      memset(s, c, n) ≢ (0 ≢ 0) ⇔
      (∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
  
  }
 */
/*@
axiomatic StrLen {
  logic ℤ strlen{L}(char *s) 
    reads *(s + (0 ..));
  
  axiom strlen_pos_or_null{L}:
    ∀ char *s;
    ∀ ℤ i;
      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
      *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
  
  axiom strlen_neg{L}:
    ∀ char *s;
      (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
  
  axiom strlen_before_null{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
  
  axiom strlen_at_null{L}:
    ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
  
  axiom strlen_not_zero{L}:
    ∀ char *s;
    ∀ ℤ i;
      0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
  
  axiom strlen_zero{L}:
    ∀ char *s;
    ∀ ℤ i;
      0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
  
  axiom strlen_sup{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
  
  axiom strlen_shift{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
  
  axiom strlen_create{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
  
  axiom strlen_create_shift{L}:
    ∀ char *s;
    ∀ ℤ i;
    ∀ ℤ k;
      0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
      0 ≤ strlen(s + k) ≤ i - k;
  
  axiom memcmp_strlen_left{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
      strlen(s1) ≡ strlen(s2);
  
  axiom memcmp_strlen_right{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
      strlen(s1) ≡ strlen(s2);
  
  axiom memcmp_strlen_shift_left{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ k, ℤ n;
      memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
      0 ≤ strlen(s2) ≤ k + strlen(s1);
  
  axiom memcmp_strlen_shift_right{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ k, ℤ n;
      memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
      0 ≤ strlen(s1) ≤ k + strlen(s2);
  
  }
 */
/*@
axiomatic StrCmp {
  logic ℤ strcmp{L}(char *s1, char *s2) 
    reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
  
  axiom strcmp_zero{L}:
    ∀ char *s1, char *s2;
      strcmp(s1, s2) ≡ 0 ⇔
      strlen(s1) ≡ strlen(s2) ∧
      (∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic StrNCmp {
  logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) 
    reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
  
  axiom strncmp_zero{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      strncmp(s1, s2, n) ≡ 0 ⇔
      (strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
      (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic StrChr {
  logic 𝔹 strchr{L}(char *s, ℤ c) 
    reads *(s + (0 .. strlen(s)));
  
  axiom strchr_def{L}:
    ∀ char *s;
    ∀ ℤ c;
      strchr(s, c) ≢ (0 ≢ 0) ⇔
      (∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
  
  }
 */
/*@
axiomatic WMemChr {
  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  axiom wmemchr_def{L}:
    ∀ int *s;
    ∀ int c;
    ∀ ℤ n;
      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
  
  }
 */
/*@
axiomatic WcsLen {
  logic ℤ wcslen{L}(int *s) 
    reads *(s + (0 ..));
  
  axiom wcslen_pos_or_null{L}:
    ∀ int *s;
    ∀ ℤ i;
      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (int)0) ∧
      *(s + i) ≡ (int)0 ⇒ wcslen(s) ≡ i;
  
  axiom wcslen_neg{L}:
    ∀ int *s;
      (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (int)0) ⇒ wcslen(s) < 0;
  
  axiom wcslen_before_null{L}:
    ∀ int *s;
    ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (int)0;
  
  axiom wcslen_at_null{L}:
    ∀ int *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (int)0;
  
  axiom wcslen_not_zero{L}:
    ∀ int *s;
    ∀ int i;
      0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (int)0 ⇒ i < wcslen(s);
  
  axiom wcslen_zero{L}:
    ∀ int *s;
    ∀ int i;
      0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (int)0 ⇒ i ≡ wcslen(s);
  
  axiom wcslen_sup{L}:
    ∀ int *s;
    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
  
  axiom wcslen_shift{L}:
    ∀ int *s;
    ∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
  
  axiom wcslen_create{L}:
    ∀ int *s;
    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
  
  axiom wcslen_create_shift{L}:
    ∀ int *s;
    ∀ int i;
    ∀ int k;
      0 ≤ k ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
  
  }
 */
/*@
axiomatic WcsCmp {
  logic ℤ wcscmp{L}(int *s1, int *s2) 
    reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
  
  axiom wcscmp_zero{L}:
    ∀ int *s1, int *s2;
      wcscmp(s1, s2) ≡ 0 ⇔
      wcslen(s1) ≡ wcslen(s2) ∧
      (∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic WcsNCmp {
  logic ℤ wcsncmp{L}(int *s1, int *s2, ℤ n) 
    reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
  
  axiom wcsncmp_zero{L}:
    ∀ int *s1, int *s2;
    ∀ ℤ n;
      wcsncmp(s1, s2, n) ≡ 0 ⇔
      (wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
      (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic WcsChr {
  logic 𝔹 wcschr{L}(int *wcs, ℤ wc) 
    reads *(wcs + (0 .. wcslen(wcs)));
  
  axiom wcschr_def{L}:
    ∀ int *wcs;
    ∀ ℤ wc;
      wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
      (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (int)((int)wc));
  
  }
 */
/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
 */
/*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
 */
/*@
predicate valid_string{L}(char *s) =
  0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
 */
/*@
predicate valid_read_string{L}(char *s) =
  0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
 */
/*@
predicate valid_read_nstring{L}(char *s, ℤ n) =
  (\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
  valid_read_string(s);
 */
/*@
predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
 */
/*@
predicate valid_wstring{L}(int *s) =
  0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
 */
/*@
predicate valid_read_wstring{L}(int *s) =
  0 ≤ wcslen(s) ∧ \valid_read(s + (0 .. wcslen(s)));
 */
/*@
predicate valid_read_nwstring{L}(int *s, ℤ n) =
  (\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
  valid_read_wstring(s);
 */
/*@
predicate valid_wstring_or_null{L}(int *s) =
  s ≡ \null ∨ valid_wstring(s);
 */
/*@ ghost int __fc_heap_status; */
/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(ℤ n) 
    reads __fc_heap_status;
  
  axiom never_allocable{L}:
    ∀ ℤ i; i < 0 ∨ i > 4294967295U ⇒ ¬is_allocable(i);
  
  }
 */
/*@
predicate non_escaping{L}(void *s, ℤ n) =
  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
 */
/*@
predicate empty_block{L}(void *s) =
  \block_length((char *)s) ≡ 0 ∧ \offset((char *)s) ≡ 0;
 */
/*@
predicate valid_or_empty{L}(void *s, size_t n) =
  (empty_block(s) ∨ \valid_read((char *)s)) ∧
  \valid((char *)s + (0 .. n - 1));
 */
/*@
predicate valid_read_or_empty{L}(void *s, size_t n) =
  (empty_block(s) ∨ \valid_read((char *)s)) ∧
  \valid_read((char *)s + (1 .. n - 1));

*/
/*@ requires valid_s1: valid_read_or_empty(s1, n);
    requires valid_s2: valid_read_or_empty(s2, n);
    requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
    requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
    requires s1: danglingness: non_escaping(s1, n);
    requires s2: danglingness: non_escaping(s2, n);
    ensures
      logic_spec:
        \result ≡
        memcmp{Pre, Pre}((char *)\old(s1), (char *)\old(s2), \old(n));
    assigns \result;
    assigns \result
      \from (indirect: *((char *)s1 + (0 .. n - 1))),
            (indirect: *((char *)s2 + (0 .. n - 1)));
 */
int memcmp(void const *s1, void const *s2, size_t n);

/*@ requires
      valid:
        valid_read_or_empty(s, n) ∨
        \valid_read((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
    requires
      initialization:
        \initialized((unsigned char *)s + (0 .. n - 1)) ∨
        \initialized((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
    requires
      danglingness:
        non_escaping(s, n) ∨
        non_escaping(s, (size_t)((int)(memchr_off((char *)s, c, n) + 1)));
    assigns \result;
    assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
    
    behavior found:
      assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
      ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
      ensures result_char: (int)*((char *)\result) ≡ \old(c);
      ensures
        result_in_str:
          ∀ ℤ i;
            (0 ≤ i < \old(n) ⇒
             *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
    
    behavior not_found:
      assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
      ensures result_null: \result ≡ \null;
 */
void *memchr(void const *s, int c, size_t n);

/*@ requires valid_dest: valid_or_empty(dest, n);
    requires valid_src: valid_read_or_empty(src, n);
    requires
      separation:
        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
    ensures
      copied_contents:
        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
        0;
    ensures result_ptr: \result ≡ \old(dest);
    assigns *((char *)dest + (0 .. n - 1)), \result;
    assigns *((char *)dest + (0 .. n - 1))
      \from *((char *)src + (0 .. n - 1));
    assigns \result \from dest;
 */
void *memcpy(void * __restrict dest, void const * __restrict src, size_t n);

/*@ requires valid_dest: valid_or_empty(dest, n);
    requires valid_src: valid_read_or_empty(src, n);
    ensures
      copied_contents:
        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡