Skip to content
Snippets Groups Projects
Forked from pub / Frama Clang
687 commits behind the upstream repository.
stl_system_error.res.oracle 135.17 KiB
[kernel] Parsing tests/stl/stl_system_error.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 tm::Ctor 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 operator= 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 operator= 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 operator= can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor 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 size_t 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 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 ;
};
typedef unsigned int uid_t;
typedef long time_t;
struct __fc_FILE {
   unsigned int __fc_FILE_id ;
   unsigned int __fc_FILE_data ;
};
typedef struct __fc_FILE FILE;
typedef int clockid_t;
typedef int pid_t;
typedef unsigned long sigset_t;
union sigval {
   int sival_int ;
   void *sival_ptr ;
};
struct __fc_siginfo_t {
   int si_signo ;
   int si_code ;
   union sigval si_value ;
   int si_errno ;
   pid_t si_pid ;
   uid_t si_uid ;
   void *si_addr ;
   int si_status ;
   int si_band ;
};
typedef struct __fc_siginfo_t siginfo_t;
struct sigaction {
   void (*sa_handler)(int ) ;
   void (*sa_sigaction)(int , siginfo_t *, void *) ;
   sigset_t sa_mask ;
   int sa_flags ;
};
typedef unsigned int clock_t;
struct tm;
struct tm {
   int tm_sec ;
   int tm_min ;
   int tm_hour ;
   int tm_mday ;
   int tm_mon ;
   int tm_year ;
   int tm_wday ;
   int tm_yday ;
   int tm_isdst ;
};
struct timespec {
   long tv_sec ;
   long tv_nsec ;
};
typedef char char_type;
typedef int char_type;
struct __shared_ref_base;
struct piecewise_construct_t;
struct piecewise_construct_t {
   
};
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 bad_weak_ptr;
struct shared_ptr<void>;
struct bad_weak_ptr {
   struct exception _frama_c__ZN3stdE9exception ;
};
struct shared_ptr<void> {
   void *__ptr ;
   struct __shared_ref_base *_ref ;
};
struct basic_string<char,std::char_traits<char>,std::allocator<char>>;
typedef struct basic_string<char,std::char_traits<char>,std::allocator<char>> string;
struct logic_error;
struct domain_error;
struct invalid_argument;
struct length_error;
struct out_of_range;
struct runtime_error;
struct range_error;
struct overflow_error;
struct underflow_error;
struct logic_error {
   struct exception _frama_c__ZN3stdE9exception ;
};
struct domain_error {
   struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct invalid_argument {
   struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct length_error {
   struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct out_of_range {
   struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct runtime_error {
   struct exception _frama_c__ZN3stdE9exception ;
};
struct range_error {
   struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct overflow_error {
   struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct underflow_error {
   struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct error_condition;
struct error_code;
struct error_category;
struct system_error;
struct error_category {
   struct _frama_c_vmt *pvmt ;
};
struct error_code {
   int val_ ;
   struct error_category const *cat_ ;
};
struct system_error {
   struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct error_condition {
   int val_ ;
   struct error_category const *cat_ ;
};
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_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];
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_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};
/*@
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)) ≡
        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, \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 ..)));
      assigns \result
        \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
    
    behavior resume_str:
      assumes s_null: s ≡ \null;
      requires not_first_call: __fc_strtok_ptr ≢ \null;
      ensures
        result_subset:
          \result ≡ \null ∨
          \subset(\result, \old(__fc_strtok_ptr) + (0 ..));
      ensures
        ptr_subset: \subset(__fc_strtok_ptr, \old(__fc_strtok_ptr) + (0 ..));
      assigns *(__fc_strtok_ptr + (0 ..)), __fc_strtok_ptr, \result;
      assigns *(__fc_strtok_ptr + (0 ..))
        \from *(__fc_strtok_ptr + (0 ..)), (indirect: __fc_strtok_ptr),
              (indirect: *(delim + (0 ..)));
      assigns __fc_strtok_ptr
        \from \old(__fc_strtok_ptr), (indirect: *(__fc_strtok_ptr + (0 ..))),
              (indirect: *(delim + (0 ..)));
      assigns \result
        \from __fc_strtok_ptr, (indirect: *(__fc_strtok_ptr + (0 ..))),
              (indirect: *(delim + (0 ..)));
    
    complete behaviors resume_str, new_str;
    disjoint behaviors resume_str, new_str;
 */
char *strtok(char * __restrict s, char const * __restrict delim);

/*@ requires valid_string_delim: valid_read_string(delim);
    requires valid_saveptr: \valid(saveptr);
    assigns *(s + (0 ..)), *(*saveptr + (0 ..)), \result, *saveptr;
    assigns *(s + (0 ..))
      \from *(s + (0 ..)), (indirect: s), (indirect: *saveptr),
            (indirect: *(delim + (0 ..)));
    assigns *(*saveptr + (0 ..))
      \from *(*saveptr + (0 ..)), (indirect: s), (indirect: *saveptr),
            (indirect: *(delim + (0 ..)));
    assigns \result
      \from s, *saveptr, (indirect: *(s + (0 ..))),
            (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..)));
    assigns *saveptr
      \from \old(*saveptr), s, (indirect: *(*saveptr + (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 initialization: \initialized(\old(saveptr));
      ensures saveptr_subset: \subset(*\old(saveptr), \old(s) + (0 ..));
      assigns *saveptr, *(s + (0 ..)), \result;
      assigns *saveptr
        \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
      assigns *(s + (0 ..))
        \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
      assigns \result
        \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
    
    behavior resume_str:
      assumes s_null: s ≡ \null;
      requires not_first_call: *saveptr ≢ \null;
      requires saveptr: initialization: \initialized(saveptr);
      ensures
        result_subset:
          \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
      ensures
        saveptr_subset: \subset(*\old(saveptr), \old(*saveptr) + (0 ..));
      assigns *(*saveptr + (0 ..)), *saveptr, \result;
      assigns *(*saveptr + (0 ..))
        \from *(*saveptr + (0 ..)), (indirect: *saveptr),
              (indirect: *(delim + (0 ..)));
      assigns *saveptr
        \from \old(*saveptr), (indirect: *(*saveptr + (0 ..))),
              (indirect: *(delim + (0 ..)));
      assigns \result
        \from *saveptr, (indirect: *(*saveptr + (0 ..))),
              (indirect: *(delim + (0 ..)));
    
    complete behaviors resume_str, new_str;
    disjoint behaviors resume_str, new_str;
 */
char *strtok_r(char * __restrict s, char const * __restrict delim,
               char ** __restrict saveptr);

/*@ requires
      valid_string_stringp: \valid(stringp) ∧ valid_string(*stringp);
    requires valid_string_delim: valid_read_string(delim);
    assigns *stringp, \result;
    assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
    assigns \result \from *(delim + (..)), *(*(stringp + (..)));
 */
char *strsep(char **stringp, char const *delim);

char __fc_strerror[64];
char * const __fc_p_strerror = __fc_strerror;
/*@ ensures result_internal_str: \result ≡ __fc_p_strerror;
    ensures result_nul_terminated: *(\result + 63) ≡ 0;
    ensures result_valid_string: valid_read_string(\result);
    assigns \result;
    assigns \result \from __fc_p_strerror, (indirect: errnum);
 */
char *strerror(int errnum);

/*@ requires valid_string_src: valid_read_string(src);
    requires room_string: \valid(dest + (0 .. strlen(src)));
    requires
      separation:
        \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
    ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest + (0 .. strlen{Old}(src))), \result;
    assigns *(dest + (0 .. strlen{Old}(src)))
      \from *(src + (0 .. strlen{Old}(src)));
    assigns \result \from dest;
 */
char *strcpy(char * __restrict dest, char const * __restrict src);

/*@ requires valid_nstring_src: valid_read_nstring(src, n);
    requires room_nstring: \valid(dest + (0 .. n - 1));
    requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
    ensures result_ptr: \result ≡ \old(dest);
    ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
    assigns \result \from dest;
    
    behavior complete:
      assumes src_fits: strlen(src) < n;
      ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
    
    behavior partial:
      assumes src_too_long: n ≤ strlen(src);
      ensures
        equal_prefix:
          memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
 */
char *strncpy(char * __restrict dest, char const * __restrict src, size_t n);

/*@ requires valid_string_src: valid_read_string(src);
    requires room_nstring: \valid(dest + (0 .. n - 1));
    requires
      separation:
        \separated(
          dest + (0 .. n - 1), src + (0 .. \max(n - 1, strlen(src)))
          );
    ensures
      initialization:
        \initialized(\old(dest) + (0 .. \min(strlen(\old(src)), \old(n) - 1)));
    ensures bounded_result: \result ≡ strlen(\old(src));
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
    assigns \result
      \from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n);
 */
size_t strlcpy(char * __restrict dest, char const * __restrict src, size_t n);

/*@ requires valid_string_src: valid_read_string(src);
    requires room_string: \valid(dest + (0 .. strlen(src)));
    requires
      separation:
        \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
    ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
    ensures points_to_end: \result ≡ \old(dest) + strlen(\old(dest));
    assigns *(dest + (0 .. strlen{Old}(src))), \result;
    assigns *(dest + (0 .. strlen{Old}(src)))
      \from *(src + (0 .. strlen{Old}(src)));
    assigns \result \from dest;
 */
char *stpcpy(char * __restrict dest, char const * __restrict src);

/*@ requires valid_string_src: valid_read_string(src);
    requires valid_string_dest: valid_string(dest);
    requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
    ensures
      sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
    ensures
      dest: initialization:
        \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
    ensures
      dest_null_terminated:
        *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest +
              (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
            \result;
    assigns
    *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
      \from *(src + (0 .. strlen{Old}(src)));
    assigns \result \from dest;
 */
char *strcat(char * __restrict dest, char const * __restrict src);

/*@ requires valid_nstring_src: valid_read_nstring(src, n);
    requires valid_string_dest: valid_string(dest);
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
    assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
      \from *(src + (0 .. n));
    assigns \result \from dest;
    
    behavior complete:
      assumes
        valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
      requires
        room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
      ensures
        sum_of_lengths:
          strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
      assigns *(dest +
                (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
              \result;
      assigns
      *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
        \from *(src + (0 .. strlen{Old}(src)));
      assigns \result \from dest;
    
    behavior partial:
      assumes
        valid_string_src_too_large:
          ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
      requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
      ensures
        sum_of_bounded_lengths:
          strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
      assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
              \result;
      assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
        \from *(src + (0 .. strlen{Old}(src)));
      assigns \result \from dest;
 */
char *strncat(char * __restrict dest, char const * __restrict src, size_t n);

/*@ requires valid_string_src: valid_read_string(src);
    requires valid_string_dest: valid_string(dest);
    requires room_nstring: \valid(dest + (0 .. n - 1));
    ensures
      bounded_result: \result ≡ strlen(\old(dest)) + strlen(\old(src));
    assigns *(dest + (strlen{Old}(dest) .. n)), \result;
    assigns *(dest + (strlen{Old}(dest) .. n))
      \from (indirect: n), *(src + (0 .. strlen{Old}(src)));
    assigns \result
      \from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n);
 */
size_t strlcat(char * __restrict dest, char const * __restrict src, size_t n);

/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
    requires valid_string_src: valid_read_string(src);
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1))
      \from (indirect: *(src + (0 ..))), (indirect: n);
    assigns \result \from dest;
 */
size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);

/*@ requires valid_string_s: valid_read_string(s);
    assigns \result;
    assigns \result
      \from (indirect: *(s + (0 .. strlen{Old}(s)))),
            (indirect: __fc_heap_status);
    allocates \result;
    
    behavior allocation:
      assumes can_allocate: is_allocable(strlen(s));
      ensures allocation: \fresh{Old, Here}(\result,strlen(\old(s)));
      ensures
        result_valid_string_and_same_contents:
          valid_string(\result) ∧ strcmp(\result, \old(s)) ≡ 0;
      assigns __fc_heap_status, \result;
      assigns __fc_heap_status \from (indirect: s), __fc_heap_status;
      assigns \result
        \from (indirect: *(s + (0 .. strlen{Old}(s)))),
              (indirect: __fc_heap_status);
    
    behavior no_allocation:
      assumes cannot_allocate: ¬is_allocable(strlen(s));
      ensures result_null: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
 */
char *strdup(char const *s);

/*@ requires valid_string_s: valid_read_string(s);
    assigns \result;
    assigns \result
      \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
            (indirect: __fc_heap_status);
    allocates \result;
    
    behavior allocation:
      assumes can_allocate: is_allocable(\min(strlen(s), n + 1));
      ensures
        allocation:
          \fresh{Old, Here}(\result,\min(strlen(\old(s)), \old(n) + 1));
      ensures
        result_valid_string_bounded_and_same_prefix:
          \valid(\result + (0 .. \min(strlen(\old(s)), \old(n)))) ∧
          valid_string(\result) ∧ strlen(\result) ≤ \old(n) ∧
          strncmp(\result, \old(s), \old(n)) ≡ 0;
      assigns __fc_heap_status, \result;
      assigns __fc_heap_status
        \from (indirect: s), (indirect: n), __fc_heap_status;
      assigns \result
        \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
              (indirect: __fc_heap_status);
    
    behavior no_allocation:
      assumes cannot_allocate: ¬is_allocable(\min(strlen(s), n + 1));
      ensures result_null: \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
 */
char *strndup(char const *s, size_t n);

char __fc_strsignal[64];
char * const __fc_p_strsignal = __fc_strsignal;
/*@ ensures result_internal_str: \result ≡ __fc_p_strsignal;
    ensures result_nul_terminated: *(\result + 63) ≡ 0;
    ensures result_valid_string: valid_read_string(\result);
    assigns \result;
    assigns \result \from __fc_p_strsignal, (indirect: signum);
 */
char *strsignal(int signum);

/*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
    ensures
      initialization: s_initialized:
        \initialized((char *)\old(s) + (0 .. \old(n) - 1));
    ensures
      zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
    assigns *((char *)s + (0 .. n - 1));
    assigns *((char *)s + (0 .. n - 1)) \from \nothing;
 */
void bzero(void *s, 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 strcasecmp(char const *s1, char const *s2);

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

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[2];

/*@ requires \valid_read(this); */
void exception::Ctor(struct exception const *this);

/*@ requires \separated(this, exn);
    requires \valid_read(this);
    requires \valid_read(exn);
 */
void exception::Ctor(struct exception const *this,
                     struct exception const *exn);

/*@ requires \valid(this);
    requires \valid_read(exn);
    ensures \valid(\result);
 */
struct exception *operator=(struct exception *this,
                            struct exception const *exn);

/*@ requires \valid_read(this); */
void exception::Dtor(struct exception const *this);

/*@ requires \valid_read(this); */
char const *what(struct exception const *this);

void bad_exception::Dtor(struct bad_exception 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this); */
void bad_exception::Ctor(struct bad_exception const *this);

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void bad_exception::Ctor(struct bad_exception const *this,
                         struct bad_exception const *__frama_c_arg_0);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct bad_exception *operator=(struct bad_exception *this,
                                struct bad_exception const *__frama_c_arg_0);

/*@ requires \valid_read(this); */
char const *what(struct bad_exception const *this);

/*@ requires \valid_read(this); */
void bad_exception::Dtor(struct bad_exception const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
  return;
}

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 nested_exception::Ctor(struct nested_exception const *this);

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void nested_exception::Ctor(struct nested_exception const *this,
                            struct nested_exception const *__frama_c_arg_0);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct nested_exception *operator=(struct nested_exception *this,
                                   struct nested_exception const *__frama_c_arg_0);

/*@ requires \valid_read(this); */
void nested_exception::Dtor(struct nested_exception const *this);

/*@ requires \valid_read(this); */
void rethrow_nested(struct nested_exception const *this);

/*@ requires \valid_read(this); */
exception_ptr nested_ptr(struct nested_exception const *this);

int _frama_c_find_dynamic_cast_aux(struct _frama_c_rtti_name_info_node *target_info,
                                   struct _frama_c_rtti_name_info_content *concrete_base,
                                   int number_of_bases,
                                   int found_shift_object,
                                   int found_shift_vmt, int last_shift_vmt,
                                   int *shift_object, int *distance)
{
  int result = 0;
  struct _frama_c_rtti_name_info_content *cursor = concrete_base;
  int is_over = 0;
  int base_index = 0;
  while (base_index < number_of_bases) {
    if (cursor->value == target_info) {
      if (*distance < 0) goto _LOR;
      else 
        if (*distance >= 1) {
          _LOR:
          {
            if (found_shift_vmt == cursor->shift_vmt) *distance = 0;
            else *distance = 1;
            *shift_object = found_shift_object - cursor->shift_object;
            result = 1;
          }
        }
    }
    else 
      if (cursor->shift_vmt <= found_shift_vmt) {
        int tmp_5;
        if (base_index < number_of_bases - 1) tmp_5 = (cursor + 1)->shift_vmt > found_shift_vmt;
        else {
          int tmp_4;
          if (last_shift_vmt == -1) tmp_4 = 1;
          else 
            if (found_shift_vmt < last_shift_vmt) tmp_4 = 1; else tmp_4 = 0;
          tmp_5 = tmp_4;
        }
        if (tmp_5) {
          int tmp_0;
          int tmp;
          int local_distance = 0;
          int local_shift_object = 0;
          if (base_index < number_of_bases - 1) tmp = (cursor + 1)->shift_vmt;
          else tmp = last_shift_vmt;
          ;
          ;
          ;
          ;
          ;
          tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
                                                 (cursor->value)->base_classes,
                                                 (cursor->value)->number_of_base_classes,
                                                 found_shift_object - cursor->shift_object,
                                                 found_shift_vmt - cursor->shift_vmt,
                                                 tmp,& local_shift_object,
                                                 & local_distance);
          int local_result = tmp_0;
          if (local_result != 0) 
            if (local_distance >= 0) 
              if (*distance < 0) goto _LOR_0;
              else 
                if (*distance >= local_distance) {
                  _LOR_0:
                  {
                    result = local_result;
                    *shift_object = local_shift_object - cursor->shift_object;
                    *distance = local_distance;
                  }
                }
          is_over = 1;
        }
        else goto _LAND;
      }
      else {
        _LAND: ;
        if (*distance < 0) goto _LOR_2;
        else 
          if (*distance >= 1) {
            _LOR_2:
            {
              int tmp_2;
              int tmp_1;
              int local_distance_0 = 0;
              int local_shift_object_0 = 0;
              if (base_index < number_of_bases + 1) tmp_1 = (cursor + 1)->shift_vmt;
              else tmp_1 = last_shift_vmt;
              ;
              ;
              ;
              ;
              ;
              tmp_2 = _frama_c_find_dynamic_cast_aux(target_info,
                                                     (cursor->value)->base_classes,
                                                     (cursor->value)->number_of_base_classes,
                                                     found_shift_object - cursor->shift_object,
                                                     found_shift_vmt - cursor->shift_vmt,
                                                     tmp_1,
                                                     & local_shift_object_0,
                                                     & local_distance_0);
              int local_result_0 = tmp_2;
              if (local_result_0 != 0) 
                if (local_distance_0 >= 0) 
                  if (*distance < 0) goto _LOR_1;
                  else {
                    int tmp_3;
                    if (is_over == 0) tmp_3 = local_distance_0;
                    else tmp_3 = local_distance_0 + 1;
                    ;
                    if (*distance > tmp_3) {
                      _LOR_1:
                      {
                        result = local_result_0;
                        *shift_object = local_shift_object_0 - cursor->shift_object;
                        *distance = local_distance_0 + 1;
                      }
                    }
                  }
            }
          }
      }
    cursor ++;
    base_index ++;
  }
  return result;
}
int _frama_c_find_dynamic_cast(struct _frama_c_rtti_name_info_node *declared_info,
                               struct _frama_c_vmt *declared_vmt,
                               struct _frama_c_rtti_name_info_node *target_info,
                               int *shift_object)
{
  int __retres;
  int shift_vmt;
  int elaborated_shift_target;
  struct _frama_c_rtti_name_info_content *cursor;
  int number_of_bases;
  int tmp_0;
  struct _frama_c_rtti_name_info_node *concrete_info =
    declared_vmt->rtti_info;
  int elaborated_shift_vmt = 0;
  int elaborated_shift_object = 0;
  int cursor_index = 0;
  int distance = -1;
  if (concrete_info->pvmt > declared_vmt) {
    __retres = 0;
    goto return_label;
  }
  else 
    if (declared_vmt > concrete_info->pvmt + declared_vmt->table_size) {
      __retres = 0;
      goto return_label;
    }
  shift_vmt = declared_vmt - concrete_info->pvmt;
  if (concrete_info == declared_info) {
    *shift_object = 0;
    __retres = target_info == declared_info;
    goto return_label;
  }
  if (target_info == concrete_info) elaborated_shift_target = 0;
  else elaborated_shift_target = -1;
  cursor = concrete_info->base_classes;
  number_of_bases = concrete_info->number_of_base_classes;
  while (1) {
    while (1) {
      if (cursor_index < number_of_bases) {
        if (! (elaborated_shift_vmt + cursor->shift_vmt < shift_vmt)) 
          break;
      }
      else break;
      {
        struct _frama_c_rtti_name_info_content *tmp;
        if (cursor_index < number_of_bases - 1) tmp = cursor + 1;
        else tmp = (struct _frama_c_rtti_name_info_content *)0;
        struct _frama_c_rtti_name_info_content *next_cursor = tmp;
        if (next_cursor != (struct _frama_c_rtti_name_info_content *)0) 
          if (elaborated_shift_vmt + next_cursor->shift_vmt <= shift_vmt) {
            cursor = next_cursor;
            cursor_index ++;
          }
          else break;
        else break;
      }
    }
    if (cursor_index < number_of_bases) {
      elaborated_shift_vmt += cursor->shift_vmt;
      elaborated_shift_object += cursor->shift_object;
      if (cursor->value == target_info) elaborated_shift_target = elaborated_shift_object;
      if (elaborated_shift_vmt == shift_vmt) 
        if (cursor->value == declared_info) {
          if (elaborated_shift_target >= 0) {
            *shift_object = elaborated_shift_target - elaborated_shift_object;
            __retres = 1;
            goto return_label;
          }
          break;
        }
      cursor = (cursor->value)->base_classes;
      number_of_bases = (cursor->value)->number_of_base_classes;
      cursor_index = 0;
    }
    if (! (cursor_index < number_of_bases)) break;
  }
  if (cursor_index >= number_of_bases) {
    __retres = 0;
    goto return_label;
  }
  tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
                                         concrete_info->base_classes,
                                         concrete_info->number_of_base_classes,
                                         elaborated_shift_object,shift_vmt,
                                         -1,shift_object,& distance);
  __retres = tmp_0;
  return_label: return __retres;
}

struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& exception::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "exception",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& bad_exception::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what), .shift_this = 0}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct bad_exception *)0)->_frama_c__ZN3stdE9exception),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "bad_exception",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[1] =
  {{.method_ptr = (void (*)())(& nested_exception::Dtor), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "nested_exception",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 1,
   .rtti_info = & _frama_c_rtti_name_info};
int __fc_errno;
char *program_invocation_name;
char *program_invocation_short_name;
/*@ assigns \nothing; */
void (*signal(int sig, void (*func)(int )))(int );

/*@ ensures never_terminates: \false;
    assigns \nothing; */
int raise(int sig);

/*@ requires valid_set: \valid(set);
    ensures set: initialization: \initialized(\old(set));
    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns *set, \result;
    assigns *set \from \nothing;
    assigns \result \from \nothing;
 */
int sigemptyset(sigset_t *set);

/*@ requires valid_set: \valid(set);
    ensures set: initialization: \initialized(\old(set));
    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns *set, \result;
    assigns *set \from \nothing;
    assigns \result \from \nothing;
 */
int sigfillset(sigset_t *set);

/*@ requires valid_set: \valid(set);
    requires set: initialization: \initialized(set);
    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns *set, \result;
    assigns *set \from (indirect: signum);
    assigns \result \from signum;
 */
int sigaddset(sigset_t *set, int signum);

/*@ requires valid_set: \valid(set);
    requires set: initialization: \initialized(set);
    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns *set, \result;
    assigns *set \from (indirect: signum);
    assigns \result \from signum;
 */
int sigdelset(sigset_t *set, int signum);

/*@ requires valid_read_set: \valid_read(set);
    requires set: initialization: \initialized(set);
    ensures
      result_found_not_found_or_error:
        \result ≡ 0 ∨ \result ≡ 1 ∨ \result ≡ -1;
    assigns \result;
    assigns \result \from *set, signum;
 */
int sigismember(sigset_t const *set, int signum);

struct sigaction __fc_sigaction[65];
struct sigaction *__fc_p_sigaction = __fc_sigaction;
/*@ requires valid_signal: 0 ≤ signum ≤ 64;
    requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact);
    requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act);
    requires separated_acts: separation: \separated(act, oldact);
    ensures
      act_changed:
        \old(act) ≡ \null ∨
        \subset(*(__fc_p_sigaction + \old(signum)), *\old(act));
    ensures
      oldact_assigned:
        \old(oldact) ≡ \null ∨
        *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns *oldact, *(__fc_p_sigaction + signum), \result;
    assigns *oldact \from __fc_p_sigaction;
    assigns *(__fc_p_sigaction + signum) \from *act;
    assigns \result
      \from (indirect: signum), (indirect: act), (indirect: *act),
            (indirect: oldact), (indirect: *oldact);
 */
int sigaction(int signum, struct sigaction const * __restrict act,
              struct sigaction * __restrict oldact);

/*@ requires valid_set_or_null: set ≡ \null ∨ \valid_read(set); */
int sigprocmask(int how, sigset_t const * __restrict set,
                sigset_t * __restrict oldset);

/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns \result;
    assigns \result \from (indirect: pid), (indirect: sig);
 */
int kill(pid_t pid, int sig);

/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
    assigns \result;
    assigns \result \from (indirect: pgrp), (indirect: sig);
 */
int killpg(pid_t pgrp, int sig);

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

/*@ ghost unsigned int volatile __fc_time; */
/*@ assigns \result;
    assigns \result \from __fc_time; */
clock_t clock(void);

/*@ assigns \result;
    assigns \result \from time1, time0; */
double difftime(time_t time1, time_t time0);

/*@ requires valid_timeptr: \valid(timeptr);
    assigns *timeptr, \result;
    assigns *timeptr \from *timeptr;
    assigns \result \from (indirect: *timeptr);
 */
time_t mktime(struct tm *timeptr);

/*@ assigns *timer, \result;
    assigns *timer \from __fc_time;
    assigns \result \from __fc_time;
    
    behavior null:
      assumes timer_null: timer ≡ \null;
      assigns \result;
      assigns \result \from __fc_time;
    
    behavior not_null:
      assumes timer_non_null: timer ≢ \null;
      requires valid_timer: \valid(timer);
      ensures timer: initialization: \initialized(\old(timer));
      assigns *timer, \result;
      assigns *timer \from __fc_time;
      assigns \result \from __fc_time;
    
    complete behaviors not_null, null;
    disjoint behaviors not_null, null;
 */
time_t time(time_t *timer);

char __fc_ctime[26];
char * const __fc_p_ctime = __fc_ctime;
/*@ requires valid_timeptr: \valid_read(timeptr);
    requires init_timeptr: initialization: \initialized(timeptr);
    ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
    ensures result_valid_string: valid_read_string(__fc_p_ctime);
    assigns __fc_ctime[0 .. 25], \result;
    assigns __fc_ctime[0 .. 25]
      \from (indirect: *timeptr), (indirect: __fc_time);
    assigns \result
      \from (indirect: *timeptr), (indirect: __fc_time), __fc_p_ctime;
 */
char *asctime(struct tm const *timeptr);

/*@ requires valid_timer: \valid_read(timer);
    requires init_timer: initialization: \initialized(timer);
    ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
    ensures result_valid_string: valid_read_string(__fc_p_ctime);
    assigns __fc_ctime[0 .. 25], \result;
    assigns __fc_ctime[0 .. 25]
      \from (indirect: *timer), (indirect: __fc_time);
    assigns \result
      \from (indirect: *timer), (indirect: __fc_time), __fc_p_ctime;
 */
char *ctime(time_t const *timer);

struct tm __fc_time_tm;
void __fc_init__fc_time_tm(void) __attribute__((__constructor__));
void __fc_init__fc_time_tm(void)
{
  tm::Ctor((struct tm const *)(& __fc_time_tm));
  return;
}

struct tm * const __fc_p_time_tm = & __fc_time_tm;
/*@ requires valid_timer: \valid_read(timer);
    ensures
      result_null_or_internal_tm:
        \result ≡ &__fc_time_tm ∨ \result ≡ \null;
    assigns \result, __fc_time_tm;
    assigns \result \from __fc_p_time_tm;
    assigns __fc_time_tm \from *timer;
 */
struct tm *gmtime(time_t const *timer);

/*@ requires valid_timer: \valid_read(timer);
    ensures
      result_null_or_internal_tm:
        \result ≡ &__fc_time_tm ∨ \result ≡ \null;
    assigns \result, __fc_time_tm;
    assigns \result \from __fc_p_time_tm;
    assigns __fc_time_tm \from *timer;
 */
struct tm *localtime(time_t const *timer);

/*@ requires dst_has_room: \valid(s + (0 .. max - 1));
    requires valid_format: valid_read_string(format);
    requires valid_tm: \valid_read(tm);
    ensures result_bounded: \result ≤ \old(max);
    assigns *(s + (0 .. max - 1)), \result;
    assigns *(s + (0 .. max - 1))
      \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
    assigns \result
      \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
 */
size_t strftime(char * __restrict s, size_t max,
                char const * __restrict format,
                struct tm const * __restrict tm);

/*@ requires tp: \valid(tp);
    assigns \result, *tp, __fc_time;
    assigns \result \from __fc_time;
    assigns *tp \from __fc_time;
    assigns __fc_time \from __fc_time;
    
    behavior realtime_clock:
      assumes realtime: clk_id ≡ 666;
      ensures success: \result ≡ 0;
      ensures initialization: \initialized(\old(tp));
    
    behavior monotonic_clock:
      assumes monotonic: clk_id ≡ 1;
      ensures success: \result ≡ 0;
      ensures initialization: \initialized(\old(tp));
    
    behavior bad_clock_id:
      assumes bad_id: clk_id ≢ 666 ∧ clk_id ≢ 1;
      ensures error: \result ≡ 22;
      assigns \result;
      assigns \result \from clk_id;
    
    complete behaviors bad_clock_id, monotonic_clock, realtime_clock;
    disjoint behaviors bad_clock_id, monotonic_clock, realtime_clock;
 */
int clock_gettime(clockid_t clk_id, struct timespec *tp);

/*@
axiomatic nanosleep_predicates {
  predicate abs_clock_in_range{L}(clockid_t id, struct timespec *tm) 
    reads __fc_time;
  
  predicate valid_clock_id{L}(clockid_t id) 
    reads __fc_time;
  
  }

*/
/*@ ghost int volatile __fc_interrupted; */
/*@ requires valid_request: \valid_read(rqtp);
    requires
      initialized_request: initialization:
        \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
    requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
    requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
    assigns \result;
    assigns \result
      \from (indirect: __fc_time), (indirect: __fc_interrupted),
            (indirect: clock_id), (indirect: flags), (indirect: rqtp),
            (indirect: *rqtp);
    
    behavior absolute:
      assumes absolute_time: (flags & 1) ≢ 0;
      assumes
        no_einval:
          abs_clock_in_range(clock_id, rqtp) ∧ valid_clock_id(clock_id);
      ensures
        result_ok_or_error:
          \result ≡ 0 ∨ \result ≡ 4 ∨ \result ≡ 22 ∨
          \result ≡ 95;
      assigns \result;
      assigns \result
        \from (indirect: __fc_time), (indirect: __fc_interrupted),
              (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp);
    
    behavior relative_interrupted:
      assumes relative_time: (flags & 1) ≡ 0;
      assumes interrupted: __fc_interrupted ≢ 0;
      assumes no_einval: valid_clock_id(clock_id);
      ensures result_interrupted: \result ≡ 4;
      ensures
        interrupted_remaining: initialization:
          \old(rmtp) ≢ \null ⇒
          \initialized(&\old(rmtp)->tv_sec) ∧
          \initialized(&\old(rmtp)->tv_nsec);
      ensures
        interrupted_remaining_decreases:
          \old(rmtp) ≢ \null ⇒
          \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
          \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
      ensures
        remaining_valid:
          \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
      assigns \result, *rmtp;
      assigns \result
        \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
              (indirect: *rqtp);
      assigns *rmtp
        \from __fc_time, (indirect: clock_id), (indirect: rqtp),
              (indirect: *rqtp), (indirect: rmtp);
    
    behavior relative_no_error:
      assumes relative_time: (flags & 1) ≡ 0;
      assumes not_interrupted: __fc_interrupted ≡ 0;
      assumes no_einval: valid_clock_id(clock_id);
      ensures result_ok: \result ≡ 0;
      assigns \result;
      assigns \result
        \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
              (indirect: *rqtp);
    
    behavior relative_invalid_clock_id:
      assumes relative_time: (flags & 1) ≡ 0;
      assumes not_interrupted: __fc_interrupted ≡ 0;
      assumes einval: ¬valid_clock_id(clock_id);
      ensures result_einval: \result ≡ 22;
      assigns \result;
      assigns \result
        \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
              (indirect: *rqtp);
    
    complete behaviors relative_invalid_clock_id,
                       relative_no_error,
                       relative_interrupted,
                       absolute;
    disjoint behaviors relative_invalid_clock_id,
                       relative_no_error,
                       relative_interrupted,
                       absolute;
 */
int clock_nanosleep(clockid_t clock_id, int flags,
                    struct timespec const *rqtp, struct timespec *rmtp);

/*@ requires valid_timer: \valid_read(timer);
    requires valid_result: \valid(result);
    ensures
      result_null_or_result: \result ≡ \old(result) ∨ \result ≡ \null;
    assigns \result, *result;
    assigns \result \from (indirect: *timer), result;
    assigns *result \from (indirect: *timer);
 */
struct tm *gmtime_r(time_t const * __restrict timer,
                    struct tm * __restrict result);

/*@ requires valid_request: \valid_read(rqtp);
    requires
      initialized_request: initialization:
        \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
    requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
    requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
    ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
    ensures
      interrupted_remaining: initialization:
        \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
        \initialized(&\old(rmtp)->tv_sec) ∧
        \initialized(&\old(rmtp)->tv_nsec);
    ensures
      interrupted_remaining_decreases:
        \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
        \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
        \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
    ensures
      interrupted_remaining_valid:
        \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
        0 ≤ \old(rmtp)->tv_nsec < 1000000000;
    assigns \result, *rmtp;
    assigns \result
      \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
    assigns *rmtp
      \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
            (indirect: rmtp);
 */
int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);

