From d5cdb0459cd17137cf8cf371e63a0a45e82439ba Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 5 Mar 2021 16:20:36 +0100
Subject: [PATCH] [stdlib] better support for <cstdbool>
---
share/libc++/cstdbool | 11 +
tests/stl/oracle/stl_bool.res.oracle | 1768 ++++++++++++++++++++++++++
tests/stl/stl_bool.cpp | 2 +
3 files changed, 1781 insertions(+)
create mode 100644 share/libc++/cstdbool
create mode 100644 tests/stl/oracle/stl_bool.res.oracle
create mode 100644 tests/stl/stl_bool.cpp
diff --git a/share/libc++/cstdbool b/share/libc++/cstdbool
new file mode 100644
index 00000000..f0ceeec1
--- /dev/null
+++ b/share/libc++/cstdbool
@@ -0,0 +1,11 @@
+// -*- C++ -*-
+#include <stdbool.h>
+#ifdef bool
+#undef bool
+#endif
+#ifdef true
+#undef true
+#endif
+#ifdef false
+#undef false
+#endif
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
new file mode 100644
index 00000000..6bb2643b
--- /dev/null
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -0,0 +1,1768 @@
+[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};
+
diff --git a/tests/stl/stl_bool.cpp b/tests/stl/stl_bool.cpp
new file mode 100644
index 00000000..dcf9bcd4
--- /dev/null
+++ b/tests/stl/stl_bool.cpp
@@ -0,0 +1,2 @@
+#include<cstdbool>
+#include<algorithm>
--
GitLab