Forked from
pub / Frama Clang
687 commits behind the upstream repository.
stl_system_error.res.oracle 135.17 KiB
[kernel] Parsing tests/stl/stl_system_error.cpp (external front-end)
Now output intermediate result
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function tm::Ctor can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function operator= can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function operator= can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
[kernel] Warning: Assuming declared function exception::Ctor can't throw any exception
[kernel] Warning: Assuming declared function operator= can't throw any exception
[kernel] Warning: Assuming declared function exception::Dtor can't throw any exception
/* Generated by Frama-C */
struct _frama_c_vmt_content {
void (*method_ptr)() ;
int shift_this ;
};
struct _frama_c_rtti_name_info_node;
struct _frama_c_vmt {
struct _frama_c_vmt_content *table ;
int table_size ;
struct _frama_c_rtti_name_info_node *rtti_info ;
};
struct _frama_c_rtti_name_info_content {
struct _frama_c_rtti_name_info_node *value ;
int shift_object ;
int shift_vmt ;
};
struct _frama_c_rtti_name_info_node {
char const *name ;
struct _frama_c_rtti_name_info_content *base_classes ;
int number_of_base_classes ;
struct _frama_c_vmt *pvmt ;
};
typedef unsigned int size_t;
typedef size_t size_t;
typedef void *nullptr_t;
typedef _Bool value_type;
struct integral_constant<bool,0>;
struct integral_constant<bool,0> {
};
typedef _Bool value_type;
struct integral_constant<bool,1>;
struct integral_constant<bool,1> {
};
struct exception;
struct bad_exception;
struct nested_exception;
struct exception {
struct _frama_c_vmt *pvmt ;
};
struct bad_exception {
struct exception _frama_c__ZN3stdE9exception ;
};
typedef void *exception_ptr;
struct nested_exception {
struct _frama_c_vmt *pvmt ;
};
typedef unsigned int uid_t;
typedef long time_t;
struct __fc_FILE {
unsigned int __fc_FILE_id ;
unsigned int __fc_FILE_data ;
};
typedef struct __fc_FILE FILE;
typedef int clockid_t;typedef int pid_t;
typedef unsigned long sigset_t;
union sigval {
int sival_int ;
void *sival_ptr ;
};
struct __fc_siginfo_t {
int si_signo ;
int si_code ;
union sigval si_value ;
int si_errno ;
pid_t si_pid ;
uid_t si_uid ;
void *si_addr ;
int si_status ;
int si_band ;
};
typedef struct __fc_siginfo_t siginfo_t;
struct sigaction {
void (*sa_handler)(int ) ;
void (*sa_sigaction)(int , siginfo_t *, void *) ;
sigset_t sa_mask ;
int sa_flags ;
};
typedef unsigned int clock_t;
struct tm;
struct tm {
int tm_sec ;
int tm_min ;
int tm_hour ;
int tm_mday ;
int tm_mon ;
int tm_year ;
int tm_wday ;
int tm_yday ;
int tm_isdst ;
};
struct timespec {
long tv_sec ;
long tv_nsec ;
};
typedef char char_type;
typedef int char_type;
struct __shared_ref_base;
struct piecewise_construct_t;
struct piecewise_construct_t {
};
struct __shared_ref_base {
struct _frama_c_vmt *pvmt ;
};
struct __shared_ref<void> {
struct __shared_ref_base _frama_c__ZN3stdE17__shared_ref_base ;
void *__ptr ;
long _n ;
long _w ;
};
struct bad_weak_ptr;
struct shared_ptr<void>;
struct bad_weak_ptr {
struct exception _frama_c__ZN3stdE9exception ;
};
struct shared_ptr<void> {
void *__ptr ;
struct __shared_ref_base *_ref ;
};
struct basic_string<char,std::char_traits<char>,std::allocator<char>>;
typedef struct basic_string<char,std::char_traits<char>,std::allocator<char>> string;
struct logic_error;
struct domain_error;struct invalid_argument;
struct length_error;
struct out_of_range;
struct runtime_error;
struct range_error;
struct overflow_error;
struct underflow_error;
struct logic_error {
struct exception _frama_c__ZN3stdE9exception ;
};
struct domain_error {
struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct invalid_argument {
struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct length_error {
struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct out_of_range {
struct logic_error _frama_c__ZN3stdE11logic_error ;
};
struct runtime_error {
struct exception _frama_c__ZN3stdE9exception ;
};
struct range_error {
struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct overflow_error {
struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct underflow_error {
struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct error_condition;
struct error_code;
struct error_category;
struct system_error;
struct error_category {
struct _frama_c_vmt *pvmt ;
};
struct error_code {
int val_ ;
struct error_category const *cat_ ;
};
struct system_error {
struct runtime_error _frama_c__ZN3stdE13runtime_error ;
};
struct error_condition {
int val_ ;
struct error_category const *cat_ ;
};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
_Bool const value;
/*@ requires \valid_read(this); */
value_type value_type)(struct integral_constant<bool,0> const *this);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "integral_constant",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
_Bool const value;/*@ requires \valid_read(this); */
value_type value_type)(struct integral_constant<bool,1> const *this);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "integral_constant",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "__boolean",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "__boolean",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "_is_void",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "ok_type",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "ko_type",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
/*@
axiomatic MemCmp {
logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n)
reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
axiom memcmp_zero{L1, L2}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
}
*/
/*@axiomatic MemChr {
logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
axiom memchr_def{L}:
∀ char *s;
∀ ℤ c;
∀ ℤ n;
memchr(s, c, n) ≢ (0 ≢ 0) ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
*/
/*@
axiomatic MemSet {
logic 𝔹 memset{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
axiom memset_def{L}:
∀ char *s;
∀ ℤ c;
∀ ℤ n;
memset(s, c, n) ≢ (0 ≢ 0) ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
*/
/*@
axiomatic StrLen {
logic ℤ strlen{L}(char *s)
reads *(s + (0 ..));
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
*(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
(∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
axiom strlen_at_null{L}:
∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
axiom strlen_create{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
strlen(s1) ≡ strlen(s2);
axiom memcmp_strlen_right{L}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
strlen(s1) ≡ strlen(s2);
axiom memcmp_strlen_shift_left{L}:
∀ char *s1, char *s2;
∀ ℤ k, ℤ n;
memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
0 ≤ strlen(s2) ≤ k + strlen(s1);
axiom memcmp_strlen_shift_right{L}:
∀ char *s1, char *s2;
∀ ℤ k, ℤ n;
memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
0 ≤ strlen(s1) ≤ k + strlen(s2);
}
*/
/*@
axiomatic StrCmp {
logic ℤ strcmp{L}(char *s1, char *s2)
reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
axiom strcmp_zero{L}:
∀ char *s1, char *s2;
strcmp(s1, s2) ≡ 0 ⇔
strlen(s1) ≡ strlen(s2) ∧
(∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic StrNCmp {
logic ℤ strncmp{L}(char *s1, char *s2, ℤ n)
reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
axiom strncmp_zero{L}:
∀ char *s1, char *s2;
∀ ℤ n;
strncmp(s1, s2, n) ≡ 0 ⇔
(strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
(∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic StrChr {
logic 𝔹 strchr{L}(char *s, ℤ c)
reads *(s + (0 .. strlen(s)));
axiom strchr_def{L}: ∀ char *s;
∀ ℤ c;
strchr(s, c) ≢ (0 ≢ 0) ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
*/
/*@
axiomatic WMemChr {
logic 𝔹 wmemchr{L}(int *s, int c, ℤ n)
reads *(s + (0 .. n - 1));
logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
reads *(s + (0 .. n - 1));
axiom wmemchr_def{L}:
∀ int *s;
∀ int c;
∀ ℤ n;
wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
*/
/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
axiom wcslen_pos_or_null{L}:
∀ int *s;
∀ ℤ i;
0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (int)0) ∧
*(s + i) ≡ (int)0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
∀ int *s;
(∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (int)0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ int *s;
∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (int)0;
axiom wcslen_at_null{L}:
∀ int *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (int)0;
axiom wcslen_not_zero{L}:
∀ int *s;
∀ int i;
0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (int)0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ int *s;
∀ int i;
0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (int)0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ int *s;
∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ int *s;
∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
axiom wcslen_create{L}:
∀ int *s;
∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ int *s; ∀ int i;
∀ int k;
0 ≤ k ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
/*@
axiomatic WcsCmp {
logic ℤ wcscmp{L}(int *s1, int *s2)
reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
axiom wcscmp_zero{L}:
∀ int *s1, int *s2;
wcscmp(s1, s2) ≡ 0 ⇔
wcslen(s1) ≡ wcslen(s2) ∧
(∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic WcsNCmp {
logic ℤ wcsncmp{L}(int *s1, int *s2, ℤ n)
reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
axiom wcsncmp_zero{L}:
∀ int *s1, int *s2;
∀ ℤ n;
wcsncmp(s1, s2, n) ≡ 0 ⇔
(wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
(∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic WcsChr {
logic 𝔹 wcschr{L}(int *wcs, ℤ wc)
reads *(wcs + (0 .. wcslen(wcs)));
axiom wcschr_def{L}:
∀ int *wcs;
∀ ℤ wc;
wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
(∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (int)((int)wc));
}
*/
/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
*/
/*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
*/
/*@
predicate valid_string{L}(char *s) =
0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
*/
/*@
predicate valid_read_string{L}(char *s) =
0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
*/
/*@
predicate valid_read_nstring{L}(char *s, ℤ n) =
(\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
valid_read_string(s);
*/
/*@
predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
*/
/*@
predicate valid_wstring{L}(int *s) =
0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
*//*@
predicate valid_read_wstring{L}(int *s) =
0 ≤ wcslen(s) ∧ \valid_read(s + (0 .. wcslen(s)));
*/
/*@
predicate valid_read_nwstring{L}(int *s, ℤ n) =
(\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
valid_read_wstring(s);
*/
/*@
predicate valid_wstring_or_null{L}(int *s) =
s ≡ \null ∨ valid_wstring(s);
*/
/*@ ghost int __fc_heap_status; */
/*@
axiomatic dynamic_allocation {
predicate is_allocable{L}(ℤ n)
reads __fc_heap_status;
axiom never_allocable{L}:
∀ ℤ i; i < 0 ∨ i > 4294967295U ⇒ ¬is_allocable(i);
}
*/
/*@
predicate non_escaping{L}(void *s, ℤ n) =
∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
\block_length((char *)s) ≡ 0 ∧ \offset((char *)s) ≡ 0;
*/
/*@
predicate valid_or_empty{L}(void *s, size_t n) =
(empty_block(s) ∨ \valid_read((char *)s)) ∧
\valid((char *)s + (0 .. n - 1));
*/
/*@
predicate valid_read_or_empty{L}(void *s, size_t n) =
(empty_block(s) ∨ \valid_read((char *)s)) ∧
\valid_read((char *)s + (1 .. n - 1));
*/
/*@ requires valid_s1: valid_read_or_empty(s1, n);
requires valid_s2: valid_read_or_empty(s2, n);
requires s1: initialization: \initialized((char *)s1 + (0 .. n - 1));
requires s2: initialization: \initialized((char *)s2 + (0 .. n - 1));
requires s1: danglingness: non_escaping(s1, n);
requires s2: danglingness: non_escaping(s2, n);
ensures
logic_spec:
\result ≡
memcmp{Pre, Pre}((char *)\old(s1), (char *)\old(s2), \old(n));
assigns \result;
assigns \result
\from (indirect: *((char *)s1 + (0 .. n - 1))),
(indirect: *((char *)s2 + (0 .. n - 1)));
*/
int memcmp(void const *s1, void const *s2, size_t n);
/*@ requires
valid:
valid_read_or_empty(s, n) ∨
\valid_read((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
requires
initialization:
\initialized((unsigned char *)s + (0 .. n - 1)) ∨
\initialized((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
requires
danglingness:
non_escaping(s, n) ∨ non_escaping(s, (size_t)((int)(memchr_off((char *)s, c, n) + 1)));
assigns \result;
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
result_in_str:
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
separation:
\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_ptr: \result ≡ \old(dest);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest;
*/
void *memcpy(void * __restrict dest, void const * __restrict src, size_t n);
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
ensures
copied_contents:
memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
0;
ensures result_ptr: \result ≡ \old(dest);
assigns *((char *)dest + (0 .. n - 1)), \result;
assigns *((char *)dest + (0 .. n - 1))
\from *((char *)src + (0 .. n - 1));
assigns \result \from dest;
*/
void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
assigns \result \from s;
*/
void *memset(void *s, int c, size_t n);
/*@ requires valid_string_s: valid_read_string(s);
ensures acsl_c_equiv: \result ≡ strlen(\old(s));
assigns \result;
assigns \result \from (indirect: *(s + (0 ..)));
*/
size_t strlen(char const *s);
/*@ requires valid_string_s: valid_read_nstring(s, n); ensures
result_bounded: \result ≡ strlen(\old(s)) ∨ \result ≡ \old(n);
assigns \result;
assigns \result \from (indirect: *(s + (0 .. n - 1))), (indirect: n);
*/
size_t strnlen(char const *s, size_t n);
/*@ requires valid_string_s1: valid_read_string(s1);
requires valid_string_s2: valid_read_string(s2);
ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2));
assigns \result;
assigns \result
\from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
int strcmp(char const *s1, char const *s2);
/*@ requires valid_string_s1: valid_read_nstring(s1, n);
requires valid_string_s2: valid_read_nstring(s2, n);
ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n));
assigns \result;
assigns \result
\from (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
int strncmp(char const *s1, char const *s2, size_t n);
/*@ requires valid_string_s1: valid_read_string(s1);
requires valid_string_s2: valid_read_string(s2);
assigns \result;
assigns \result
\from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
result_in_length: \old(s) ≤ \result ≤ \old(s) + strlen(\old(s));
ensures result_valid_string: valid_read_string(\result);
ensures
result_first_occur:
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
ensures result_null: \result ≡ \null;
behavior default:
ensures
result_null_or_same_base:
\result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
*/
char *strchr(char const *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
ensures
result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
assigns \result;
assigns \result
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
*/
char *strchrnul(char const *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
ensures result_null: \result ≡ \null;
behavior default:
ensures
result_null_or_same_base:
\result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
*/
char *strrchr(char const *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_reject: valid_read_string(reject);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result;
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(reject + (0 ..)));
*/
size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
*/
size_t strspn(char const *s, char const *accept);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures
result_null_or_same_base:
\result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
assigns \result;
assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
*/
char *strpbrk(char const *s, char const *accept);
/*@ requires valid_string_haystack: valid_read_string(haystack);
requires valid_string_needle: valid_read_string(needle);
ensures
result_null_or_in_haystack:
\result ≡ \null ∨
(\subset(\result, \old(haystack) + (0 ..)) ∧
\valid_read(\result) ∧
memcmp{Pre, Pre}(\result, \old(needle), strlen(\old(needle))) ≡ 0);
assigns \result;
assigns \result
\from haystack, (indirect: *(haystack + (0 ..))),
(indirect: *(needle + (0 ..)));
*/
char *strstr(char const *haystack, char const *needle);
/*@ requires valid_string_haystack: valid_read_string(haystack);
requires valid_string_needle: valid_read_string(needle);
ensures
result_null_or_in_haystack:
\result ≡ \null ∨ (\subset(\result, \old(haystack) + (0 ..)) ∧ \valid_read(\result));
assigns \result;
assigns \result
\from haystack, (indirect: *(haystack + (0 ..))),
(indirect: *(needle + (0 ..)));
*/
char *strcasestr(char const *haystack, char const *needle);
char *__fc_strtok_ptr;
/*@ requires valid_string_delim: valid_read_string(delim);
assigns *(s + (0 ..)), *(__fc_strtok_ptr + (0 ..)), \result,
__fc_strtok_ptr;
assigns *(s + (0 ..))
\from *(s + (0 ..)), (indirect: s), (indirect: __fc_strtok_ptr),
(indirect: *(delim + (0 ..)));
assigns *(__fc_strtok_ptr + (0 ..))
\from *(__fc_strtok_ptr + (0 ..)), (indirect: s),
(indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..)));
assigns \result
\from s, __fc_strtok_ptr, (indirect: *(s + (0 ..))),
(indirect: *(__fc_strtok_ptr + (0 ..))),
(indirect: *(delim + (0 ..)));
assigns __fc_strtok_ptr
\from \old(__fc_strtok_ptr), s,
(indirect: *(__fc_strtok_ptr + (0 ..))),
(indirect: *(delim + (0 ..)));
behavior new_str:
assumes s_not_null: s ≢ \null;
requires
valid_string_s_or_delim_not_found:
valid_string(s) ∨
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
ensures ptr_subset: \subset(__fc_strtok_ptr, \old(s) + (0 ..));
assigns __fc_strtok_ptr, *(s + (0 ..)), \result;
assigns __fc_strtok_ptr
\from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
assigns *(s + (0 ..))
\from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
assigns \result
\from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
behavior resume_str:
assumes s_null: s ≡ \null;
requires not_first_call: __fc_strtok_ptr ≢ \null;
ensures
result_subset:
\result ≡ \null ∨
\subset(\result, \old(__fc_strtok_ptr) + (0 ..));
ensures
ptr_subset: \subset(__fc_strtok_ptr, \old(__fc_strtok_ptr) + (0 ..));
assigns *(__fc_strtok_ptr + (0 ..)), __fc_strtok_ptr, \result;
assigns *(__fc_strtok_ptr + (0 ..))
\from *(__fc_strtok_ptr + (0 ..)), (indirect: __fc_strtok_ptr),
(indirect: *(delim + (0 ..)));
assigns __fc_strtok_ptr
\from \old(__fc_strtok_ptr), (indirect: *(__fc_strtok_ptr + (0 ..))),
(indirect: *(delim + (0 ..)));
assigns \result
\from __fc_strtok_ptr, (indirect: *(__fc_strtok_ptr + (0 ..))),
(indirect: *(delim + (0 ..)));
complete behaviors resume_str, new_str;
disjoint behaviors resume_str, new_str; */
char *strtok(char * __restrict s, char const * __restrict delim);
/*@ requires valid_string_delim: valid_read_string(delim);
requires valid_saveptr: \valid(saveptr);
assigns *(s + (0 ..)), *(*saveptr + (0 ..)), \result, *saveptr;
assigns *(s + (0 ..))
\from *(s + (0 ..)), (indirect: s), (indirect: *saveptr),
(indirect: *(delim + (0 ..)));
assigns *(*saveptr + (0 ..))
\from *(*saveptr + (0 ..)), (indirect: s), (indirect: *saveptr),
(indirect: *(delim + (0 ..)));
assigns \result
\from s, *saveptr, (indirect: *(s + (0 ..))),
(indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..)));
assigns *saveptr
\from \old(*saveptr), s, (indirect: *(*saveptr + (0 ..))),
(indirect: *(delim + (0 ..)));
behavior new_str:
assumes s_not_null: s ≢ \null;
requires
valid_string_s_or_delim_not_found:
valid_string(s) ∨
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
ensures initialization: \initialized(\old(saveptr));
ensures saveptr_subset: \subset(*\old(saveptr), \old(s) + (0 ..));
assigns *saveptr, *(s + (0 ..)), \result;
assigns *saveptr
\from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
assigns *(s + (0 ..))
\from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
assigns \result
\from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
behavior resume_str:
assumes s_null: s ≡ \null;
requires not_first_call: *saveptr ≢ \null;
requires saveptr: initialization: \initialized(saveptr);
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
ensures
saveptr_subset: \subset(*\old(saveptr), \old(*saveptr) + (0 ..));
assigns *(*saveptr + (0 ..)), *saveptr, \result;
assigns *(*saveptr + (0 ..))
\from *(*saveptr + (0 ..)), (indirect: *saveptr),
(indirect: *(delim + (0 ..)));
assigns *saveptr
\from \old(*saveptr), (indirect: *(*saveptr + (0 ..))),
(indirect: *(delim + (0 ..)));
assigns \result
\from *saveptr, (indirect: *(*saveptr + (0 ..))),
(indirect: *(delim + (0 ..)));
complete behaviors resume_str, new_str;
disjoint behaviors resume_str, new_str;
*/
char *strtok_r(char * __restrict s, char const * __restrict delim,
char ** __restrict saveptr);
/*@ requires
valid_string_stringp: \valid(stringp) ∧ valid_string(*stringp);
requires valid_string_delim: valid_read_string(delim); assigns *stringp, \result;
assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
assigns \result \from *(delim + (..)), *(*(stringp + (..)));
*/
char *strsep(char **stringp, char const *delim);
char __fc_strerror[64];
char * const __fc_p_strerror = __fc_strerror;
/*@ ensures result_internal_str: \result ≡ __fc_p_strerror;
ensures result_nul_terminated: *(\result + 63) ≡ 0;
ensures result_valid_string: valid_read_string(\result);
assigns \result;
assigns \result \from __fc_p_strerror, (indirect: errnum);
*/
char *strerror(int errnum);
/*@ requires valid_string_src: valid_read_string(src);
requires room_string: \valid(dest + (0 .. strlen(src)));
requires
separation:
\separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 .. strlen{Old}(src))), \result;
assigns *(dest + (0 .. strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
assigns \result \from dest;
behavior complete:
assumes src_fits: strlen(src) < n;
ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
behavior partial:
assumes src_too_long: n ≤ strlen(src);
ensures
equal_prefix:
memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
*/
char *strncpy(char * __restrict dest, char const * __restrict src, size_t n);
/*@ requires valid_string_src: valid_read_string(src);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires
separation:
\separated(
dest + (0 .. n - 1), src + (0 .. \max(n - 1, strlen(src)))
);
ensures
initialization:
\initialized(\old(dest) + (0 .. \min(strlen(\old(src)), \old(n) - 1)));
ensures bounded_result: \result ≡ strlen(\old(src));
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
assigns \result
\from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n);
*/
size_t strlcpy(char * __restrict dest, char const * __restrict src, size_t n);
/*@ requires valid_string_src: valid_read_string(src); requires room_string: \valid(dest + (0 .. strlen(src)));
requires
separation:
\separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
ensures points_to_end: \result ≡ \old(dest) + strlen(\old(dest));
assigns *(dest + (0 .. strlen{Old}(src))), \result;
assigns *(dest + (0 .. strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
*/
char *stpcpy(char * __restrict dest, char const * __restrict src);
/*@ requires valid_string_src: valid_read_string(src);
requires valid_string_dest: valid_string(dest);
requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
ensures
sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
ensures
dest: initialization:
\initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
ensures
dest_null_terminated:
*(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest +
(strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
\result;
assigns
*(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
*/
char *strcat(char * __restrict dest, char const * __restrict src);
/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires valid_string_dest: valid_string(dest);
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
\from *(src + (0 .. n));
assigns \result \from dest;
behavior complete:
assumes
valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
requires
room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
ensures
sum_of_lengths:
strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
assigns *(dest +
(strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
\result;
assigns
*(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
\from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
behavior partial:
assumes
valid_string_src_too_large:
¬(valid_read_string(src) ∧ strlen(src) ≤ n);
requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
ensures
sum_of_bounded_lengths:
strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
\result;
assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) \from *(src + (0 .. strlen{Old}(src)));
assigns \result \from dest;
*/
char *strncat(char * __restrict dest, char const * __restrict src, size_t n);
/*@ requires valid_string_src: valid_read_string(src);
requires valid_string_dest: valid_string(dest);
requires room_nstring: \valid(dest + (0 .. n - 1));
ensures
bounded_result: \result ≡ strlen(\old(dest)) + strlen(\old(src));
assigns *(dest + (strlen{Old}(dest) .. n)), \result;
assigns *(dest + (strlen{Old}(dest) .. n))
\from (indirect: n), *(src + (0 .. strlen{Old}(src)));
assigns \result
\from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n);
*/
size_t strlcat(char * __restrict dest, char const * __restrict src, size_t n);
/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
requires valid_string_src: valid_read_string(src);
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from (indirect: *(src + (0 ..))), (indirect: n);
assigns \result \from dest;
*/
size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))),
(indirect: __fc_heap_status);
allocates \result;
behavior allocation:
assumes can_allocate: is_allocable(strlen(s));
ensures allocation: \fresh{Old, Here}(\result,strlen(\old(s)));
ensures
result_valid_string_and_same_contents:
valid_string(\result) ∧ strcmp(\result, \old(s)) ≡ 0;
assigns __fc_heap_status, \result;
assigns __fc_heap_status \from (indirect: s), __fc_heap_status;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))),
(indirect: __fc_heap_status);
behavior no_allocation:
assumes cannot_allocate: ¬is_allocable(strlen(s));
ensures result_null: \result ≡ \null;
assigns \result;
assigns \result \from \nothing;
allocates \nothing;
*/
char *strdup(char const *s);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
allocates \result;
behavior allocation:
assumes can_allocate: is_allocable(\min(strlen(s), n + 1));
ensures
allocation:
\fresh{Old, Here}(\result,\min(strlen(\old(s)), \old(n) + 1));
ensures
result_valid_string_bounded_and_same_prefix:
\valid(\result + (0 .. \min(strlen(\old(s)), \old(n)))) ∧ valid_string(\result) ∧ strlen(\result) ≤ \old(n) ∧
strncmp(\result, \old(s), \old(n)) ≡ 0;
assigns __fc_heap_status, \result;
assigns __fc_heap_status
\from (indirect: s), (indirect: n), __fc_heap_status;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
behavior no_allocation:
assumes cannot_allocate: ¬is_allocable(\min(strlen(s), n + 1));
ensures result_null: \result ≡ \null;
assigns \result;
assigns \result \from \nothing;
allocates \nothing;
*/
char *strndup(char const *s, size_t n);
char __fc_strsignal[64];
char * const __fc_p_strsignal = __fc_strsignal;
/*@ ensures result_internal_str: \result ≡ __fc_p_strsignal;
ensures result_nul_terminated: *(\result + 63) ≡ 0;
ensures result_valid_string: valid_read_string(\result);
assigns \result;
assigns \result \from __fc_p_strsignal, (indirect: signum);
*/
char *strsignal(int signum);
/*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
ensures
initialization: s_initialized:
\initialized((char *)\old(s) + (0 .. \old(n) - 1));
ensures
zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
assigns *((char *)s + (0 .. n - 1));
assigns *((char *)s + (0 .. n - 1)) \from \nothing;
*/
void bzero(void *s, size_t n);
/*@ requires valid_string_s1: valid_read_string(s1);
requires valid_string_s2: valid_read_string(s2);
assigns \result;
assigns \result
\from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
int strcasecmp(char const *s1, char const *s2);
/*@ requires valid_string_s1: valid_read_nstring(s1, n);
requires valid_string_s2: valid_read_nstring(s2, n);
assigns \result;
assigns \result
\from (indirect: n), (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1)));
*/
int strncasecmp(char const *s1, char const *s2, size_t n);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this); */
void exception::Ctor(struct exception const *this);
/*@ requires \separated(this, exn);
requires \valid_read(this);
requires \valid_read(exn);
*/
void exception::Ctor(struct exception const *this, struct exception const *exn);
/*@ requires \valid(this);
requires \valid_read(exn);
ensures \valid(\result);
*/
struct exception *operator=(struct exception *this,
struct exception const *exn);
/*@ requires \valid_read(this); */
void exception::Dtor(struct exception const *this);
/*@ requires \valid_read(this); */
char const *what(struct exception const *this);
void bad_exception::Dtor(struct bad_exception const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this); */
void bad_exception::Ctor(struct bad_exception const *this);
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void bad_exception::Ctor(struct bad_exception const *this,
struct bad_exception const *__frama_c_arg_0);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct bad_exception *operator=(struct bad_exception *this,
struct bad_exception const *__frama_c_arg_0);
/*@ requires \valid_read(this); */
char const *what(struct bad_exception const *this);
/*@ requires \valid_read(this); */
void bad_exception::Dtor(struct bad_exception const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
exception::Dtor(& this->_frama_c__ZN3stdE9exception);
return;
}
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void nested_exception::Ctor(struct nested_exception const *this);
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void nested_exception::Ctor(struct nested_exception const *this,
struct nested_exception const *__frama_c_arg_0);
/*@ requires \valid(this); requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct nested_exception *operator=(struct nested_exception *this,
struct nested_exception const *__frama_c_arg_0);
/*@ requires \valid_read(this); */
void nested_exception::Dtor(struct nested_exception const *this);
/*@ requires \valid_read(this); */
void rethrow_nested(struct nested_exception const *this);
/*@ requires \valid_read(this); */
exception_ptr nested_ptr(struct nested_exception const *this);
int _frama_c_find_dynamic_cast_aux(struct _frama_c_rtti_name_info_node *target_info,
struct _frama_c_rtti_name_info_content *concrete_base,
int number_of_bases,
int found_shift_object,
int found_shift_vmt, int last_shift_vmt,
int *shift_object, int *distance)
{
int result = 0;
struct _frama_c_rtti_name_info_content *cursor = concrete_base;
int is_over = 0;
int base_index = 0;
while (base_index < number_of_bases) {
if (cursor->value == target_info) {
if (*distance < 0) goto _LOR;
else
if (*distance >= 1) {
_LOR:
{
if (found_shift_vmt == cursor->shift_vmt) *distance = 0;
else *distance = 1;
*shift_object = found_shift_object - cursor->shift_object;
result = 1;
}
}
}
else
if (cursor->shift_vmt <= found_shift_vmt) {
int tmp_5;
if (base_index < number_of_bases - 1) tmp_5 = (cursor + 1)->shift_vmt > found_shift_vmt;
else {
int tmp_4;
if (last_shift_vmt == -1) tmp_4 = 1;
else
if (found_shift_vmt < last_shift_vmt) tmp_4 = 1; else tmp_4 = 0;
tmp_5 = tmp_4;
}
if (tmp_5) {
int tmp_0;
int tmp;
int local_distance = 0;
int local_shift_object = 0;
if (base_index < number_of_bases - 1) tmp = (cursor + 1)->shift_vmt;
else tmp = last_shift_vmt;
;
;
;
;
;
tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
(cursor->value)->base_classes,
(cursor->value)->number_of_base_classes,
found_shift_object - cursor->shift_object,
found_shift_vmt - cursor->shift_vmt,
tmp,& local_shift_object,
& local_distance); int local_result = tmp_0;
if (local_result != 0)
if (local_distance >= 0)
if (*distance < 0) goto _LOR_0;
else
if (*distance >= local_distance) {
_LOR_0:
{
result = local_result;
*shift_object = local_shift_object - cursor->shift_object;
*distance = local_distance;
}
}
is_over = 1;
}
else goto _LAND;
}
else {
_LAND: ;
if (*distance < 0) goto _LOR_2;
else
if (*distance >= 1) {
_LOR_2:
{
int tmp_2;
int tmp_1;
int local_distance_0 = 0;
int local_shift_object_0 = 0;
if (base_index < number_of_bases + 1) tmp_1 = (cursor + 1)->shift_vmt;
else tmp_1 = last_shift_vmt;
;
;
;
;
;
tmp_2 = _frama_c_find_dynamic_cast_aux(target_info,
(cursor->value)->base_classes,
(cursor->value)->number_of_base_classes,
found_shift_object - cursor->shift_object,
found_shift_vmt - cursor->shift_vmt,
tmp_1,
& local_shift_object_0,
& local_distance_0);
int local_result_0 = tmp_2;
if (local_result_0 != 0)
if (local_distance_0 >= 0)
if (*distance < 0) goto _LOR_1;
else {
int tmp_3;
if (is_over == 0) tmp_3 = local_distance_0;
else tmp_3 = local_distance_0 + 1;
;
if (*distance > tmp_3) {
_LOR_1:
{
result = local_result_0;
*shift_object = local_shift_object_0 - cursor->shift_object;
*distance = local_distance_0 + 1;
}
}
}
}
}
}
cursor ++;
base_index ++;
}
return result;
}
int _frama_c_find_dynamic_cast(struct _frama_c_rtti_name_info_node *declared_info,
struct _frama_c_vmt *declared_vmt,
struct _frama_c_rtti_name_info_node *target_info,
int *shift_object)
{
int __retres;
int shift_vmt;
int elaborated_shift_target;
struct _frama_c_rtti_name_info_content *cursor;
int number_of_bases;
int tmp_0;
struct _frama_c_rtti_name_info_node *concrete_info =
declared_vmt->rtti_info;
int elaborated_shift_vmt = 0;
int elaborated_shift_object = 0;
int cursor_index = 0;
int distance = -1;
if (concrete_info->pvmt > declared_vmt) {
__retres = 0;
goto return_label;
}
else
if (declared_vmt > concrete_info->pvmt + declared_vmt->table_size) {
__retres = 0;
goto return_label;
}
shift_vmt = declared_vmt - concrete_info->pvmt;
if (concrete_info == declared_info) {
*shift_object = 0;
__retres = target_info == declared_info;
goto return_label;
}
if (target_info == concrete_info) elaborated_shift_target = 0;
else elaborated_shift_target = -1;
cursor = concrete_info->base_classes;
number_of_bases = concrete_info->number_of_base_classes;
while (1) {
while (1) {
if (cursor_index < number_of_bases) {
if (! (elaborated_shift_vmt + cursor->shift_vmt < shift_vmt))
break;
}
else break;
{
struct _frama_c_rtti_name_info_content *tmp;
if (cursor_index < number_of_bases - 1) tmp = cursor + 1;
else tmp = (struct _frama_c_rtti_name_info_content *)0;
struct _frama_c_rtti_name_info_content *next_cursor = tmp;
if (next_cursor != (struct _frama_c_rtti_name_info_content *)0)
if (elaborated_shift_vmt + next_cursor->shift_vmt <= shift_vmt) {
cursor = next_cursor;
cursor_index ++;
}
else break;
else break;
}
}
if (cursor_index < number_of_bases) {
elaborated_shift_vmt += cursor->shift_vmt;
elaborated_shift_object += cursor->shift_object;
if (cursor->value == target_info) elaborated_shift_target = elaborated_shift_object;
if (elaborated_shift_vmt == shift_vmt)
if (cursor->value == declared_info) {
if (elaborated_shift_target >= 0) {
*shift_object = elaborated_shift_target - elaborated_shift_object;
__retres = 1;
goto return_label;
}
break;
} cursor = (cursor->value)->base_classes;
number_of_bases = (cursor->value)->number_of_base_classes;
cursor_index = 0;
}
if (! (cursor_index < number_of_bases)) break;
}
if (cursor_index >= number_of_bases) {
__retres = 0;
goto return_label;
}
tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
concrete_info->base_classes,
concrete_info->number_of_base_classes,
elaborated_shift_object,shift_vmt,
-1,shift_object,& distance);
__retres = tmp_0;
return_label: return __retres;
}
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& exception::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "exception",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& bad_exception::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what), .shift_this = 0}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct bad_exception *)0)->_frama_c__ZN3stdE9exception),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "bad_exception",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[1] =
{{.method_ptr = (void (*)())(& nested_exception::Dtor), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "nested_exception",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 1,
.rtti_info = & _frama_c_rtti_name_info};
int __fc_errno;
char *program_invocation_name;
char *program_invocation_short_name;
/*@ assigns \nothing; */
void (*signal(int sig, void (*func)(int )))(int );
/*@ ensures never_terminates: \false;
assigns \nothing; */
int raise(int sig);
/*@ requires valid_set: \valid(set);
ensures set: initialization: \initialized(\old(set)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns *set, \result;
assigns *set \from \nothing;
assigns \result \from \nothing;
*/
int sigemptyset(sigset_t *set);
/*@ requires valid_set: \valid(set);
ensures set: initialization: \initialized(\old(set));
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns *set, \result;
assigns *set \from \nothing;
assigns \result \from \nothing;
*/
int sigfillset(sigset_t *set);
/*@ requires valid_set: \valid(set);
requires set: initialization: \initialized(set);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns *set, \result;
assigns *set \from (indirect: signum);
assigns \result \from signum;
*/
int sigaddset(sigset_t *set, int signum);
/*@ requires valid_set: \valid(set);
requires set: initialization: \initialized(set);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns *set, \result;
assigns *set \from (indirect: signum);
assigns \result \from signum;
*/
int sigdelset(sigset_t *set, int signum);
/*@ requires valid_read_set: \valid_read(set);
requires set: initialization: \initialized(set);
ensures
result_found_not_found_or_error:
\result ≡ 0 ∨ \result ≡ 1 ∨ \result ≡ -1;
assigns \result;
assigns \result \from *set, signum;
*/
int sigismember(sigset_t const *set, int signum);
struct sigaction __fc_sigaction[65];
struct sigaction *__fc_p_sigaction = __fc_sigaction;
/*@ requires valid_signal: 0 ≤ signum ≤ 64;
requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact);
requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act);
requires separated_acts: separation: \separated(act, oldact);
ensures
act_changed:
\old(act) ≡ \null ∨
\subset(*(__fc_p_sigaction + \old(signum)), *\old(act));
ensures
oldact_assigned:
\old(oldact) ≡ \null ∨
*\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns *oldact, *(__fc_p_sigaction + signum), \result;
assigns *oldact \from __fc_p_sigaction;
assigns *(__fc_p_sigaction + signum) \from *act;
assigns \result
\from (indirect: signum), (indirect: act), (indirect: *act),
(indirect: oldact), (indirect: *oldact);
*/
int sigaction(int signum, struct sigaction const * __restrict act,
struct sigaction * __restrict oldact);
/*@ requires valid_set_or_null: set ≡ \null ∨ \valid_read(set); */int sigprocmask(int how, sigset_t const * __restrict set,
sigset_t * __restrict oldset);
/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result \from (indirect: pid), (indirect: sig);
*/
int kill(pid_t pid, int sig);
/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result \from (indirect: pgrp), (indirect: sig);
*/
int killpg(pid_t pgrp, int sig);
void tm::Ctor(struct tm const *this);
/*@ ghost unsigned int volatile __fc_time; */
/*@ assigns \result;
assigns \result \from __fc_time; */
clock_t clock(void);
/*@ assigns \result;
assigns \result \from time1, time0; */
double difftime(time_t time1, time_t time0);
/*@ requires valid_timeptr: \valid(timeptr);
assigns *timeptr, \result;
assigns *timeptr \from *timeptr;
assigns \result \from (indirect: *timeptr);
*/
time_t mktime(struct tm *timeptr);
/*@ assigns *timer, \result;
assigns *timer \from __fc_time;
assigns \result \from __fc_time;
behavior null:
assumes timer_null: timer ≡ \null;
assigns \result;
assigns \result \from __fc_time;
behavior not_null:
assumes timer_non_null: timer ≢ \null;
requires valid_timer: \valid(timer);
ensures timer: initialization: \initialized(\old(timer));
assigns *timer, \result;
assigns *timer \from __fc_time;
assigns \result \from __fc_time;
complete behaviors not_null, null;
disjoint behaviors not_null, null;
*/
time_t time(time_t *timer);
char __fc_ctime[26];
char * const __fc_p_ctime = __fc_ctime;
/*@ requires valid_timeptr: \valid_read(timeptr);
requires init_timeptr: initialization: \initialized(timeptr);
ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
ensures result_valid_string: valid_read_string(__fc_p_ctime);
assigns __fc_ctime[0 .. 25], \result;
assigns __fc_ctime[0 .. 25]
\from (indirect: *timeptr), (indirect: __fc_time);
assigns \result
\from (indirect: *timeptr), (indirect: __fc_time), __fc_p_ctime;
*/
char *asctime(struct tm const *timeptr);
/*@ requires valid_timer: \valid_read(timer); requires init_timer: initialization: \initialized(timer);
ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
ensures result_valid_string: valid_read_string(__fc_p_ctime);
assigns __fc_ctime[0 .. 25], \result;
assigns __fc_ctime[0 .. 25]
\from (indirect: *timer), (indirect: __fc_time);
assigns \result
\from (indirect: *timer), (indirect: __fc_time), __fc_p_ctime;
*/
char *ctime(time_t const *timer);
struct tm __fc_time_tm;
void __fc_init__fc_time_tm(void) __attribute__((__constructor__));
void __fc_init__fc_time_tm(void)
{
tm::Ctor((struct tm const *)(& __fc_time_tm));
return;
}
struct tm * const __fc_p_time_tm = & __fc_time_tm;
/*@ requires valid_timer: \valid_read(timer);
ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
assigns \result, __fc_time_tm;
assigns \result \from __fc_p_time_tm;
assigns __fc_time_tm \from *timer;
*/
struct tm *gmtime(time_t const *timer);
/*@ requires valid_timer: \valid_read(timer);
ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
assigns \result, __fc_time_tm;
assigns \result \from __fc_p_time_tm;
assigns __fc_time_tm \from *timer;
*/
struct tm *localtime(time_t const *timer);
/*@ requires dst_has_room: \valid(s + (0 .. max - 1));
requires valid_format: valid_read_string(format);
requires valid_tm: \valid_read(tm);
ensures result_bounded: \result ≤ \old(max);
assigns *(s + (0 .. max - 1)), \result;
assigns *(s + (0 .. max - 1))
\from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
assigns \result
\from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
*/
size_t strftime(char * __restrict s, size_t max,
char const * __restrict format,
struct tm const * __restrict tm);
/*@ requires tp: \valid(tp);
assigns \result, *tp, __fc_time;
assigns \result \from __fc_time;
assigns *tp \from __fc_time;
assigns __fc_time \from __fc_time;
behavior realtime_clock:
assumes realtime: clk_id ≡ 666;
ensures success: \result ≡ 0;
ensures initialization: \initialized(\old(tp));
behavior monotonic_clock:
assumes monotonic: clk_id ≡ 1;
ensures success: \result ≡ 0;
ensures initialization: \initialized(\old(tp));
behavior bad_clock_id:
assumes bad_id: clk_id ≢ 666 ∧ clk_id ≢ 1;
ensures error: \result ≡ 22;
assigns \result;
assigns \result \from clk_id;
complete behaviors bad_clock_id, monotonic_clock, realtime_clock;
disjoint behaviors bad_clock_id, monotonic_clock, realtime_clock;
*/
int clock_gettime(clockid_t clk_id, struct timespec *tp);
/*@
axiomatic nanosleep_predicates {
predicate abs_clock_in_range{L}(clockid_t id, struct timespec *tm)
reads __fc_time;
predicate valid_clock_id{L}(clockid_t id)
reads __fc_time;
}
*/
/*@ ghost int volatile __fc_interrupted; */
/*@ requires valid_request: \valid_read(rqtp);
requires
initialized_request: initialization:
\initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
assigns \result;
assigns \result
\from (indirect: __fc_time), (indirect: __fc_interrupted),
(indirect: clock_id), (indirect: flags), (indirect: rqtp),
(indirect: *rqtp);
behavior absolute:
assumes absolute_time: (flags & 1) ≢ 0;
assumes
no_einval:
abs_clock_in_range(clock_id, rqtp) ∧ valid_clock_id(clock_id);
ensures
result_ok_or_error:
\result ≡ 0 ∨ \result ≡ 4 ∨ \result ≡ 22 ∨
\result ≡ 95;
assigns \result;
assigns \result
\from (indirect: __fc_time), (indirect: __fc_interrupted),
(indirect: clock_id), (indirect: rqtp), (indirect: *rqtp);
behavior relative_interrupted:
assumes relative_time: (flags & 1) ≡ 0;
assumes interrupted: __fc_interrupted ≢ 0;
assumes no_einval: valid_clock_id(clock_id);
ensures result_interrupted: \result ≡ 4;
ensures
interrupted_remaining: initialization:
\old(rmtp) ≢ \null ⇒
\initialized(&\old(rmtp)->tv_sec) ∧
\initialized(&\old(rmtp)->tv_nsec);
ensures
interrupted_remaining_decreases:
\old(rmtp) ≢ \null ⇒
\old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
\old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
ensures
remaining_valid:
\old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
assigns \result, *rmtp;
assigns \result
\from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp);
assigns *rmtp
\from __fc_time, (indirect: clock_id), (indirect: rqtp),
(indirect: *rqtp), (indirect: rmtp);
behavior relative_no_error:
assumes relative_time: (flags & 1) ≡ 0;
assumes not_interrupted: __fc_interrupted ≡ 0;
assumes no_einval: valid_clock_id(clock_id);
ensures result_ok: \result ≡ 0;
assigns \result;
assigns \result
\from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
(indirect: *rqtp);
behavior relative_invalid_clock_id:
assumes relative_time: (flags & 1) ≡ 0;
assumes not_interrupted: __fc_interrupted ≡ 0;
assumes einval: ¬valid_clock_id(clock_id);
ensures result_einval: \result ≡ 22;
assigns \result;
assigns \result
\from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
(indirect: *rqtp);
complete behaviors relative_invalid_clock_id,
relative_no_error,
relative_interrupted,
absolute;
disjoint behaviors relative_invalid_clock_id,
relative_no_error,
relative_interrupted,
absolute;
*/
int clock_nanosleep(clockid_t clock_id, int flags,
struct timespec const *rqtp, struct timespec *rmtp);
/*@ requires valid_timer: \valid_read(timer);
requires valid_result: \valid(result);
ensures
result_null_or_result: \result ≡ \old(result) ∨ \result ≡ \null;
assigns \result, *result;
assigns \result \from (indirect: *timer), result;
assigns *result \from (indirect: *timer);
*/
struct tm *gmtime_r(time_t const * __restrict timer,
struct tm * __restrict result);
/*@ requires valid_request: \valid_read(rqtp);
requires
initialized_request: initialization:
\initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
ensures
interrupted_remaining: initialization:
\old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
\initialized(&\old(rmtp)->tv_sec) ∧
\initialized(&\old(rmtp)->tv_nsec);
ensures
interrupted_remaining_decreases:
\old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
\old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
\old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
ensures
interrupted_remaining_valid:
\old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
0 ≤ \old(rmtp)->tv_nsec < 1000000000;
assigns \result, *rmtp; assigns \result
\from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
assigns *rmtp
\from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
(indirect: rmtp);
*/
int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);
int daylight;
long timezone;
char *tzname[2];
/*@ assigns *(tzname[0 .. 1] + (0 ..));
assigns *(tzname[0 .. 1] + (0 ..)) \from \nothing;
*/
void tzset(void);
/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
requires valid_dest: \valid(dest + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result \from dest;
*/
int *wmemmove(int *dest, int const *src, size_t n);
/*@ requires valid_wcs: \valid(wcs + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(wcs);
ensures
wcs: initialization: \initialized(\old(wcs) + (0 .. \old(n) - 1));
ensures
contents_equal_wc: \subset(*(\old(wcs) + (0 .. \old(n) - 1)), \old(wc));
assigns *(wcs + (0 .. n - 1)), \result;
assigns *(wcs + (0 .. n - 1)) \from wc, (indirect: n);
assigns \result \from wcs;
*/
int *wmemset(int *wcs, int wc, size_t n);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires valid_wstring_dest: valid_wstring(dest);
requires
room_for_concatenation:
\valid(dest + (wcslen(dest) .. wcslen(dest) + wcslen(src)));
requires
separation:
\separated(
dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
);
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 ..)),
(indirect: src);
assigns \result \from dest;
*/
int *wcscat(int * __restrict dest, int const * __restrict src);
/*@ requires valid_wstring_src: valid_read_wstring(wcs);
ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
*/
int *wcschr(int const *wcs, int wc);
/*@ requires valid_wstring_s1: valid_read_wstring(s1);
requires valid_wstring_s2: valid_read_wstring(s2);
assigns \result;
assigns \result \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
int wcscmp(int const *s1, int const *s2);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires room_wstring: \valid(dest + (0 .. wcslen(src)));
requires
separation:
\separated(dest + (0 .. wcslen(src)), src + (0 .. wcslen(src)));
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 .. wcslen{Old}(src))), \result;
assigns *(dest + (0 .. wcslen{Old}(src)))
\from *(src + (0 .. wcslen{Old}(src))), (indirect: src);
assigns \result \from dest;
*/
int *wcscpy(int * __restrict dest, int const * __restrict src);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
requires valid_wstring_accept: valid_read_wstring(accept);
assigns \result;
assigns \result
\from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
size_t wcscspn(int const *wcs, int const *accept);
/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
requires valid_wstring_dest: valid_wstring(dest);
requires
room_for_concatenation:
\valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
requires
separation:
\separated(
dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
(indirect: src), (indirect: n);
assigns \result
\from (indirect: *(dest + (0 ..))), (indirect: *(src + (0 .. n - 1))),
(indirect: n);
*/
size_t wcslcat(int * __restrict dest, int const * __restrict src, size_t n);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires room_nwstring: \valid(dest + (0 .. n));
requires
src: dest: separation:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result
\from (indirect: *(dest + (0 .. n - 1))), (indirect: dest),
(indirect: *(src + (0 .. n - 1))), (indirect: src), (indirect: n);
*/
size_t wcslcpy(int *dest, int const *src, size_t n);
/*@ requires valid_string_s: valid_read_wstring(s);
ensures result_is_length: \result ≡ wcslen(\old(s));
assigns \result;
assigns \result \from (indirect: *(s + (0 .. wcslen{Old}(s))));
*/
size_t wcslen(int const *s);
/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
requires valid_wstring_dest: valid_wstring(dest);
requires
room_for_concatenation: \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
requires
separation:
\separated(
dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
);
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
(indirect: src), (indirect: n);
assigns \result \from dest;
*/
int *wcsncat(int * __restrict dest, int const * __restrict src, size_t n);
/*@ requires valid_wstring_s1: valid_read_wstring(s1);
requires valid_wstring_s2: valid_read_wstring(s2);
assigns \result;
assigns \result
\from (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
int wcsncmp(int const *s1, int const *s2, size_t n);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires room_nwstring: \valid(dest + (0 .. n - 1));
requires
src: dest: separation:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result \from dest;
*/
int *wcsncpy(int * __restrict dest, int const * __restrict src, size_t n);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
requires valid_wstring_accept: valid_read_wstring(accept);
ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
assigns \result
\from wcs, (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
int *wcspbrk(int const *wcs, int const *accept);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
assigns \result
\from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
*/
int *wcsrchr(int const *wcs, int wc);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
requires valid_wstring_accept: valid_read_wstring(accept);
assigns \result;
assigns \result
\from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
(indirect: *(accept + (0 .. wcslen{Old}(accept))));
*/
size_t wcsspn(int const *wcs, int const *accept);
/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
requires valid_wstring_needle: valid_read_wstring(needle); ensures
result_null_or_inside_haystack:
\result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
assigns \result;
assigns \result
\from haystack, (indirect: *(haystack + (0 ..))),
(indirect: *(needle + (0 ..)));
*/
int *wcsstr(int const *haystack, int const *needle);
/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
requires valid_stream: \valid(stream);
ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
ensures
terminated_string_on_success:
\result ≢ \null ⇒ valid_wstring(\old(ws));
assigns *(ws + (0 .. n - 1)), \result;
assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
assigns \result \from ws, (indirect: n), (indirect: *stream);
*/
int *fgetws(int * __restrict ws, int n, FILE * __restrict stream);
/*@ axiomatic wformat_length {
logic ℤ wformat_length{L}(int *format) ;
}
*/
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(c2);
requires \valid(c1); */
void assign(char_type *c1, char_type const *c2);
/*@ requires \valid_read(a); */
char_type const *find(char_type const *s, size_t n, char_type const *a);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(c2);
requires \valid(c1); */
void assign(char_type *c1, char_type const *c2);
/*@ requires \valid_read(a); */
char_type const *find(char_type const *s, size_t n, char_type const *a);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "char_traits",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "char_traits",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
/*@ requires \valid(b);
requires \valid(a); */
void swap<void*>(void **a, void **b)
{
void *tmp = *a;
*a = *b;
*b = tmp;
return;
}
/*@ requires \valid(b);
requires \valid(a); */
void swap<std::__shared_ref_base*>(struct __shared_ref_base **a,
struct __shared_ref_base **b)
{
struct __shared_ref_base *tmp = *a;
*a = *b;
*b = tmp;
return;
}
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this);
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this,
struct piecewise_construct_t const *__frama_c_arg_0);
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this,
struct piecewise_construct_t *__frama_c_arg_0);
void piecewise_construct_t::Dtor(struct piecewise_construct_t const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this)
{
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this,
struct piecewise_construct_t const *__frama_c_arg_0)
{
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
void piecewise_construct_t::Ctor(struct piecewise_construct_t const *this,
struct piecewise_construct_t *__frama_c_arg_0)
{
return;
}
/*@ requires \valid_read(this); */
void piecewise_construct_t::Dtor(struct piecewise_construct_t const *this)
{
return;
}
struct piecewise_construct_t piecewise_construct;
void __fc_init_ZN3stdE19piecewise_construct(void) __attribute__((__constructor__));
void __fc_init_ZN3stdE19piecewise_construct(void)
{
struct piecewise_construct_t __fc_tmp_0;
piecewise_construct_t::Ctor(& __fc_tmp_0);
piecewise_construct = __fc_tmp_0;
piecewise_construct_t::Dtor((struct piecewise_construct_t const *)(& __fc_tmp_0));
return;
}
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "piecewise_construct_t", .base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
struct __shared_ref_base *operator=(struct __shared_ref_base *this,
struct __shared_ref_base const *__frama_c_arg_0);
struct __shared_ref_base *operator=(struct __shared_ref_base *this,
struct __shared_ref_base *__frama_c_arg_0);
void __shared_ref_base::Dtor(struct __shared_ref_base const *this);
void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
struct __shared_ref_base const *__frama_c_arg_0);
void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
struct __shared_ref_base *__frama_c_arg_0);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[7];
/*@ requires \valid(this); */
void unlink(struct __shared_ref_base *this);
/*@ requires \valid(this); */
void link(struct __shared_ref_base *this);
/*@ requires \valid(this); */
long count(struct __shared_ref_base *this);
/*@ requires \valid(this); */
void weak_unlink(struct __shared_ref_base *this);
/*@ requires \valid(this); */
void weak_link(struct __shared_ref_base *this);
/*@ requires \valid(this); */
struct __shared_ref_base *ref(struct __shared_ref_base *this);
/*@ requires \valid(this); */
void *get_deleter(struct __shared_ref_base *this)
{
void *__retres;
__retres = (void *)0;
return __retres;
}
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct __shared_ref_base *operator=(struct __shared_ref_base *this,
struct __shared_ref_base const *__frama_c_arg_0)
{
this->pvmt = __frama_c_arg_0->pvmt;
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct __shared_ref_base *operator=(struct __shared_ref_base *this,
struct __shared_ref_base *__frama_c_arg_0){
this->pvmt = __frama_c_arg_0->pvmt;
return this;
}
/*@ requires \valid_read(this); */
void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
struct __shared_ref_base const *__frama_c_arg_0)
{
this->pvmt = __frama_c_arg_0->pvmt;
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
void __shared_ref_base::Ctor(struct __shared_ref_base const *this,
struct __shared_ref_base *__frama_c_arg_0)
{
this->pvmt = __frama_c_arg_0->pvmt;
return;
}
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "allocator",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt_content _frama_c_vmt[7] =
{{.method_ptr = (void (*)())(& unlink), .shift_this = 0},
{.method_ptr = (void (*)())(& link), .shift_this = 0},
{.method_ptr = (void (*)())(& count), .shift_this = 0},
{.method_ptr = (void (*)())(& weak_unlink), .shift_this = 0},
{.method_ptr = (void (*)())(& weak_link), .shift_this = 0},
{.method_ptr = (void (*)())(& ref), .shift_this = 0},
{.method_ptr = (void (*)())(& get_deleter), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "__shared_ref_base",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 7,
.rtti_info = & _frama_c_rtti_name_info};
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
struct __shared_ref<void> const *__frama_c_arg_0);
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
struct __shared_ref<void> *__frama_c_arg_0);
void __shared_ref<void>::Dtor(struct __shared_ref<void> const *this);
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
struct __shared_ref<void> const *__frama_c_arg_0);
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
struct __shared_ref<void> *__frama_c_arg_0);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[7];
/*@ requires \valid_read(this); */
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this, void *p);
/*@ requires \valid(this); */
void unlink(struct __shared_ref<void> *this);
/*@ requires \valid(this); */
void link(struct __shared_ref<void> *this);
/*@ requires \valid(this); */
long count(struct __shared_ref<void> *this);
/*@ requires \valid(this); */
void weak_unlink(struct __shared_ref<void> *this);
/*@ requires \valid(this); */
void weak_link(struct __shared_ref<void> *this);
/*@ requires \valid(this); */
struct __shared_ref_base *ref(struct __shared_ref<void> *this);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
struct __shared_ref<void> const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE17__shared_ref_base,
& __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
this->__ptr = __frama_c_arg_0->__ptr;
this->_n = __frama_c_arg_0->_n;
this->_w = __frama_c_arg_0->_w;
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct __shared_ref<void> *operator=(struct __shared_ref<void> *this,
struct __shared_ref<void> *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE17__shared_ref_base,
& __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
this->__ptr = __frama_c_arg_0->__ptr;
this->_n = __frama_c_arg_0->_n;
this->_w = __frama_c_arg_0->_w;
return this;
}
/*@ requires \valid_read(this); */
void __shared_ref<void>::Dtor(struct __shared_ref<void> const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
__shared_ref_base::Dtor(& this->_frama_c__ZN3stdE17__shared_ref_base);
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0); */
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
struct __shared_ref<void> const *__frama_c_arg_0)
{
__shared_ref_base::Ctor(& this->_frama_c__ZN3stdE17__shared_ref_base,
& __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
this->__ptr = __frama_c_arg_0->__ptr;
this->_n = __frama_c_arg_0->_n;
this->_w = __frama_c_arg_0->_w;
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
void __shared_ref<void>::Ctor(struct __shared_ref<void> const *this,
struct __shared_ref<void> *__frama_c_arg_0)
{
__shared_ref_base::Ctor(& this->_frama_c__ZN3stdE17__shared_ref_base,
& __frama_c_arg_0->_frama_c__ZN3stdE17__shared_ref_base);
this->__ptr = __frama_c_arg_0->__ptr;
this->_n = __frama_c_arg_0->_n;
this->_w = __frama_c_arg_0->_w;
return;
}
struct _frama_c_vmt_content _frama_c_vmt[7] =
{{.method_ptr = (void (*)())(& unlink), .shift_this = 0},
{.method_ptr = (void (*)())(& link), .shift_this = 0},
{.method_ptr = (void (*)())(& count), .shift_this = 0},
{.method_ptr = (void (*)())(& weak_unlink), .shift_this = 0},
{.method_ptr = (void (*)())(& weak_link), .shift_this = 0},
{.method_ptr = (void (*)())(& ref), .shift_this = 0},
{.method_ptr = (void (*)())(& get_deleter),
.shift_this = (char *)(& ((struct __shared_ref<void> *)0)->_frama_c__ZN3stdE17__shared_ref_base) - (char *)(& ((struct __shared_ref<void> *)0)->_frama_c__ZN3stdE17__shared_ref_base)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct __shared_ref<void> *)0)->_frama_c__ZN3stdE17__shared_ref_base),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "__shared_ref",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 7,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
struct bad_weak_ptr const *__frama_c_arg_0);
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
struct bad_weak_ptr *__frama_c_arg_0);
struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
struct bad_weak_ptr const *__frama_c_arg_0);
struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
struct bad_weak_ptr *__frama_c_arg_0);
void bad_weak_ptr::Dtor(struct bad_weak_ptr const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this); */
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception);
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
struct bad_weak_ptr const *__frama_c_arg_0)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return;
}
void exception::Ctor(struct exception const *this,
struct exception *__frama_c_arg_0)
{
this->pvmt = __frama_c_arg_0->pvmt;
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
void bad_weak_ptr::Ctor(struct bad_weak_ptr const *this,
struct bad_weak_ptr *__frama_c_arg_0)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return;
}
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
struct bad_weak_ptr const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return this;
}
struct exception *operator=(struct exception *this,
struct exception *__frama_c_arg_0)
{
this->pvmt = __frama_c_arg_0->pvmt;
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct bad_weak_ptr *operator=(struct bad_weak_ptr *this,
struct bad_weak_ptr *__frama_c_arg_0)
{ operator=(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return this;
}
/*@ requires \valid_read(this); */
void bad_weak_ptr::Dtor(struct bad_weak_ptr const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
exception::Dtor(& this->_frama_c__ZN3stdE9exception);
return;
}
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this)
{
this->_ref = (struct __shared_ref_base *)0;
return;
}
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
struct shared_ptr<void> const *r);
/*@ requires \separated(this, r);
requires \valid_read(this);
requires \valid(r);
*/
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
struct shared_ptr<void> *r)
{
this->__ptr = r->__ptr;
this->_ref = r->_ref;
r->__ptr = (void *)0;
r->_ref = (struct __shared_ref_base *)0;
return;
}
/*@ requires \valid_read(this); */
void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
nullptr_t __frama_c_arg_0)
{
this->_ref = (struct __shared_ref_base *)0;
return;
}
/*@ requires \valid_read(this); */
void shared_ptr<void>::Dtor(struct shared_ptr<void> const *this)
{
if (this->_ref != (struct __shared_ref_base *)0) {
struct _frama_c_vmt_content *__virtual_tmp_0 =
(*((struct _frama_c_vmt **)this->_ref))->table + 0;
(*((void (*)(struct __shared_ref_base *))__virtual_tmp_0->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_0->shift_this));
}
return;
}
/*@ requires \valid(this);
requires \valid_read(r);
ensures \valid(\result); */
struct shared_ptr<void> *operator=(struct shared_ptr<void> *this,
struct shared_ptr<void> const *r)
{
if (this->_ref != r->_ref) {
this->__ptr = r->__ptr;
if (this->_ref != (struct __shared_ref_base *)0) { struct _frama_c_vmt_content *__virtual_tmp_1 =
(*((struct _frama_c_vmt **)this->_ref))->table + 0;
(*((void (*)(struct __shared_ref_base *))__virtual_tmp_1->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_1->shift_this));
}
this->_ref = r->_ref;
if (this->_ref != (struct __shared_ref_base *)0) {
struct _frama_c_vmt_content *__virtual_tmp_2 =
(*((struct _frama_c_vmt **)this->_ref))->table + 1;
(*((void (*)(struct __shared_ref_base *))__virtual_tmp_2->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_2->shift_this));
}
}
return this;
}
/*@ requires \valid(this);
requires \valid(r);
ensures \valid(\result); */
struct shared_ptr<void> *operator=(struct shared_ptr<void> *this,
struct shared_ptr<void> *r)
{
if (this->_ref != (struct __shared_ref_base *)0) {
struct _frama_c_vmt_content *__virtual_tmp_3 =
(*((struct _frama_c_vmt **)this->_ref))->table + 0;
(*((void (*)(struct __shared_ref_base *))__virtual_tmp_3->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_3->shift_this));
}
if (this->_ref != r->_ref) {
this->__ptr = r->__ptr;
this->_ref = r->_ref;
}
r->_ref = (struct __shared_ref_base *)0;
return this;
}
/*@ requires \valid(this);
requires \valid(r); */
void swap(struct shared_ptr<void> *this, struct shared_ptr<void> *r)
{
if (this->_ref != r->_ref) {
swap<void*>(& this->__ptr,& r->__ptr);
swap<std::__shared_ref_base*>(& this->_ref,& r->_ref);
}
return;
}
/*@ requires \valid(this); */
void reset(struct shared_ptr<void> *this)
{
if (this->_ref != (struct __shared_ref_base *)0) {
struct _frama_c_vmt_content *__virtual_tmp_4 =
(*((struct _frama_c_vmt **)this->_ref))->table + 0;
(*((void (*)(struct __shared_ref_base *))__virtual_tmp_4->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_4->shift_this));
this->_ref = (struct __shared_ref_base *)0;
}
return;
}
/*@ requires \valid_read(this); */
void *get(struct shared_ptr<void> const *this)
{
void *__retres;
__retres = this->__ptr;
return __retres;
}
/*@ requires \valid_read(this); */
void *std::shared_ptr<void>::operator->(struct shared_ptr<void> const *this){
void *tmp;
tmp = get(this);
return tmp;
}
/*@ requires \valid_read(this); */
long use_count(struct shared_ptr<void> const *this)
{
long tmp_0;
struct _frama_c_vmt_content *__virtual_tmp_5 =
(*((struct _frama_c_vmt **)this->_ref))->table + 2;
if (this->_ref == (struct __shared_ref_base *)0) tmp_0 = 0L;
else tmp_0 = (*((long (*)(struct __shared_ref_base *))__virtual_tmp_5->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_5->shift_this));
return tmp_0;
}
/*@ requires \valid_read(this); */
_Bool unique(struct shared_ptr<void> const *this)
{
_Bool __retres;
int tmp_0;
struct _frama_c_vmt_content *__virtual_tmp_6 =
(*((struct _frama_c_vmt **)this->_ref))->table + 2;
if (this->_ref == (struct __shared_ref_base *)0) tmp_0 = 0;
else {
long tmp;
tmp = (*((long (*)(struct __shared_ref_base *))__virtual_tmp_6->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_6->shift_this));
tmp_0 = tmp == 1L;
}
__retres = (_Bool)(tmp_0 != 0);
return __retres;
}
/*@ requires \valid_read(this); */
_Bool conversion(bool)(struct shared_ptr<void> const *this)
{
_Bool __retres;
__retres = (_Bool)(this->__ptr != (void *)0);
return __retres;
}
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "auto_ptr",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& bad_weak_ptr::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct bad_weak_ptr *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct bad_weak_ptr *)0)->_frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct bad_weak_ptr *)0)->_frama_c__ZN3stdE9exception),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "bad_weak_ptr",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
/*@ requires \separated(this, r);
requires \valid_read(this);
requires \valid_read(r);
*/void shared_ptr<void>::Ctor(struct shared_ptr<void> const *this,
struct shared_ptr<void> const *r)
{
struct _frama_c_vmt_content *__virtual_tmp_7 =
(*((struct _frama_c_vmt **)r->_ref))->table + 5;
if (r->_ref == (struct __shared_ref_base *)0) this->_ref = (struct __shared_ref_base *)0;
else this->_ref = (*((struct __shared_ref_base *(*)(struct __shared_ref_base *))__virtual_tmp_7->method_ptr))
((struct __shared_ref_base *)((char *)r->_ref - __virtual_tmp_7->shift_this));
if (this->_ref != (struct __shared_ref_base *)0) {
this->__ptr = get(r);
struct _frama_c_vmt_content *__virtual_tmp_8 =
(*((struct _frama_c_vmt **)this->_ref))->table + 1;
(*((void (*)(struct __shared_ref_base *))__virtual_tmp_8->method_ptr))
((struct __shared_ref_base *)((char *)this->_ref - __virtual_tmp_8->shift_this));
}
else this->__ptr = (void *)0;
return;
}
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "shared_ptr",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
/*@ requires \valid_read(str); */
int stoi(string const *str, size_t *idx, int base);
/*@ requires \valid_read(str); */
long stol(string const *str, size_t *idx, int base);
/*@ requires \valid_read(str); */
unsigned long stoul(string const *str, size_t *idx, int base);
/*@ requires \valid_read(str); */
long long stoll(string const *str, size_t *idx, int base);
/*@ requires \valid_read(str); */
unsigned long long stoull(string const *str, size_t *idx, int base);
/*@ requires \valid_read(str); */
float stof(string const *str, size_t *idx);
/*@ requires \valid_read(str); */
double stod(string const *str, size_t *idx);
/*@ requires \valid_read(str); */
long double stold(string const *str, size_t *idx);
void logic_error::Ctor(struct logic_error const *this,
struct logic_error const *__frama_c_arg_0);
void logic_error::Ctor(struct logic_error const *this,
struct logic_error *__frama_c_arg_0);
struct logic_error *operator=(struct logic_error *this,
struct logic_error const *__frama_c_arg_0);
struct logic_error *operator=(struct logic_error *this,
struct logic_error *__frama_c_arg_0);
void logic_error::Dtor(struct logic_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void logic_error::Ctor(struct logic_error const *this, string const *what_arg);
/*@ requires \valid_read(this); */
void logic_error::Ctor(struct logic_error const *this, char const *what_arg);
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void logic_error::Ctor(struct logic_error const *this,
struct logic_error const *__frama_c_arg_0)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
void logic_error::Ctor(struct logic_error const *this,
struct logic_error *__frama_c_arg_0)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return;
}
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct logic_error *operator=(struct logic_error *this,
struct logic_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct logic_error *operator=(struct logic_error *this,
struct logic_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return this;
}
/*@ requires \valid_read(this); */
void logic_error::Dtor(struct logic_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
exception::Dtor(& this->_frama_c__ZN3stdE9exception);
return;
}
struct domain_error *operator=(struct domain_error *this,
struct domain_error const *__frama_c_arg_0);
struct domain_error *operator=(struct domain_error *this,
struct domain_error *__frama_c_arg_0);
void domain_error::Dtor(struct domain_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void domain_error::Ctor(struct domain_error const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void domain_error::Ctor(struct domain_error const *this, char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct domain_error *operator=(struct domain_error *this,
struct domain_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct domain_error *operator=(struct domain_error *this,
struct domain_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid_read(this); */
void domain_error::Dtor(struct domain_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
return;
}
struct invalid_argument *operator=(struct invalid_argument *this,
struct invalid_argument const *__frama_c_arg_0);
struct invalid_argument *operator=(struct invalid_argument *this,
struct invalid_argument *__frama_c_arg_0);
void invalid_argument::Dtor(struct invalid_argument const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void invalid_argument::Ctor(struct invalid_argument const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void invalid_argument::Ctor(struct invalid_argument const *this,
char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct invalid_argument *operator=(struct invalid_argument *this,
struct invalid_argument const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct invalid_argument *operator=(struct invalid_argument *this,
struct invalid_argument *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid_read(this); */
void invalid_argument::Dtor(struct invalid_argument const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
return;
}
struct length_error *operator=(struct length_error *this,
struct length_error const *__frama_c_arg_0);
struct length_error *operator=(struct length_error *this,
struct length_error *__frama_c_arg_0);
void length_error::Dtor(struct length_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void length_error::Ctor(struct length_error const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void length_error::Ctor(struct length_error const *this, char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct length_error *operator=(struct length_error *this,
struct length_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct length_error *operator=(struct length_error *this,
struct length_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid_read(this); */
void length_error::Dtor(struct length_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
return;
}
struct out_of_range *operator=(struct out_of_range *this,
struct out_of_range const *__frama_c_arg_0);
struct out_of_range *operator=(struct out_of_range *this,
struct out_of_range *__frama_c_arg_0);
void out_of_range::Dtor(struct out_of_range const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void out_of_range::Ctor(struct out_of_range const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void out_of_range::Ctor(struct out_of_range const *this, char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct out_of_range *operator=(struct out_of_range *this,
struct out_of_range const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct out_of_range *operator=(struct out_of_range *this,
struct out_of_range *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE11logic_error,
& __frama_c_arg_0->_frama_c__ZN3stdE11logic_error);
return this;
}
/*@ requires \valid_read(this); */
void out_of_range::Dtor(struct out_of_range const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
logic_error::Dtor(& this->_frama_c__ZN3stdE11logic_error);
return;
}
void runtime_error::Ctor(struct runtime_error const *this,
struct runtime_error const *__frama_c_arg_0);
void runtime_error::Ctor(struct runtime_error const *this,
struct runtime_error *__frama_c_arg_0);
struct runtime_error *operator=(struct runtime_error *this,
struct runtime_error const *__frama_c_arg_0);
struct runtime_error *operator=(struct runtime_error *this,
struct runtime_error *__frama_c_arg_0);
void runtime_error::Dtor(struct runtime_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void runtime_error::Ctor(struct runtime_error const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void runtime_error::Ctor(struct runtime_error const *this,
char const *what_arg);
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
void runtime_error::Ctor(struct runtime_error const *this,
struct runtime_error const *__frama_c_arg_0)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return;
}
/*@ requires \separated(this, __frama_c_arg_0);
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
void runtime_error::Ctor(struct runtime_error const *this,
struct runtime_error *__frama_c_arg_0)
{
exception::Ctor(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return;
}
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct runtime_error *operator=(struct runtime_error *this,
struct runtime_error const *__frama_c_arg_0)
{ operator=(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct runtime_error *operator=(struct runtime_error *this,
struct runtime_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE9exception,
& __frama_c_arg_0->_frama_c__ZN3stdE9exception);
return this;
}
/*@ requires \valid_read(this); */
void runtime_error::Dtor(struct runtime_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
exception::Dtor(& this->_frama_c__ZN3stdE9exception);
return;
}
struct range_error *operator=(struct range_error *this,
struct range_error const *__frama_c_arg_0);
struct range_error *operator=(struct range_error *this,
struct range_error *__frama_c_arg_0);
void range_error::Dtor(struct range_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void range_error::Ctor(struct range_error const *this, string const *what_arg);
/*@ requires \valid_read(this); */
void range_error::Ctor(struct range_error const *this, char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct range_error *operator=(struct range_error *this,
struct range_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct range_error *operator=(struct range_error *this,
struct range_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;}
/*@ requires \valid_read(this); */
void range_error::Dtor(struct range_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
return;
}
struct overflow_error *operator=(struct overflow_error *this,
struct overflow_error const *__frama_c_arg_0);
struct overflow_error *operator=(struct overflow_error *this,
struct overflow_error *__frama_c_arg_0);
void overflow_error::Dtor(struct overflow_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void overflow_error::Ctor(struct overflow_error const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void overflow_error::Ctor(struct overflow_error const *this,
char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct overflow_error *operator=(struct overflow_error *this,
struct overflow_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct overflow_error *operator=(struct overflow_error *this,
struct overflow_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid_read(this); */
void overflow_error::Dtor(struct overflow_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
return;
}
struct underflow_error *operator=(struct underflow_error *this,
struct underflow_error const *__frama_c_arg_0);
struct underflow_error *operator=(struct underflow_error *this,
struct underflow_error *__frama_c_arg_0);
void underflow_error::Dtor(struct underflow_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void underflow_error::Ctor(struct underflow_error const *this,
string const *what_arg);
/*@ requires \valid_read(this); */
void underflow_error::Ctor(struct underflow_error const *this,
char const *what_arg);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
struct underflow_error *operator=(struct underflow_error *this,
struct underflow_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct underflow_error *operator=(struct underflow_error *this,
struct underflow_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid_read(this); */
void underflow_error::Dtor(struct underflow_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
return;
}
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& logic_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct logic_error *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct logic_error *)0)->_frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct logic_error *)0)->_frama_c__ZN3stdE9exception),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "logic_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2, .rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& domain_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct domain_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct domain_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct domain_error *)0)->_frama_c__ZN3stdE11logic_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "domain_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& invalid_argument::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct invalid_argument *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct invalid_argument *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct invalid_argument *)0)->_frama_c__ZN3stdE11logic_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "invalid_argument",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& length_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct length_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct length_error *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct length_error *)0)->_frama_c__ZN3stdE11logic_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "length_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& out_of_range::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct out_of_range *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct out_of_range *)0)->_frama_c__ZN3stdE11logic_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct out_of_range *)0)->_frama_c__ZN3stdE11logic_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "out_of_range",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] = {{.method_ptr = (void (*)())(& runtime_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct runtime_error *)0)->_frama_c__ZN3stdE9exception) - (char *)(& ((struct runtime_error *)0)->_frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct runtime_error *)0)->_frama_c__ZN3stdE9exception),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "runtime_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& range_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct range_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct range_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct range_error *)0)->_frama_c__ZN3stdE13runtime_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "range_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& overflow_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct overflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct overflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct overflow_error *)0)->_frama_c__ZN3stdE13runtime_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "overflow_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& underflow_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what),
.shift_this = (char *)(& ((struct underflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception) - (char *)(& ((struct underflow_error *)0)->_frama_c__ZN3stdE13runtime_error._frama_c__ZN3stdE9exception)}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct underflow_error *)0)->_frama_c__ZN3stdE13runtime_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "underflow_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[6];
/*@ requires \valid_read(this); */
void error_category::Dtor(struct error_category const *this);
/*@ requires \valid_read(this); */
char const *name(struct error_category const *this);
/*@ requires \valid_read(this); */
struct error_condition default_error_condition(struct error_category const *this,
int ev);
/*@ requires \valid_read(this);
requires \valid_read(condition); */
_Bool equivalent(struct error_category const *this, int code,
struct error_condition const *condition);
/*@ requires \valid_read(this);
requires \valid_read(code); */
_Bool equivalent(struct error_category const *this,
struct error_code const *code, int condition);
/*@ requires \valid_read(this); */
string message(struct error_category const *this, int ev);
/*@ requires \valid_read(this);
requires \valid_read(rhs); */
_Bool operator==(struct error_category const *this,
struct error_category const *rhs);
/*@ requires \valid_read(this);
requires \valid_read(rhs); */
_Bool operator!=(struct error_category const *this,
struct error_category const *rhs);
/*@ requires \valid_read(this);
requires \valid_read(rhs); */
_Bool operator<(struct error_category const *this,
struct error_category const *rhs);
/*@ ensures \valid_read(\result); */
struct error_category const *generic_category(void);
/*@ ensures \valid_read(\result); */
struct error_category const *system_category(void);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void error_code::Ctor(struct error_code const *this);
/*@ requires \valid_read(this);
requires \valid_read(cat); */
void error_code::Ctor(struct error_code const *this, int val,
struct error_category const *cat);
/*@ requires \valid(this);
requires \valid_read(cat); */
void assign(struct error_code *this, int val,
struct error_category const *cat);
/*@ requires \valid(this); */
void clear(struct error_code *this);
/*@ requires \valid_read(this); */
int value(struct error_code const *this);
/*@ requires \valid_read(this);
ensures \valid_read(\result); */
struct error_category const *category(struct error_code const *this);
/*@ requires \valid_read(this); */
struct error_condition default_error_condition(struct error_code const *this);
/*@ requires \valid_read(this); */
string message(struct error_code const *this);
/*@ requires \valid_read(this); */
_Bool conversion(bool)(struct error_code const *this);
struct system_error *operator=(struct system_error *this,
struct system_error const *__frama_c_arg_0);
struct system_error *operator=(struct system_error *this,
struct system_error *__frama_c_arg_0);
void system_error::Dtor(struct system_error const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[2];
/*@ requires \valid_read(this);
requires \valid_read(what_arg); */
void system_error::Ctor(struct system_error const *this,
struct error_code ec, string const *what_arg);
/*@ requires \valid_read(this); */
void system_error::Ctor(struct system_error const *this,
struct error_code ec, char const *what_arg);
/*@ requires \valid_read(this); */
void system_error::Ctor(struct system_error const *this, struct error_code ec);
/*@ requires \valid_read(this);
requires \valid_read(what_arg);
requires \valid_read(ecat);
*/
void system_error::Ctor(struct system_error const *this, int ev,
struct error_category const *ecat,
string const *what_arg);
/*@ requires \valid_read(this);
requires \valid_read(ecat); */
void system_error::Ctor(struct system_error const *this, int ev,
struct error_category const *ecat,
char const *what_arg);
/*@ requires \valid_read(this);
requires \valid_read(ecat); */
void system_error::Ctor(struct system_error const *this, int ev,
struct error_category const *ecat);
/*@ requires \valid_read(this);
ensures \valid_read(\result); */
struct error_code const *code(struct system_error const *this);
/*@ requires \valid_read(this); */
char const *what(struct system_error const *this);
/*@ requires \valid(this);
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result); */
struct system_error *operator=(struct system_error *this,
struct system_error const *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
struct system_error *operator=(struct system_error *this,
struct system_error *__frama_c_arg_0)
{
operator=(& this->_frama_c__ZN3stdE13runtime_error,
& __frama_c_arg_0->_frama_c__ZN3stdE13runtime_error);
return this;
}
/*@ requires \valid_read(this); */
void system_error::Dtor(struct system_error const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
runtime_error::Dtor(& this->_frama_c__ZN3stdE13runtime_error);
return;
}
struct _frama_c_vmt_content _frama_c_vmt[6] =
{{.method_ptr = (void (*)())(& error_category::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& name), .shift_this = 0},
{.method_ptr = (void (*)())(& default_error_condition), .shift_this = 0},
{.method_ptr = (void (*)())(& equivalent), .shift_this = 0},
{.method_ptr = (void (*)())(& equivalent), .shift_this = 0},
{.method_ptr = (void (*)())(& message), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "error_category",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 6,
.rtti_info = & _frama_c_rtti_name_info};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "error_code",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_vmt_content _frama_c_vmt[2] =
{{.method_ptr = (void (*)())(& system_error::Dtor), .shift_this = 0},
{.method_ptr = (void (*)())(& what), .shift_this = 0}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct system_error *)0)->_frama_c__ZN3stdE13runtime_error),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "system_error",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 2,
.rtti_info = & _frama_c_rtti_name_info};
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator<(struct error_code const *lhs, struct error_code const *rhs);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
void error_condition::Ctor(struct error_condition const *this);
/*@ requires \valid_read(this);
requires \valid_read(cat); */
void error_condition::Ctor(struct error_condition const *this, int val,
struct error_category const *cat);
/*@ requires \valid(this);
requires \valid_read(cat); */
void assign(struct error_condition *this, int val,
struct error_category const *cat);
/*@ requires \valid(this); */
void clear(struct error_condition *this);
/*@ requires \valid_read(this); */
int value(struct error_condition const *this);
/*@ requires \valid_read(this);
ensures \valid_read(\result); */
struct error_category const *category(struct error_condition const *this);
/*@ requires \valid_read(this); */
string message(struct error_condition const *this);
/*@ requires \valid_read(this); */
_Bool conversion(bool)(struct error_condition const *this);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator<(struct error_condition const *lhs,
struct error_condition const *rhs);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator==(struct error_code const *lhs, struct error_code const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator==(struct error_code const *lhs,
struct error_condition const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator==(struct error_condition const *lhs,
struct error_code const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator==(struct error_condition const *lhs,
struct error_condition const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator!=(struct error_code const *lhs, struct error_code const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator!=(struct error_code const *lhs,
struct error_condition const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator!=(struct error_condition const *lhs,
struct error_code const *rhs);
/*@ requires \valid_read(rhs);
requires \valid_read(lhs); */
_Bool operator!=(struct error_condition const *lhs,
struct error_condition const *rhs);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "error_condition",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "is_error_condition_enum",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};