int daylight;
long timezone;
char *tzname[2];
/*@ assigns *(tzname[0 .. 1] + (0 ..));
    assigns *(tzname[0 .. 1] + (0 ..)) \from \nothing;
 */
void tzset(void);

/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
    requires valid_dest: \valid(dest + (0 .. n - 1));
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1))
      \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
    assigns \result \from dest;
 */
int *wmemmove(int *dest, int const *src, size_t n);

/*@ requires valid_wcs: \valid(wcs + (0 .. n - 1));
    ensures result_ptr: \result ≡ \old(wcs);
    ensures
      wcs: initialization: \initialized(\old(wcs) + (0 .. \old(n) - 1));
    ensures
      contents_equal_wc: \subset(*(\old(wcs) + (0 .. \old(n) - 1)), \old(wc));
    assigns *(wcs + (0 .. n - 1)), \result;
    assigns *(wcs + (0 .. n - 1)) \from wc, (indirect: n);
    assigns \result \from wcs;
 */
int *wmemset(int *wcs, int wc, size_t n);

/*@ requires valid_wstring_src: valid_read_wstring(src);
    requires valid_wstring_dest: valid_wstring(dest);
    requires
      room_for_concatenation:
        \valid(dest + (wcslen(dest) .. wcslen(dest) + wcslen(src)));
    requires
      separation:
        \separated(
          dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
          );
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest + (0 ..)), \result;
    assigns *(dest + (0 ..))
      \from *(dest + (0 ..)), (indirect: dest), *(src + (0 ..)),
            (indirect: src);
    assigns \result \from dest;
 */
