stl_shared_ptr_mistake10.res.oracle

[kernel] Parsing tests/stl/stl_shared_ptr_mistake10.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 free can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor 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 malloc can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function malloc can't throw any exception
[kernel] Warning: Assuming declared function malloc 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 unsigned int size_t;
typedef void *nullptr_t;
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> {
   
};
struct Aircraft;
typedef struct Aircraft *type;
typedef type *type;
struct __shared_ref_base;
struct piecewise_construct_t;
struct piecewise_construct_t {
   
};
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 weak_ptr<Aircraft>;
struct shared_ptr<Aircraft> {
   struct Aircraft *__ptr ;
   struct __shared_ref_base *_ref ;
};
struct __shared_ref_base {
   struct _frama_c_vmt *pvmt ;
};
struct __shared_ref<void> {
   struct __shared_ref_base _frama_c__ZN3stdE17__shared_ref_base ;
   void *__ptr ;
   long _n ;
   long _w ;
};
struct __shared_ref<Aircraft> {
   struct __shared_ref_base _frama_c__ZN3stdE17__shared_ref_base ;
   struct Aircraft *__ptr ;
   long _n ;
   long _w ;
};
struct weak_ptr<Aircraft> {
   struct Aircraft *__ptr ;
   struct __shared_ref_base *_ref ;
};
struct bad_weak_ptr;
struct bad_weak_ptr {
   struct exception _frama_c__ZN3stdE9exception ;
};
struct shared_ptr<void>;
struct shared_ptr<void> {
   void *__ptr ;
   struct __shared_ref_base *_ref ;
};
struct __fc_div_t {
   int quot ;
   int rem ;
};
typedef struct __fc_div_t div_t;
struct __fc_ldiv_t {
   long quot ;
   long rem ;
};
typedef struct __fc_ldiv_t ldiv_t;
struct __fc_lldiv_t {
   long long quot ;
   long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
struct Aircraft {
   int m_id ;
   int m_flyCount ;
   struct weak_ptr<Aircraft> myWingMan ;
};
void *malloc(size_t size);

void free(void *p);

enum __fc_exn_enum {
    __fc_exn_kind___fc_S_ZN3stdE12bad_weak_ptr = 0
};
union __fc_exn_union {
   struct bad_weak_ptr __fc_S_ZN3stdE12bad_weak_ptr ;
};
struct __fc_exn_struct {
   int exn_uncaught ;
   enum __fc_exn_enum exn_kind ;
   union __fc_exn_union exn_obj ;
};
struct __fc_exn_struct __fc_exn =
  {.exn_uncaught = 0,
   .exn_kind = 0,
   .exn_obj = {.__fc_S_ZN3stdE12bad_weak_ptr = {._frama_c__ZN3stdE9exception = {
                                                .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 = "_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_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<Aircraft*>(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 = "pre_is_base_of2",
   .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_base_of",
   .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 = "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(b);
    requires \valid(a); */
void swap<void*>(void **a, void **b)
{
  void *tmp = *a;
  *a = *b;
  *b = tmp;
  return;
}

/*@ requires \valid(b);
    requires \valid(a); */
void swap<std::__shared_ref_base*>(struct __shared_ref_base **a,
                                   struct __shared_ref_base **b)
{
  struct __shared_ref_base *tmp = *a;
  *a = *b;
  *b = tmp;
  return;
}

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};
/*@
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; */
/*@ requires freeable: p ≡ \null ∨ \freeable(p);
    assigns __fc_heap_status;
    assigns __fc_heap_status \from __fc_heap_status;
    frees p;
    
    behavior deallocation:
      assumes nonnull_p: p ≢ \null;
      ensures freed: \allocable(\old(p));
      assigns __fc_heap_status;
      assigns __fc_heap_status \from __fc_heap_status;
    
    behavior no_deallocation:
      assumes null_p: p ≡ \null;
      assigns \nothing;
      allocates \nothing;
    
    complete behaviors no_deallocation, deallocation;
    disjoint behaviors no_deallocation, deallocation;
 */
void free(void *p);

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(ℤ n) 
    reads __fc_heap_status;
  
  axiom never_allocable{L}:
    ∀ ℤ i; i < 0 ∨ i > 4294967295U ⇒ ¬is_allocable(i);
  
  }

*/
/*@ assigns __fc_heap_status, \result;
    assigns __fc_heap_status \from size, __fc_heap_status;
    assigns \result \from (indirect: size), (indirect: __fc_heap_status);
    allocates \result;
    
    behavior allocation:
      assumes can_allocate: is_allocable(size);
      ensures allocation: \fresh{Old, Here}(\result,\old(size));
      assigns __fc_heap_status, \result;
      assigns __fc_heap_status \from size, __fc_heap_status;
      assigns \result \from (indirect: size), (indirect: __fc_heap_status);
    
    behavior no_allocation:
      assumes cannot_allocate: ¬is_allocable(size);
      ensures null_result: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
void *malloc(size_t size);

/*@
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)) ≡
        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 *memmove(void *dest, void const *src, size_t n);

/*@ requires valid_s: valid_or_empty(s, n);
    ensures
      acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
    ensures result_ptr: \result ≡ \old(s);
    assigns *((char *)s + (0 .. n - 1)), \result;
    assigns *((char *)s + (0 .. n - 1)) \from c;
    assigns \result \from s;
 */
void *memset(void *s, int c, size_t n);

/*@ requires valid_string_s: valid_read_string(s);
    ensures acsl_c_equiv: \result ≡ strlen(\old(s));
    assigns \result;
    assigns \result \from (indirect: *(s + (0 ..)));
 */
size_t strlen(char const *s);

/*@ requires valid_string_s: valid_read_nstring(s, n);
    ensures
      result_bounded: \result ≡ strlen(\old(s)) ∨ \result ≡ \old(n);
    assigns \result;
    assigns \result \from (indirect: *(s + (0 .. n - 1))), (indirect: n);
 */
size_t strnlen(char const *s, size_t n);

/*@ requires valid_string_s1: valid_read_string(s1);
    requires valid_string_s2: valid_read_string(s2);
    ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
 */
int strcmp(char const *s1, char const *s2);

/*@ requires valid_string_s1: valid_read_nstring(s1, n);
    requires valid_string_s2: valid_read_nstring(s2, n);
    ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n));
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. n - 1))),
            (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
 */
int strncmp(char const *s1, char const *s2, size_t n);

/*@ requires valid_string_s1: valid_read_string(s1);
    requires valid_string_s2: valid_read_string(s2);
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
 */
int strcoll(char const *s1, char const *s2);

/*@ requires valid_string_s: valid_read_string(s);
    assigns \result;
    assigns \result
      \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
    
    behavior found:
      assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
      ensures result_char: *\result ≡ (char)\old(c);
      ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
      ensures
        result_in_length: \old(s) ≤ \result ≤ \old(s) + strlen(\old(s));
      ensures result_valid_string: valid_read_string(\result);
      ensures
        result_first_occur:
          ∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
    
    behavior not_found:
      assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
      ensures result_null: \result ≡ \null;
    
    behavior default:
      ensures
        result_null_or_same_base:
          \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
 */
char *strchr(char const *s, int c);

/*@ requires valid_string_s: valid_read_string(s);
    ensures
      result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
    assigns \result;
    assigns \result
      \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
 */
char *strchrnul(char const *s, int c);

/*@ requires valid_string_s: valid_read_string(s);
    assigns \result;
    assigns \result \from s, *(s + (0 ..)), c;
    
    behavior found:
      assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
      ensures result_char: (int)*\result ≡ \old(c);
      ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
      ensures result_valid_string: valid_read_string(\result);
    
    behavior not_found:
      assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
      ensures result_null: \result ≡ \null;
    
    behavior default:
      ensures
        result_null_or_same_base:
          \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
 */
char *strrchr(char const *s, int c);

/*@ requires valid_string_s: valid_read_string(s);
    requires valid_string_reject: valid_read_string(reject);
    ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
    assigns \result;
    assigns \result
      \from (indirect: *(s + (0 ..))), (indirect: *(reject + (0 ..)));
 */
size_t strcspn(char const *s, char const *reject);

/*@ requires valid_string_s: valid_read_string(s);
    requires valid_string_accept: valid_read_string(accept);
    ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
    assigns \result;
    assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
    assigns \result
      \from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
 */
size_t strspn(char const *s, char const *accept);

/*@ requires valid_string_s: valid_read_string(s);
    requires valid_string_accept: valid_read_string(accept);
    ensures
      result_null_or_same_base:
        \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
    assigns \result;
    assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
 */
char *strpbrk(char const *s, char const *accept);

/*@ requires valid_string_haystack: valid_read_string(haystack);
    requires valid_string_needle: valid_read_string(needle);
    ensures
      result_null_or_in_haystack:
        \result ≡ \null ∨
        (\subset(\result, \old(haystack) + (0 ..)) ∧
         \valid_read(\result) ∧
         memcmp{Pre, Pre}(\result, \old(needle), strlen(\old(needle))) ≡ 0);
    assigns \result;
    assigns \result
      \from haystack, (indirect: *(haystack + (0 ..))),
            (indirect: *(needle + (0 ..)));
 */
char *strstr(char const *haystack, char const *needle);

/*@ requires valid_string_haystack: valid_read_string(haystack);
    requires valid_string_needle: valid_read_string(needle);
    ensures
      result_null_or_in_haystack:
        \result ≡ \null ∨
        (\subset(\result, \old(haystack) + (0 ..)) ∧ \valid_read(\result));
    assigns \result;
    assigns \result
      \from haystack, (indirect: *(haystack + (0 ..))),
            (indirect: *(needle + (0 ..)));
 */
char *strcasestr(char const *haystack, char const *needle);

char *__fc_strtok_ptr;
/*@ requires valid_string_delim: valid_read_string(delim);
    assigns *(s + (0 ..)), *(__fc_strtok_ptr + (0 ..)), \result,
            __fc_strtok_ptr;
    assigns *(s + (0 ..))
      \from *(s + (0 ..)), (indirect: s), (indirect: __fc_strtok_ptr),
            (indirect: *(delim + (0 ..)));
    assigns *(__fc_strtok_ptr + (0 ..))
      \from *(__fc_strtok_ptr + (0 ..)), (indirect: s),
            (indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..)));
    assigns \result
      \from s, __fc_strtok_ptr, (indirect: *(s + (0 ..))),
            (indirect: *(__fc_strtok_ptr + (0 ..))),
            (indirect: *(delim + (0 ..)));
    assigns __fc_strtok_ptr
      \from \old(__fc_strtok_ptr), s,
            (indirect: *(__fc_strtok_ptr + (0 ..))),
            (indirect: *(delim + (0 ..)));
    
    behavior new_str:
      assumes s_not_null: s ≢ \null;
      requires
        valid_string_s_or_delim_not_found:
          valid_string(s) ∨
          (valid_read_string(s) ∧
           (∀ int i;
              0 ≤ i < strlen(delim) ⇒
              strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
      ensures
        result_subset:
          \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
      ensures ptr_subset: \subset(__fc_strtok_ptr, \old(s) + (0 ..));
      assigns __fc_strtok_ptr, *(s + (0 ..)), \result;
      assigns __fc_strtok_ptr
        \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
      assigns *(s + (0 ..))
        \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));