[stdlib] better support for <cstdbool>

share/libc++/cstdbool

+// -*- C++ -*-
+#include <stdbool.h>
+#ifdef bool
+#undef bool
+#endif
+#ifdef true
+#undef true
+#endif
+#ifdef false
+#undef false
+#endif

tests/stl/oracle/stl_bool.res.oracle

+[kernel] Parsing tests/stl/stl_bool.cpp (external front-end)
+Now output intermediate result
+[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
+[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
+[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
+[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
+[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
+/* 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 _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 piecewise_construct_t;
+struct piecewise_construct_t {
+   
+};
+struct exception;
+struct bad_exception;
+struct nested_exception;
+struct exception {
+   struct _frama_c_vmt *pvmt ;
+};
+struct bad_exception {
+   struct exception _frama_c__ZN3stdE9exception ;
+};
+typedef void *exception_ptr;
+struct nested_exception {
+   struct _frama_c_vmt *pvmt ;
+};
+struct type_info;
+struct bad_cast;
+struct bad_typeid;
+struct type_info {
+   struct _frama_c_vmt *pvmt ;
+};
+struct bad_cast {
+   struct exception _frama_c__ZN3stdE9exception ;
+};
+struct bad_typeid {
+   struct exception _frama_c__ZN3stdE9exception ;
+};
+struct bad_function_call;
+struct bad_function_call {
+   struct exception _frama_c__ZN3stdE9exception ;
+};
+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};
+void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this);
+
+void piecewise_construct_t::Dtor(struct piecewise_construct_t const *this);
+
+struct _frama_c_vmt _frama_c_vmt_header;
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
+
+struct _frama_c_vmt_content _frama_c_vmt[1];
+/*@ requires \valid_read(this); */
+void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this)
+{
+  return;
+}
+
+/*@ requires \valid_read(this); */
+void piecewise_construct_t::Dtor(struct piecewise_construct_t const *this)
+{
+  return;
+}
+
+struct piecewise_construct_t piecewise_construct;
+void __fc_init_ZN3stdE19piecewise_construct(void) __attribute__((__constructor__));
+void __fc_init_ZN3stdE19piecewise_construct(void)
+{
+  struct piecewise_construct_t __fc_tmp_0;
+  piecewise_construct_t::Ctor(& __fc_tmp_0);
+  piecewise_construct = __fc_tmp_0;
+  piecewise_construct_t::Dtor((struct piecewise_construct_t const *)(& __fc_tmp_0));
+  return;
+}
+
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "piecewise_construct_t",
+   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
+   .number_of_base_classes = 0,
+   .pvmt = (struct _frama_c_vmt *)0};
+/*@
+axiomatic MemCmp {
+  logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n) 
+    reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
+  
+  axiom memcmp_zero{L1, L2}:
+    ∀ char *s1, char *s2;
+    ∀ ℤ n;
+      memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
+      (∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
+  
+  }
+ */
+/*@
+axiomatic MemChr {
+  logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom memchr_def{L}:
+    ∀ char *s;
+    ∀ ℤ c;
+    ∀ ℤ n;
+      memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
+axiomatic MemSet {
+  logic 𝔹 memset{L}(char *s, ℤ c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom memset_def{L}:
+    ∀ char *s;
+    ∀ ℤ c;
+    ∀ ℤ n;
+      memset(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
+axiomatic StrLen {
+  logic ℤ strlen{L}(char *s) 
+    reads *(s + (0 ..));
+  
+  axiom strlen_pos_or_null{L}:
+    ∀ char *s;
+    ∀ ℤ i;
+      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
+      *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+  
+  axiom strlen_neg{L}:
+    ∀ char *s;
+      (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+  
+  axiom strlen_before_null{L}:
+    ∀ char *s;
+    ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+  
+  axiom strlen_at_null{L}:
+    ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+  
+  axiom strlen_not_zero{L}:
+    ∀ char *s;
+    ∀ ℤ i;
+      0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+  
+  axiom strlen_zero{L}:
+    ∀ char *s;
+    ∀ ℤ i;
+      0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+  
+  axiom strlen_sup{L}:
+    ∀ char *s;
+    ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+  
+  axiom strlen_shift{L}:
+    ∀ char *s;
+    ∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
+  
+  axiom strlen_create{L}:
+    ∀ char *s;
+    ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+  
+  axiom strlen_create_shift{L}:
+    ∀ char *s;
+    ∀ ℤ i;
+    ∀ ℤ k;
+      0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
+      0 ≤ strlen(s + k) ≤ i - k;
+  
+  axiom memcmp_strlen_left{L}:
+    ∀ char *s1, char *s2;
+    ∀ ℤ n;
+      memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
+      strlen(s1) ≡ strlen(s2);
+  
+  axiom memcmp_strlen_right{L}:
+    ∀ char *s1, char *s2;
+    ∀ ℤ n;
+      memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
+      strlen(s1) ≡ strlen(s2);
+  
+  axiom memcmp_strlen_shift_left{L}:
+    ∀ char *s1, char *s2;
+    ∀ ℤ k, ℤ n;
+      memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
+      0 ≤ strlen(s2) ≤ k + strlen(s1);
+  
+  axiom memcmp_strlen_shift_right{L}:
+    ∀ char *s1, char *s2;
+    ∀ ℤ k, ℤ n;
+      memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
+      0 ≤ strlen(s1) ≤ k + strlen(s2);
+  
+  }
+ */
+/*@
+axiomatic StrCmp {
+  logic ℤ strcmp{L}(char *s1, char *s2) 
+    reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
+  
+  axiom strcmp_zero{L}:
+    ∀ char *s1, char *s2;
+      strcmp(s1, s2) ≡ 0 ⇔
+      strlen(s1) ≡ strlen(s2) ∧
+      (∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
+  
+  }
+ */
+/*@
+axiomatic StrNCmp {
+  logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) 
+    reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
+  
+  axiom strncmp_zero{L}:
+    ∀ char *s1, char *s2;
+    ∀ ℤ n;
+      strncmp(s1, s2, n) ≡ 0 ⇔
+      (strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
+      (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
+  
+  }
+ */
+/*@
+axiomatic StrChr {
+  logic 𝔹 strchr{L}(char *s, ℤ c) 
+    reads *(s + (0 .. strlen(s)));
+  
+  axiom strchr_def{L}:
+    ∀ char *s;
+    ∀ ℤ c;
+      strchr(s, c) ≢ (0 ≢ 0) ⇔
+      (∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
+  
+  }
+ */
+/*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
+axiomatic WcsLen {
+  logic ℤ wcslen{L}(int *s) 
+    reads *(s + (0 ..));
+  
+  axiom wcslen_pos_or_null{L}:
+    ∀ int *s;
+    ∀ ℤ i;
+      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (int)0) ∧
+      *(s + i) ≡ (int)0 ⇒ wcslen(s) ≡ i;
+  
+  axiom wcslen_neg{L}:
+    ∀ int *s;
+      (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (int)0) ⇒ wcslen(s) < 0;
+  
+  axiom wcslen_before_null{L}:
+    ∀ int *s;
+    ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (int)0;
+  
+  axiom wcslen_at_null{L}:
+    ∀ int *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (int)0;
+  
+  axiom wcslen_not_zero{L}:
+    ∀ int *s;
+    ∀ int i;
+      0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (int)0 ⇒ i < wcslen(s);
+  
+  axiom wcslen_zero{L}:
+    ∀ int *s;
+    ∀ int i;
+      0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (int)0 ⇒ i ≡ wcslen(s);
+  
+  axiom wcslen_sup{L}:
+    ∀ int *s;
+    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+  
+  axiom wcslen_shift{L}:
+    ∀ int *s;
+    ∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
+  
+  axiom wcslen_create{L}:
+    ∀ int *s;
+    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+  
+  axiom wcslen_create_shift{L}:
+    ∀ int *s;
+    ∀ int i;
+    ∀ int k;
+      0 ≤ k ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
+  
+  }
+ */
+/*@
+axiomatic WcsCmp {
+  logic ℤ wcscmp{L}(int *s1, int *s2) 
+    reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
+  
+  axiom wcscmp_zero{L}:
+    ∀ int *s1, int *s2;
+      wcscmp(s1, s2) ≡ 0 ⇔
+      wcslen(s1) ≡ wcslen(s2) ∧
+      (∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
+  
+  }
+ */
+/*@
+axiomatic WcsNCmp {
+  logic ℤ wcsncmp{L}(int *s1, int *s2, ℤ n) 
+    reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
+  
+  axiom wcsncmp_zero{L}:
+    ∀ int *s1, int *s2;
+    ∀ ℤ n;
+      wcsncmp(s1, s2, n) ≡ 0 ⇔
+      (wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
+      (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
+  
+  }
+ */
+/*@
+axiomatic WcsChr {
+  logic 𝔹 wcschr{L}(int *wcs, ℤ wc) 
+    reads *(wcs + (0 .. wcslen(wcs)));
+  
+  axiom wcschr_def{L}:
+    ∀ int *wcs;
+    ∀ ℤ wc;
+      wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+      (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (int)((int)wc));
+  
+  }
+ */
+/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
+ */
+/*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
+ */
+/*@
+predicate valid_string{L}(char *s) =
+  0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
+ */
+/*@
+predicate valid_read_string{L}(char *s) =
+  0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
+ */
+/*@
+predicate valid_read_nstring{L}(char *s, ℤ n) =
+  (\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
+  valid_read_string(s);
+ */
+/*@
+predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
+ */
+/*@
+predicate valid_wstring{L}(int *s) =
+  0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
+ */
+/*@
+predicate valid_read_wstring{L}(int *s) =
+  0 ≤ wcslen(s) ∧ \valid_read(s + (0 .. wcslen(s)));
+ */
+/*@
+predicate valid_read_nwstring{L}(int *s, ℤ n) =
+  (\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
+  valid_read_wstring(s);
+ */
+/*@
+predicate valid_wstring_or_null{L}(int *s) =
+  s ≡ \null ∨ valid_wstring(s);
+ */
+/*@ ghost int __fc_heap_status; */
+/*@
+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;
+    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};
+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 type_info::Dtor(struct type_info const *this);
+
+/*@ requires \valid_read(this); */
+void type_info::Ctor(struct type_info const *this,
+                     char const *__frama_c_arg_0);
+
+/*@ requires \valid_read(this);
+    requires \valid_read(rhs); */
+_Bool operator==(struct type_info const *this, struct type_info const *rhs);
+
+/*@ requires \valid_read(this);
+    requires \valid_read(rhs); */
+_Bool operator!=(struct type_info const *this, struct type_info const *rhs);
+
+/*@ requires \valid_read(this);
+    requires \valid_read(rhs); */
+_Bool before(struct type_info const *this, struct type_info const *rhs);
+
+/*@ requires \valid_read(this); */
+size_t hash_code(struct type_info const *this);
+
+/*@ requires \valid_read(this); */
+char const *name(struct type_info const *this);
+
+void bad_cast::Dtor(struct bad_cast 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_cast::Ctor(struct bad_cast const *this);
+
+/*@ requires \separated(this, __frama_c_arg_0);
+    requires \valid_read(this);
+    requires \valid_read(__frama_c_arg_0);
+ */
+void bad_cast::Ctor(struct bad_cast const *this,
+                    struct bad_cast const *__frama_c_arg_0);
+
+/*@ requires \valid(this);
+    requires \valid_read(__frama_c_arg_0);
+    ensures \valid(\result);
+ */
+struct bad_cast *operator=(struct bad_cast *this,
+                           struct bad_cast const *__frama_c_arg_0);
+
+/*@ requires \valid_read(this); */
+char const *what(struct bad_cast const *this);
+
+/*@ requires \valid_read(this); */
+void bad_cast::Dtor(struct bad_cast const *this)
+{
+  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
+  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
+  return;
+}
+
+void bad_typeid::Dtor(struct bad_typeid 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_typeid::Ctor(struct bad_typeid const *this);
+
+/*@ requires \separated(this, __frama_c_arg_0);
+    requires \valid_read(this);
+    requires \valid_read(__frama_c_arg_0);
+ */
+void bad_typeid::Ctor(struct bad_typeid const *this,
+                      struct bad_typeid const *__frama_c_arg_0);
+
+/*@ requires \valid(this);
+    requires \valid_read(__frama_c_arg_0);
+    ensures \valid(\result);
+ */
+struct bad_typeid *operator=(struct bad_typeid *this,
+                             struct bad_typeid const *__frama_c_arg_0);
+
+/*@ requires \valid_read(this); */
+char const *what(struct bad_typeid const *this);
+
+/*@ requires \valid_read(this); */
+void bad_typeid::Dtor(struct bad_typeid const *this)
+{
+  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
+  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
+  return;
+}
+
+struct _frama_c_vmt_content _frama_c_vmt[1] =
+  {{.method_ptr = (void (*)())(& type_info::Dtor), .shift_this = 0}};
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "type_info",
+   .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};
+struct _frama_c_vmt_content _frama_c_vmt[2] =
+  {{.method_ptr = (void (*)())(& bad_cast::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_cast *)0)->_frama_c__ZN3stdE9exception),
+    .shift_vmt = 0}};
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "bad_cast",
+   .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 (*)())(& bad_typeid::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_typeid *)0)->_frama_c__ZN3stdE9exception),
+    .shift_vmt = 0}};
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "bad_typeid",
+   .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};
+void bad_function_call::Dtor(struct bad_function_call 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_function_call::Ctor(struct bad_function_call const *this)
+{
+  exception::Ctor(& this->_frama_c__ZN3stdE9exception);
+  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
+  return;
+}
+
+/*@ requires \valid_read(this); */
+void bad_function_call::Dtor(struct bad_function_call const *this)
+{
+  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
+  exception::Dtor(& this->_frama_c__ZN3stdE9exception);
+  return;
+}
+
+struct _frama_c_vmt_content _frama_c_vmt[2] =
+  {{.method_ptr = (void (*)())(& bad_function_call::Dtor), .shift_this = 0},
+   {.method_ptr = (void (*)())(& what),
+    .shift_this = (char *)(& ((struct bad_function_call *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct bad_function_call *)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_function_call *)0)->_frama_c__ZN3stdE9exception),
+    .shift_vmt = 0}};
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "bad_function_call",
+   .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[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_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_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_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 = "input_iterator_tag",
+   .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 = "output_iterator_tag",
+   .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 = "forward_iterator_tag",
+   .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 = "bidirectional_iterator_tag",
+   .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 = "random_access_iterator_tag",
+   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
+   .number_of_base_classes = 0,
+   .pvmt = (struct _frama_c_vmt *)0};
+struct _frama_c_vmt _frama_c_vmt_header;
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
+
+struct _frama_c_vmt_content _frama_c_vmt[1];
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "iterator",
+   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
+   .number_of_base_classes = 0,
+   .pvmt = (struct _frama_c_vmt *)0};
+

tests/stl/stl_bool.cpp

+#include<cstdbool>
+#include<algorithm>