int *wcscat(int * __restrict dest, int const * __restrict src);

/*@ requires valid_wstring_src: valid_read_wstring(wcs);
    ensures
      result_null_or_inside_wcs:
        \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
    assigns \result;
    assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
 */
int *wcschr(int const *wcs, int wc);

/*@ requires valid_wstring_s1: valid_read_wstring(s1);
    requires valid_wstring_s2: valid_read_wstring(s2);
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
 */
int wcscmp(int const *s1, int const *s2);

/*@ requires valid_wstring_src: valid_read_wstring(src);
    requires room_wstring: \valid(dest + (0 .. wcslen(src)));
    requires
      separation:
        \separated(dest + (0 .. wcslen(src)), src + (0 .. wcslen(src)));
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest + (0 .. wcslen{Old}(src))), \result;
    assigns *(dest + (0 .. wcslen{Old}(src)))
      \from *(src + (0 .. wcslen{Old}(src))), (indirect: src);
    assigns \result \from dest;
 */
int *wcscpy(int * __restrict dest, int const * __restrict src);

/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
    requires valid_wstring_accept: valid_read_wstring(accept);
    assigns \result;
    assigns \result
      \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
 */
size_t wcscspn(int const *wcs, int const *accept);

/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
    requires valid_wstring_dest: valid_wstring(dest);
    requires
      room_for_concatenation:
        \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
    requires
      separation:
        \separated(
          dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
          );
    assigns *(dest + (0 ..)), \result;
    assigns *(dest + (0 ..))
      \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
            (indirect: src), (indirect: n);
    assigns \result
      \from (indirect: *(dest + (0 ..))), (indirect: *(src + (0 .. n - 1))),
            (indirect: n);
 */
size_t wcslcat(int * __restrict dest, int const * __restrict src, size_t n);

/*@ requires valid_wstring_src: valid_read_wstring(src);
    requires room_nwstring: \valid(dest + (0 .. n));
    requires
      src: dest: separation:
        \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1))
      \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
    assigns \result
      \from (indirect: *(dest + (0 .. n - 1))), (indirect: dest),
            (indirect: *(src + (0 .. n - 1))), (indirect: src), (indirect: n);
 */
size_t wcslcpy(int *dest, int const *src, size_t n);

/*@ requires valid_string_s: valid_read_wstring(s);
    ensures result_is_length: \result ≡ wcslen(\old(s));
    assigns \result;
    assigns \result \from (indirect: *(s + (0 .. wcslen{Old}(s))));
 */
size_t wcslen(int const *s);

/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
    requires valid_wstring_dest: valid_wstring(dest);
    requires
      room_for_concatenation:
        \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
    requires
      separation:
        \separated(
          dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
          );
    ensures result_ptr: \result ≡ \old(dest);
    assigns *(dest + (0 ..)), \result;
    assigns *(dest + (0 ..))
      \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
            (indirect: src), (indirect: n);
    assigns \result \from dest;
 */
int *wcsncat(int * __restrict dest, int const * __restrict src, size_t n);

/*@ requires valid_wstring_s1: valid_read_wstring(s1);
    requires valid_wstring_s2: valid_read_wstring(s2);
    assigns \result;
    assigns \result
      \from (indirect: *(s1 + (0 .. n - 1))),
            (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
 */
int wcsncmp(int const *s1, int const *s2, size_t n);

/*@ requires valid_wstring_src: valid_read_wstring(src);
    requires room_nwstring: \valid(dest + (0 .. n - 1));
    requires
      src: dest: separation:
        \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
    ensures result_ptr: \result ≡ \old(dest);
    ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1))
      \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
    assigns \result \from dest;
 */
int *wcsncpy(int * __restrict dest, int const * __restrict src, size_t n);

/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
    requires valid_wstring_accept: valid_read_wstring(accept);
    ensures
      result_null_or_inside_wcs:
        \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
    assigns \result;
    assigns \result
      \from wcs, (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
 */
int *wcspbrk(int const *wcs, int const *accept);

/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
    ensures
      result_null_or_inside_wcs:
        \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
    assigns \result;
    assigns \result
      \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
 */
int *wcsrchr(int const *wcs, int wc);

/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
    requires valid_wstring_accept: valid_read_wstring(accept);
    assigns \result;
    assigns \result
      \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
            (indirect: *(accept + (0 .. wcslen{Old}(accept))));
 */
size_t wcsspn(int const *wcs, int const *accept);

/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
    requires valid_wstring_needle: valid_read_wstring(needle);
    ensures
      result_null_or_inside_haystack:
        \result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
    assigns \result;
    assigns \result
      \from haystack, (indirect: *(haystack + (0 ..))),
            (indirect: *(needle + (0 ..)));
 */
int *wcsstr(int const *haystack, int const *needle);

/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
    requires valid_stream: \valid(stream);
    ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
    ensures
      terminated_string_on_success:
        \result ≢ \null ⇒ valid_wstring(\old(ws));
    assigns *(ws + (0 .. n - 1)), \result;
    assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
    assigns \result \from ws, (indirect: n), (indirect: *stream);
 */
int *fgetws(int * __restrict ws, int n, FILE * __restrict stream);

/*@ axiomatic wformat_length {
      logic ℤ wformat_length{L}(int *format) ;
      
      }

*/
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(c2);
    requires \valid(c1); */
void assign(char_type *c1, char_type const *c2);

/*@ requires \valid_read(a); */
char_type const *find(char_type const *s, size_t n, char_type const *a);

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(c2);
    requires \valid(c1); */
void assign(char_type *c1, char_type const *c2);

/*@ requires \valid_read(a); */
char_type const *find(char_type const *s, size_t n, char_type const *a);

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "char_traits",
   .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 = "char_traits",
   .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::Ctor(struct piecewise_construct_t const *this,
                                 struct piecewise_construct_t const *__frama_c_arg_0);

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

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 \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this,
                                 struct piecewise_construct_t const *__frama_c_arg_0)
{
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid(__frama_c_arg_0);
 */
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this,
                                 struct piecewise_construct_t *__frama_c_arg_0)
{
  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};
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 __shared_ref_base *operator=(struct __shared_ref_base *this,
                                    struct __shared_ref_base const *__frama_c_arg_0);

struct __shared_ref_base *operator=(struct __shared_ref_base *this,
                                    struct __shared_ref_base *__frama_c_arg_0);

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

void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
                             struct __shared_ref_base const *__frama_c_arg_0);

void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
                             struct __shared_ref_base *__frama_c_arg_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[7];

/*@ requires \valid(this); */
void unlink(struct __shared_ref_base *this);

/*@ requires \valid(this); */
void link(struct __shared_ref_base *this);

/*@ requires \valid(this); */
long count(struct __shared_ref_base *this);

/*@ requires \valid(this); */
void weak_unlink(struct __shared_ref_base *this);

/*@ requires \valid(this); */
void weak_link(struct __shared_ref_base *this);

/*@ requires \valid(this); */
struct __shared_ref_base *ref(struct __shared_ref_base *this);

/*@ requires \valid(this); */
void *get_deleter(struct __shared_ref_base *this)
{
  void *__retres;
  __retres = (void *)0;
  return __retres;
}

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct __shared_ref_base *operator=(struct __shared_ref_base *this,
                                    struct __shared_ref_base const *__frama_c_arg_0)
{
  this->pvmt = __frama_c_arg_0->pvmt;
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct __shared_ref_base *operator=(struct __shared_ref_base *this,
                                    struct __shared_ref_base *__frama_c_arg_0)
{
  this->pvmt = __frama_c_arg_0->pvmt;
  return this;
}

/*@ requires \valid_read(this); */
void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
                             struct __shared_ref_base const *__frama_c_arg_0)
{
  this->pvmt = __frama_c_arg_0->pvmt;
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid(__frama_c_arg_0);
 */
void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
                             struct __shared_ref_base *__frama_c_arg_0)
{
  this->pvmt = __frama_c_arg_0->pvmt;
  return;
}

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "allocator",
   .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_content _frama_c_vmt[7] =
  {{.method_ptr = (void (*)())(& unlink), .shift_this = 0},
   {.method_ptr = (void (*)())(& link), .shift_this = 0},
   {.method_ptr = (void (*)())(& count), .shift_this = 0},
   {.method_ptr = (void (*)())(& weak_unlink), .shift_this = 0},
   {.method_ptr = (void (*)())(& weak_link), .shift_this = 0},
   {.method_ptr = (void (*)())(& ref), .shift_this = 0},
   {.method_ptr = (void (*)())(& get_deleter), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "__shared_ref_base",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 7,
   .rtti_info = & _frama_c_rtti_name_info};
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
                                     struct __shared_ref<void> const *__frama_c_arg_0);

struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
                                     struct __shared_ref<void> *__frama_c_arg_0);

void __shared_ref<void>::Dtor(struct __shared_ref<void> const *this);

void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
                              struct __shared_ref<void> const *__frama_c_arg_0);

void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
                              struct __shared_ref<void> *__frama_c_arg_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[7];

/*@ requires \valid_read(this); */
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this, void *p);

/*@ requires \valid(this); */
void unlink(struct __shared_ref<void> *this);

/*@ requires \valid(this); */
void link(struct __shared_ref<void> *this);

/*@ requires \valid(this); */
long count(struct __shared_ref<void> *this);

/*@ requires \valid(this); */
void weak_unlink(struct __shared_ref<void> *this);

/*@ requires \valid(this); */
void weak_link(struct __shared_ref<void> *this);

/*@ requires \valid(this); */
struct __shared_ref_base *ref(struct __shared_ref<void> *this);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
                                     struct __shared_ref<void> const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE17__shared_ref_base,
            & __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
  this->__ptr = __frama_c_arg_0->__ptr;
  this->_n = __frama_c_arg_0->_n;
  this->_w = __frama_c_arg_0->_w;
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
                                     struct __shared_ref<void> *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE17__shared_ref_base,
            & __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
  this->__ptr = __frama_c_arg_0->__ptr;
  this->_n = __frama_c_arg_0->_n;
  this->_w = __frama_c_arg_0->_w;
  return this;
}

/*@ requires \valid_read(this); */
void __shared_ref<void>::Dtor(struct __shared_ref<void> const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  __shared_ref_base::Dtor(& this->_frama_c__ZN3stdE17__shared_ref_base);
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
                              struct __shared_ref<void> const *__frama_c_arg_0)
{
  __shared_ref_base::Ctor(& this->_frama_c__ZN3stdE17__shared_ref_base,
                          & __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
  this->__ptr = __frama_c_arg_0->__ptr;
  this->_n = __frama_c_arg_0->_n;
  this->_w = __frama_c_arg_0->_w;
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid(__frama_c_arg_0);
 */
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
                              struct __shared_ref<void> *__frama_c_arg_0)
{
  __shared_ref_base::Ctor(& this->_frama_c__ZN3stdE17__shared_ref_base,
                          & __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
  this->__ptr = __frama_c_arg_0->__ptr;
  this->_n = __frama_c_arg_0->_n;
  this->_w = __frama_c_arg_0->_w;
  return;
}

struct _frama_c_vmt_content _frama_c_vmt[7] =
  {{.method_ptr = (void (*)())(& unlink), .shift_this = 0},
   {.method_ptr = (void (*)())(& link), .shift_this = 0},
   {.method_ptr = (void (*)())(& count), .shift_this = 0},
   {.method_ptr = (void (*)())(& weak_unlink), .shift_this = 0},
   {.method_ptr = (void (*)())(& weak_link), .shift_this = 0},
   {.method_ptr = (void (*)())(& ref), .shift_this = 0},
   {.method_ptr = (void (*)())(& get_deleter),
    .shift_this = (char *)(& ((struct __shared_ref<void> *)0)->_frama_c__ZN3stdE17__shared_ref_base) - (char *)(& ((struct __shared_ref<void> *)0)->_frama_c__ZN3stdE17__shared_ref_base)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct __shared_ref<void> *)0)->_frama_c__ZN3stdE17__shared_ref_base),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "__shared_ref",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 7,
   .rtti_info = & _frama_c_rtti_name_info};
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];
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
                        struct bad_weak_ptr const *__frama_c_arg_0);

void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
                        struct bad_weak_ptr *__frama_c_arg_0);

struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
                               struct bad_weak_ptr const *__frama_c_arg_0);

struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
                               struct bad_weak_ptr *__frama_c_arg_0);

void bad_weak_ptr::Dtor(struct bad_weak_ptr 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this); */
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception);
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
                        struct bad_weak_ptr const *__frama_c_arg_0)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception,
                  & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return;
}

void exception::Ctor(struct exception const *this,
                     struct exception *__frama_c_arg_0)
{
  this->pvmt = __frama_c_arg_0->pvmt;
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid(__frama_c_arg_0);
 */
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
                        struct bad_weak_ptr *__frama_c_arg_0)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception,
                  & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return;
}

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
                               struct bad_weak_ptr const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE9exception,
            & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return this;
}

struct exception *operator=(struct exception *this,
                            struct exception *__frama_c_arg_0)
{
  this->pvmt = __frama_c_arg_0->pvmt;
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
                               struct bad_weak_ptr *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE9exception,
            & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return this;
}

/*@ requires \valid_read(this); */
void bad_weak_ptr::Dtor(struct bad_weak_ptr const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
  return;
}

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 shared_ptr<void>::Ctor(struct shared_ptr<void> const *this)
{
  this->_ref = (struct __shared_ref_base *)0;
  return;
}

void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
                            struct shared_ptr<void> const *r);

/*@ requires \separated(this, r);
    requires \valid_read(this);
    requires \valid(r);
 */
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
                            struct shared_ptr<void> *r)
{
  this->__ptr = r->__ptr;
  this->_ref = r->_ref;
  r->__ptr = (void *)0;
  r->_ref = (struct __shared_ref_base *)0;
  return;
}

/*@ requires \valid_read(this); */
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
                            nullptr_t __frama_c_arg_0)
{
  this->_ref = (struct __shared_ref_base *)0;
  return;
}

/*@ requires \valid_read(this); */
void shared_ptr<void>::Dtor(struct shared_ptr<void> const *this)
{
  if (this->_ref != (struct __shared_ref_base *)0) {
    struct _frama_c_vmt_content *__virtual_tmp_0 =
      (*((struct _frama_c_vmt **)this->_ref))->table + 0;
    (*((void (*)(struct __shared_ref_base *))__virtual_tmp_0->method_ptr))
    ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_0->shift_this));
  }
  return;
}

/*@ requires \valid(this);
    requires \valid_read(r);
    ensures \valid(\result); */
struct shared_ptr<void> *operator=(struct shared_ptr<void> *this,
                                   struct shared_ptr<void> const *r)
{
  if (this->_ref != r->_ref) {
    this->__ptr = r->__ptr;
    if (this->_ref != (struct __shared_ref_base *)0) {
      struct _frama_c_vmt_content *__virtual_tmp_1 =
        (*((struct _frama_c_vmt **)this->_ref))->table + 0;
      (*((void (*)(struct __shared_ref_base *))__virtual_tmp_1->method_ptr))
      ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_1->shift_this));
    }
    this->_ref = r->_ref;
    if (this->_ref != (struct __shared_ref_base *)0) {
      struct _frama_c_vmt_content *__virtual_tmp_2 =
        (*((struct _frama_c_vmt **)this->_ref))->table + 1;
      (*((void (*)(struct __shared_ref_base *))__virtual_tmp_2->method_ptr))
      ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_2->shift_this));
    }
  }
  return this;
}

/*@ requires \valid(this);
    requires \valid(r);
    ensures \valid(\result); */
struct shared_ptr<void> *operator=(struct shared_ptr<void> *this,
                                   struct shared_ptr<void> *r)
{
  if (this->_ref != (struct __shared_ref_base *)0) {
    struct _frama_c_vmt_content *__virtual_tmp_3 =
      (*((struct _frama_c_vmt **)this->_ref))->table + 0;
    (*((void (*)(struct __shared_ref_base *))__virtual_tmp_3->method_ptr))
    ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_3->shift_this));
  }
  if (this->_ref != r->_ref) {
    this->__ptr = r->__ptr;
    this->_ref = r->_ref;
  }
  r->_ref = (struct __shared_ref_base *)0;
  return this;
}

/*@ requires \valid(this);
    requires \valid(r); */
void swap(struct shared_ptr<void> *this, struct shared_ptr<void> *r)
{
  if (this->_ref != r->_ref) {
    swap<void*>(& this->__ptr,& r->__ptr);
    swap<std::__shared_ref_base*>(& this->_ref,& r->_ref);
  }
  return;
}

/*@ requires \valid(this); */
void reset(struct shared_ptr<void> *this)
{
  if (this->_ref != (struct __shared_ref_base *)0) {
    struct _frama_c_vmt_content *__virtual_tmp_4 =
      (*((struct _frama_c_vmt **)this->_ref))->table + 0;
    (*((void (*)(struct __shared_ref_base *))__virtual_tmp_4->method_ptr))
    ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_4->shift_this));
    this->_ref = (struct __shared_ref_base *)0;
  }
  return;
}

/*@ requires \valid_read(this); */
void *get(struct shared_ptr<void> const *this)
{
  void *__retres;
  __retres = this->__ptr;
  return __retres;
}

/*@ requires \valid_read(this); */
void *std::shared_ptr<void>::operator->(struct shared_ptr<void> const *this)
{
  void *tmp;
  tmp = get(this);
  return tmp;
}

/*@ requires \valid_read(this); */
long use_count(struct shared_ptr<void> const *this)
{
  long tmp_0;
  struct _frama_c_vmt_content *__virtual_tmp_5 =
    (*((struct _frama_c_vmt **)this->_ref))->table + 2;
  if (this->_ref == (struct __shared_ref_base *)0) tmp_0 = 0L;
  else tmp_0 = (*((long (*)(struct __shared_ref_base *))__virtual_tmp_5->method_ptr))
       ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_5->shift_this));
  return tmp_0;
}

/*@ requires \valid_read(this); */
_Bool unique(struct shared_ptr<void> const *this)
{
  _Bool __retres;
  int tmp_0;
  struct _frama_c_vmt_content *__virtual_tmp_6 =
    (*((struct _frama_c_vmt **)this->_ref))->table + 2;
  if (this->_ref == (struct __shared_ref_base *)0) tmp_0 = 0;
  else {
    long tmp;
    tmp = (*((long (*)(struct __shared_ref_base *))__virtual_tmp_6->method_ptr))
    ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_6->shift_this));
    tmp_0 = tmp == 1L;
  }
  __retres = (_Bool)(tmp_0 != 0);
  return __retres;
}

/*@ requires \valid_read(this); */
_Bool conversion(bool)(struct shared_ptr<void> const *this)
{
  _Bool __retres;
  __retres = (_Bool)(this->__ptr != (void *)0);
  return __retres;
}

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "auto_ptr",
   .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_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& bad_weak_ptr::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct bad_weak_ptr *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct bad_weak_ptr *)0)->_frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct bad_weak_ptr *)0)->_frama_c__ZN3stdE9exception),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "bad_weak_ptr",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
/*@ requires \separated(this, r);
    requires \valid_read(this);
    requires \valid_read(r);
 */
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
                            struct shared_ptr<void> const *r)
{
  struct _frama_c_vmt_content *__virtual_tmp_7 =
    (*((struct _frama_c_vmt **)r->_ref))->table + 5;
  if (r->_ref == (struct __shared_ref_base *)0) this->_ref = (struct __shared_ref_base *)0;
  else this->_ref = (*((struct __shared_ref_base *(*)(struct __shared_ref_base *))__virtual_tmp_7->method_ptr))
       ((struct __shared_ref_base *)((char *)r->_ref - __virtual_tmp_7->shift_this));
  if (this->_ref != (struct __shared_ref_base *)0) {
    this->__ptr = get(r);
    struct _frama_c_vmt_content *__virtual_tmp_8 =
      (*((struct _frama_c_vmt **)this->_ref))->table + 1;
    (*((void (*)(struct __shared_ref_base *))__virtual_tmp_8->method_ptr))
    ((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_8->shift_this));
  }
  else this->__ptr = (void *)0;
  return;
}

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "shared_ptr",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};
/*@ requires \valid_read(str); */
int stoi(string const *str, size_t *idx, int base);

/*@ requires \valid_read(str); */
long stol(string const *str, size_t *idx, int base);

/*@ requires \valid_read(str); */
unsigned long stoul(string const *str, size_t *idx, int base);

/*@ requires \valid_read(str); */
long long stoll(string const *str, size_t *idx, int base);

/*@ requires \valid_read(str); */
unsigned long long stoull(string const *str, size_t *idx, int base);

/*@ requires \valid_read(str); */
float stof(string const *str, size_t *idx);

/*@ requires \valid_read(str); */
double stod(string const *str, size_t *idx);

/*@ requires \valid_read(str); */
long double stold(string const *str, size_t *idx);

void logic_error::Ctor(struct logic_error const *this,
                       struct logic_error const *__frama_c_arg_0);

void logic_error::Ctor(struct logic_error const *this,
                       struct logic_error *__frama_c_arg_0);

struct logic_error *operator=(struct logic_error *this,
                              struct logic_error const *__frama_c_arg_0);

struct logic_error *operator=(struct logic_error *this,
                              struct logic_error *__frama_c_arg_0);

void logic_error::Dtor(struct logic_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void logic_error::Ctor(struct logic_error const *this, string const *what_arg);

/*@ requires \valid_read(this); */
void logic_error::Ctor(struct logic_error const *this, char const *what_arg);

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void logic_error::Ctor(struct logic_error const *this,
                       struct logic_error const *__frama_c_arg_0)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception,
                  & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid(__frama_c_arg_0);
 */
void logic_error::Ctor(struct logic_error const *this,
                       struct logic_error *__frama_c_arg_0)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception,
                  & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return;
}

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct logic_error *operator=(struct logic_error *this,
                              struct logic_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE9exception,
            & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct logic_error *operator=(struct logic_error *this,
                              struct logic_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE9exception,
            & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return this;
}

/*@ requires \valid_read(this); */
void logic_error::Dtor(struct logic_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
  return;
}

struct domain_error *operator=(struct domain_error *this,
                               struct domain_error const *__frama_c_arg_0);

struct domain_error *operator=(struct domain_error *this,
                               struct domain_error *__frama_c_arg_0);

void domain_error::Dtor(struct domain_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void domain_error::Ctor(struct domain_error const *this,
                        string const *what_arg);

/*@ requires \valid_read(this); */
void domain_error::Ctor(struct domain_error const *this, char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct domain_error *operator=(struct domain_error *this,
                               struct domain_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct domain_error *operator=(struct domain_error *this,
                               struct domain_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid_read(this); */
void domain_error::Dtor(struct domain_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
  return;
}

struct invalid_argument *operator=(struct invalid_argument *this,
                                   struct invalid_argument const *__frama_c_arg_0);

struct invalid_argument *operator=(struct invalid_argument *this,
                                   struct invalid_argument *__frama_c_arg_0);

void invalid_argument::Dtor(struct invalid_argument 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void invalid_argument::Ctor(struct invalid_argument const *this,
                            string const *what_arg);
/*@ requires \valid_read(this); */
void invalid_argument::Ctor(struct invalid_argument const *this,
                            char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct invalid_argument *operator=(struct invalid_argument *this,
                                   struct invalid_argument const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct invalid_argument *operator=(struct invalid_argument *this,
                                   struct invalid_argument *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid_read(this); */
void invalid_argument::Dtor(struct invalid_argument const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
  return;
}

struct length_error *operator=(struct length_error *this,
                               struct length_error const *__frama_c_arg_0);

struct length_error *operator=(struct length_error *this,
                               struct length_error *__frama_c_arg_0);

void length_error::Dtor(struct length_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void length_error::Ctor(struct length_error const *this,
                        string const *what_arg);

/*@ requires \valid_read(this); */
void length_error::Ctor(struct length_error const *this, char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct length_error *operator=(struct length_error *this,
                               struct length_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct length_error *operator=(struct length_error *this,
                               struct length_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid_read(this); */
void length_error::Dtor(struct length_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
  return;
}

struct out_of_range *operator=(struct out_of_range *this,
                               struct out_of_range const *__frama_c_arg_0);

struct out_of_range *operator=(struct out_of_range *this,
                               struct out_of_range *__frama_c_arg_0);

void out_of_range::Dtor(struct out_of_range 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void out_of_range::Ctor(struct out_of_range const *this,
                        string const *what_arg);

/*@ requires \valid_read(this); */
void out_of_range::Ctor(struct out_of_range const *this, char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct out_of_range *operator=(struct out_of_range *this,
                               struct out_of_range const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct out_of_range *operator=(struct out_of_range *this,
                               struct out_of_range *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE11logic_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
  return this;
}
/*@ requires \valid_read(this); */
void out_of_range::Dtor(struct out_of_range const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
  return;
}

void runtime_error::Ctor(struct runtime_error const *this,
                         struct runtime_error const *__frama_c_arg_0);

void runtime_error::Ctor(struct runtime_error const *this,
                         struct runtime_error *__frama_c_arg_0);

struct runtime_error *operator=(struct runtime_error *this,
                                struct runtime_error const *__frama_c_arg_0);

struct runtime_error *operator=(struct runtime_error *this,
                                struct runtime_error *__frama_c_arg_0);

void runtime_error::Dtor(struct runtime_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void runtime_error::Ctor(struct runtime_error const *this,
                         string const *what_arg);

/*@ requires \valid_read(this); */
void runtime_error::Ctor(struct runtime_error const *this,
                         char const *what_arg);

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid_read(__frama_c_arg_0);
 */
void runtime_error::Ctor(struct runtime_error const *this,
                         struct runtime_error const *__frama_c_arg_0)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception,
                  & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return;
}

/*@ requires \separated(this, __frama_c_arg_0);
    requires \valid_read(this);
    requires \valid(__frama_c_arg_0);
 */
void runtime_error::Ctor(struct runtime_error const *this,
                         struct runtime_error *__frama_c_arg_0)
{
  exception::Ctor(& this->_frama_c__ZN3stdE9exception,
                  & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return;
}

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct runtime_error *operator=(struct runtime_error *this,
                                struct runtime_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE9exception,
            & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct runtime_error *operator=(struct runtime_error *this,
                                struct runtime_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE9exception,
            & __frama_c_arg_0->_frama_c__ZN3stdE9exception);
  return this;
}

/*@ requires \valid_read(this); */
void runtime_error::Dtor(struct runtime_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
  return;
}

struct range_error *operator=(struct range_error *this,
                              struct range_error const *__frama_c_arg_0);

struct range_error *operator=(struct range_error *this,
                              struct range_error *__frama_c_arg_0);

void range_error::Dtor(struct range_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void range_error::Ctor(struct range_error const *this, string const *what_arg);

/*@ requires \valid_read(this); */
void range_error::Ctor(struct range_error const *this, char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct range_error *operator=(struct range_error *this,
                              struct range_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct range_error *operator=(struct range_error *this,
                              struct range_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid_read(this); */
void range_error::Dtor(struct range_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
  return;
}

struct overflow_error *operator=(struct overflow_error *this,
                                 struct overflow_error const *__frama_c_arg_0);

struct overflow_error *operator=(struct overflow_error *this,
                                 struct overflow_error *__frama_c_arg_0);

void overflow_error::Dtor(struct overflow_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void overflow_error::Ctor(struct overflow_error const *this,
                          string const *what_arg);

/*@ requires \valid_read(this); */
void overflow_error::Ctor(struct overflow_error const *this,
                          char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct overflow_error *operator=(struct overflow_error *this,
                                 struct overflow_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct overflow_error *operator=(struct overflow_error *this,
                                 struct overflow_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid_read(this); */
void overflow_error::Dtor(struct overflow_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
  return;
}

struct underflow_error *operator=(struct underflow_error *this,
                                  struct underflow_error const *__frama_c_arg_0);
struct underflow_error *operator=(struct underflow_error *this,
                                  struct underflow_error *__frama_c_arg_0);

void underflow_error::Dtor(struct underflow_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void underflow_error::Ctor(struct underflow_error const *this,
                           string const *what_arg);

/*@ requires \valid_read(this); */
void underflow_error::Ctor(struct underflow_error const *this,
                           char const *what_arg);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct underflow_error *operator=(struct underflow_error *this,
                                  struct underflow_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct underflow_error *operator=(struct underflow_error *this,
                                  struct underflow_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid_read(this); */
void underflow_error::Dtor(struct underflow_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
  return;
}

struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& logic_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct logic_error *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct logic_error *)0)->_frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct logic_error *)0)->_frama_c__ZN3stdE9exception),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "logic_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& domain_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct domain_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct domain_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct domain_error *)0)->_frama_c__ZN3stdE11logic_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "domain_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& invalid_argument::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct invalid_argument *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct invalid_argument *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct invalid_argument *)0)->_frama_c__ZN3stdE11logic_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "invalid_argument",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& length_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct length_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct length_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct length_error *)0)->_frama_c__ZN3stdE11logic_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "length_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& out_of_range::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct out_of_range *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct out_of_range *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct out_of_range *)0)->_frama_c__ZN3stdE11logic_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "out_of_range",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& runtime_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct runtime_error *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct runtime_error *)0)->_frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct runtime_error *)0)->_frama_c__ZN3stdE9exception),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "runtime_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& range_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct range_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct range_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct range_error *)0)->_frama_c__ZN3stdE13runtime_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "range_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& overflow_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct overflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct overflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct overflow_error *)0)->_frama_c__ZN3stdE13runtime_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "overflow_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& underflow_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what),
    .shift_this = (char *)(& ((struct underflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct underflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct underflow_error *)0)->_frama_c__ZN3stdE13runtime_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "underflow_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
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[6];

/*@ requires \valid_read(this); */
void error_category::Dtor(struct error_category const *this);

/*@ requires \valid_read(this); */
char const *name(struct error_category const *this);

/*@ requires \valid_read(this); */
struct error_condition default_error_condition(struct error_category const *this,
                                               int ev);

/*@ requires \valid_read(this);
    requires \valid_read(condition); */
_Bool equivalent(struct error_category const *this, int code,
                 struct error_condition const *condition);

/*@ requires \valid_read(this);
    requires \valid_read(code); */
_Bool equivalent(struct error_category const *this,
                 struct error_code const *code, int condition);

/*@ requires \valid_read(this); */
string message(struct error_category const *this, int ev);

/*@ requires \valid_read(this);
    requires \valid_read(rhs); */
_Bool operator==(struct error_category const *this,
                 struct error_category const *rhs);

/*@ requires \valid_read(this);
    requires \valid_read(rhs); */
_Bool operator!=(struct error_category const *this,
                 struct error_category const *rhs);

/*@ requires \valid_read(this);
    requires \valid_read(rhs); */
_Bool operator<(struct error_category const *this,
                struct error_category const *rhs);

/*@ ensures \valid_read(\result); */
struct error_category const *generic_category(void);

/*@ ensures \valid_read(\result); */
struct error_category const *system_category(void);

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 error_code::Ctor(struct error_code const *this);

/*@ requires \valid_read(this);
    requires \valid_read(cat); */
void error_code::Ctor(struct error_code const *this, int val,
                      struct error_category const *cat);

/*@ requires \valid(this);
    requires \valid_read(cat); */
void assign(struct error_code *this, int val,
            struct error_category const *cat);

/*@ requires \valid(this); */
void clear(struct error_code *this);

/*@ requires \valid_read(this); */
int value(struct error_code const *this);
/*@ requires \valid_read(this);
    ensures \valid_read(\result); */
struct error_category const *category(struct error_code const *this);

/*@ requires \valid_read(this); */
struct error_condition default_error_condition(struct error_code const *this);

/*@ requires \valid_read(this); */
string message(struct error_code const *this);

/*@ requires \valid_read(this); */
_Bool conversion(bool)(struct error_code const *this);

struct system_error *operator=(struct system_error *this,
                               struct system_error const *__frama_c_arg_0);

struct system_error *operator=(struct system_error *this,
                               struct system_error *__frama_c_arg_0);

void system_error::Dtor(struct system_error 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_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[2];

/*@ requires \valid_read(this);
    requires \valid_read(what_arg); */
void system_error::Ctor(struct system_error const *this,
                        struct error_code ec, string const *what_arg);

/*@ requires \valid_read(this); */
void system_error::Ctor(struct system_error const *this,
                        struct error_code ec, char const *what_arg);

/*@ requires \valid_read(this); */
void system_error::Ctor(struct system_error const *this, struct error_code ec);

/*@ requires \valid_read(this);
    requires \valid_read(what_arg);
    requires \valid_read(ecat);
 */
void system_error::Ctor(struct system_error const *this, int ev,
                        struct error_category const *ecat,
                        string const *what_arg);

/*@ requires \valid_read(this);
    requires \valid_read(ecat); */
void system_error::Ctor(struct system_error const *this, int ev,
                        struct error_category const *ecat,
                        char const *what_arg);

/*@ requires \valid_read(this);
    requires \valid_read(ecat); */
void system_error::Ctor(struct system_error const *this, int ev,
                        struct error_category const *ecat);

/*@ requires \valid_read(this);
    ensures \valid_read(\result); */
struct error_code const *code(struct system_error const *this);

/*@ requires \valid_read(this); */
char const *what(struct system_error const *this);

/*@ requires \valid(this);
    requires \valid_read(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct system_error *operator=(struct system_error *this,
                               struct system_error const *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid(this);
    requires \valid(__frama_c_arg_0);
    ensures \valid(\result);
 */
struct system_error *operator=(struct system_error *this,
                               struct system_error *__frama_c_arg_0)
{
  operator=(& this->_frama_c__ZN3stdE13runtime_error,
            & __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
  return this;
}

/*@ requires \valid_read(this); */
void system_error::Dtor(struct system_error const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
  return;
}

struct _frama_c_vmt_content _frama_c_vmt[6] =
  {{.method_ptr = (void (*)())(& error_category::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& name), .shift_this = 0},
   {.method_ptr = (void (*)())(& default_error_condition), .shift_this = 0},
   {.method_ptr = (void (*)())(& equivalent), .shift_this = 0},
   {.method_ptr = (void (*)())(& equivalent), .shift_this = 0},
   {.method_ptr = (void (*)())(& message), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "error_category",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 6,
   .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "error_code",
   .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_content _frama_c_vmt[2] =
  {{.method_ptr = (void (*)())(& system_error::Dtor), .shift_this = 0},
   {.method_ptr = (void (*)())(& what), .shift_this = 0}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct system_error *)0)->_frama_c__ZN3stdE13runtime_error),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "system_error",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 2,
   .rtti_info = & _frama_c_rtti_name_info};
/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator<(struct error_code const *lhs, struct error_code const *rhs);
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 error_condition::Ctor(struct error_condition const *this);

/*@ requires \valid_read(this);
    requires \valid_read(cat); */
void error_condition::Ctor(struct error_condition const *this, int val,
                           struct error_category const *cat);

/*@ requires \valid(this);
    requires \valid_read(cat); */
void assign(struct error_condition *this, int val,
            struct error_category const *cat);

/*@ requires \valid(this); */
void clear(struct error_condition *this);

/*@ requires \valid_read(this); */
int value(struct error_condition const *this);

/*@ requires \valid_read(this);
    ensures \valid_read(\result); */
struct error_category const *category(struct error_condition const *this);

/*@ requires \valid_read(this); */
string message(struct error_condition const *this);

/*@ requires \valid_read(this); */
_Bool conversion(bool)(struct error_condition const *this);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator<(struct error_condition const *lhs,
                struct error_condition const *rhs);

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];
/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator==(struct error_code const *lhs, struct error_code const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator==(struct error_code const *lhs,
                 struct error_condition const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator==(struct error_condition const *lhs,
                 struct error_code const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator==(struct error_condition const *lhs,
                 struct error_condition const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator!=(struct error_code const *lhs, struct error_code const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator!=(struct error_code const *lhs,
                 struct error_condition const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator!=(struct error_condition const *lhs,
                 struct error_code const *rhs);

/*@ requires \valid_read(rhs);
    requires \valid_read(lhs); */
_Bool operator!=(struct error_condition const *lhs,
                 struct error_condition const *rhs);

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "error_condition",
   .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 = "is_error_condition_enum",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = (struct _frama_c_vmt *)0};