|
|
|
|
SSL VCC_Max.b2i
Interaktion und
Portierbarkeitunbekannt
|
|
|
type-decl $ctype 0 0
type-decl $ptr 0 0
type-decl $field 0 0
type-decl $kind 0 0
type-decl $type_state 0 0
type-decl $status 0 0
type-decl $primitive 0 0
type-decl $struct 0 0
type-decl $token 0 0
type-decl $state 0 0
type-decl $pure_function 0 0
type-decl $label 0 0
type-decl $memory_t 0 0
type-decl $typemap_t 0 0
type-decl $statusmap_t 0 0
type-decl $record 0 0
type-decl $version 0 0
type-decl $vol_version 0 0
type-decl $ptrset 0 0
fun-decl $kind_of 2 0
type-con $ctype 0
type-con $kind 0
fun-decl $kind_composite 1 1
type-con $kind 0
attribute unique 0
fun-decl $kind_primitive 1 1
type-con $kind 0
attribute unique 0
fun-decl $kind_array 1 1
type-con $kind 0
attribute unique 0
fun-decl $kind_thread 1 1
type-con $kind 0
attribute unique 0
fun-decl $sizeof 2 0
type-con $ctype 0
int
fun-decl ^^i1 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^i2 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^i4 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^i8 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^u1 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^u2 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^u4 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^u8 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^void 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^bool 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^f4 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^f8 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^claim 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^root_emb 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^^mathint 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^$#thread_id_t 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^$#ptrset 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^$#state_t 1 1
type-con $ctype 0
attribute unique 0
fun-decl ^$#struct 1 1
type-con $ctype 0
attribute unique 0
fun-decl $ptr_to 2 0
type-con $ctype 0
type-con $ctype 0
fun-decl $unptr_to 2 0
type-con $ctype 0
type-con $ctype 0
fun-decl $ptr_level 2 0
type-con $ctype 0
int
fun-decl $map_t 3 0
type-con $ctype 0
type-con $ctype 0
type-con $ctype 0
fun-decl $map_domain 2 0
type-con $ctype 0
type-con $ctype 0
fun-decl $map_range 2 0
type-con $ctype 0
type-con $ctype 0
fun-decl $is_primitive 2 1
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $is_primitive_ch 2 1
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_composite 2 1
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $is_composite_ch 2 1
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_arraytype 2 1
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $is_arraytype_ch 2 1
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_threadtype 2 1
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $is_thread 2 1
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_ptr_to_composite 2 1
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $field_offset 2 0
type-con $field 0
int
fun-decl $field_parent_type 2 0
type-con $field 0
type-con $ctype 0
fun-decl $is_non_primitive 2 0
type-con $ctype 0
bool
fun-decl $is_non_primitive_ch 2 1
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_non_primitive_ptr 2 1
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $me_ref 1 0
int
fun-decl $me 1 0
type-con $ptr 0
fun-decl $current_state 2 1
type-con $state 0
type-con $state 0
attribute inline 1
expr-attr
true
fun-decl $select.mem 3 0
type-con $memory_t 0
type-con $ptr 0
int
fun-decl $store.mem 4 0
type-con $memory_t 0
type-con $ptr 0
int
type-con $memory_t 0
fun-decl $select.tm 3 0
type-con $typemap_t 0
type-con $ptr 0
type-con $type_state 0
fun-decl $store.tm 4 0
type-con $typemap_t 0
type-con $ptr 0
type-con $type_state 0
type-con $typemap_t 0
fun-decl $select.sm 3 0
type-con $statusmap_t 0
type-con $ptr 0
type-con $status 0
fun-decl $store.sm 4 0
type-con $statusmap_t 0
type-con $ptr 0
type-con $status 0
type-con $statusmap_t 0
fun-decl $memory 2 0
type-con $state 0
type-con $memory_t 0
fun-decl $typemap 2 0
type-con $state 0
type-con $typemap_t 0
fun-decl $statusmap 2 0
type-con $state 0
type-con $statusmap_t 0
fun-decl $mem 3 1
type-con $state 0
type-con $ptr 0
int
attribute inline 1
expr-attr
true
fun-decl $read_any 3 1
type-con $state 0
type-con $ptr 0
int
attribute inline 1
expr-attr
true
fun-decl $mem_eq 4 1
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $st_eq 4 1
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $ts_eq 4 1
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $extent_hint 3 0
type-con $ptr 0
type-con $ptr 0
bool
fun-decl $nesting_level 2 0
type-con $ctype 0
int
fun-decl $is_nested 3 0
type-con $ctype 0
type-con $ctype 0
bool
fun-decl $nesting_min 3 0
type-con $ctype 0
type-con $ctype 0
int
fun-decl $nesting_max 3 0
type-con $ctype 0
type-con $ctype 0
int
fun-decl $is_nested_range 5 0
type-con $ctype 0
type-con $ctype 0
int
int
bool
fun-decl $typ 2 0
type-con $ptr 0
type-con $ctype 0
fun-decl $ref 2 0
type-con $ptr 0
int
fun-decl $ptr 3 0
type-con $ctype 0
int
type-con $ptr 0
fun-decl $ghost_ref 3 0
type-con $ptr 0
type-con $field 0
int
fun-decl $ghost_emb 2 0
int
type-con $ptr 0
fun-decl $ghost_path 2 0
int
type-con $field 0
fun-decl $physical_ref 3 0
type-con $ptr 0
type-con $field 0
int
fun-decl $array_path 3 0
type-con $field 0
int
type-con $field 0
fun-decl $is_base_field 2 0
type-con $field 0
bool
fun-decl $array_path_1 2 0
type-con $field 0
type-con $field 0
fun-decl $array_path_2 2 0
type-con $field 0
int
fun-decl $null 1 0
type-con $ptr 0
fun-decl $is 3 0
type-con $ptr 0
type-con $ctype 0
bool
fun-decl $ptr_cast 3 1
type-con $ptr 0
type-con $ctype 0
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $read_ptr 4 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $dot 3 0
type-con $ptr 0
type-con $field 0
type-con $ptr 0
fun-decl $emb 3 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $path 3 1
type-con $state 0
type-con $ptr 0
type-con $field 0
attribute inline 1
expr-attr
true
fun-decl $containing_struct 3 0
type-con $ptr 0
type-con $field 0
type-con $ptr 0
fun-decl $containing_struct_ref 3 0
type-con $ptr 0
type-con $field 0
int
fun-decl $is_primitive_non_volatile_field 2 0
type-con $field 0
bool
fun-decl $is_primitive_volatile_field 2 0
type-con $field 0
bool
fun-decl $is_primitive_embedded_array 3 0
type-con $field 0
int
bool
fun-decl $is_primitive_embedded_volatile_array 4 0
type-con $field 0
int
type-con $ctype 0
bool
fun-decl $static_field_properties 3 1
type-con $field 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $field_properties 6 1
type-con $state 0
type-con $ptr 0
type-con $field 0
type-con $ctype 0
bool
bool
attribute inline 1
expr-attr
true
fun-decl $ts_typed 2 0
type-con $type_state 0
bool
fun-decl $ts_emb 2 0
type-con $type_state 0
type-con $ptr 0
fun-decl $ts_path 2 0
type-con $type_state 0
type-con $field 0
fun-decl $ts_is_array_elt 2 0
type-con $type_state 0
bool
fun-decl $ts_is_volatile 2 0
type-con $type_state 0
bool
fun-decl $is_object_root 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_volatile 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_malloc_root 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $current_timestamp 2 0
type-con $state 0
int
fun-decl $is_fresh 4 1
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $in_writes_at 3 0
int
type-con $ptr 0
bool
fun-decl $writable 4 1
type-con $state 0
int
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $top_writable 4 1
type-con $state 0
int
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $struct_zero 1 0
type-con $struct 0
fun-decl $vs_base 3 1
type-con $struct 0
type-con $ctype 0
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $vs_base_ref 2 0
type-con $struct 0
int
fun-decl $vs_state 2 0
type-con $struct 0
type-con $state 0
fun-decl $vs_ctor 3 0
type-con $state 0
type-con $ptr 0
type-con $struct 0
fun-decl $rec_zero 1 0
type-con $record 0
fun-decl $rec_update 4 0
type-con $record 0
type-con $field 0
int
type-con $record 0
fun-decl $rec_fetch 3 0
type-con $record 0
type-con $field 0
int
fun-decl $rec_update_bv 7 0
type-con $record 0
type-con $field 0
int
int
int
int
type-con $record 0
fun-decl $is_record_type 2 0
type-con $ctype 0
bool
fun-decl $is_record_field 4 0
type-con $ctype 0
type-con $field 0
type-con $ctype 0
bool
fun-decl $as_record_record_field 2 0
type-con $field 0
type-con $field 0
fun-decl $rec_eq 3 0
type-con $record 0
type-con $record 0
bool
fun-decl $rec_base_eq 3 0
int
int
bool
fun-decl $int_to_record 2 0
int
type-con $record 0
fun-decl $record_to_int 2 0
type-con $record 0
int
fun-decl $good_state 2 0
type-con $state 0
bool
fun-decl $invok_state 2 0
type-con $state 0
bool
fun-decl $has_volatile_owns_set 2 0
type-con $ctype 0
bool
fun-decl $owns_set_field 2 0
type-con $ctype 0
type-con $field 0
fun-decl $st_owner 2 0
type-con $status 0
type-con $ptr 0
fun-decl $st_closed 2 0
type-con $status 0
bool
fun-decl $st_timestamp 2 0
type-con $status 0
int
fun-decl $st_ref_cnt 2 0
type-con $status 0
int
fun-decl $owner 3 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
fun-decl $closed 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $timestamp 3 0
type-con $state 0
type-con $ptr 0
int
fun-decl $position_marker 1 0
bool
fun-decl $st 3 1
type-con $state 0
type-con $ptr 0
type-con $status 0
attribute inline 1
expr-attr
true
fun-decl $ts 3 1
type-con $state 0
type-con $ptr 0
type-con $type_state 0
attribute inline 1
expr-attr
true
fun-decl $owns 3 1
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
attribute weight 1
expr-attr
int-num 0
fun-decl $nested 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $nested_in 4 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $wrapped 4 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $irrelevant 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $mutable 3 1
type-con $state 0
type-con $ptr 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $thread_owned 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $thread_owned_or_even_mutable 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $typed 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $typed2 4 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $ptr_eq 3 1
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $ptr_neq 3 1
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_primitive_field_of 4 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $instantiate_st 2 0
type-con $status 0
bool
fun-decl $is_domain_root 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $in_wrapped_domain 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $thread_local_np 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $thread_local 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $thread_local2 4 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $dont_instantiate 2 0
type-con $ptr 0
bool
fun-decl $dont_instantiate_int 2 0
int
bool
fun-decl $dont_instantiate_state 2 0
type-con $state 0
bool
fun-decl $instantiate_int 2 0
int
bool
fun-decl $instantiate_bool 2 0
bool
bool
fun-decl $instantiate_ptr 2 0
type-con $ptr 0
bool
fun-decl $instantiate_ptrset 2 0
type-con $ptrset 0
bool
fun-decl $inv 4 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $inv2nt 4 1
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $imply_inv 4 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
fun-decl $inv2 5 0
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
fun-decl $inv2_when_closed 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $sequential 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $depends 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $spans_the_same 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $state_spans_the_same 5 0
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
fun-decl $nonvolatile_spans_the_same 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $state_nonvolatile_spans_the_same 5 0
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
bool
fun-decl $in_extent_of 4 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $in_full_extent_of 3 1
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $extent_mutable 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $extent_is_fresh 4 0
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $forall_inv2_when_closed 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $function_entry 2 0
type-con $state 0
bool
fun-decl $full_stop 2 0
type-con $state 0
bool
fun-decl $full_stop_ext 3 1
type-con $token 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $file_name_is 3 0
int
type-con $token 0
bool
fun-decl $closed_is_transitive 2 1
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $call_transition 3 0
type-con $state 0
type-con $state 0
bool
fun-decl $good_state_ext 3 0
type-con $token 0
type-con $state 0
bool
fun-decl $local_value_is 6 0
type-con $state 0
type-con $token 0
type-con $token 0
int
type-con $ctype 0
bool
fun-decl $local_value_is_ptr 6 0
type-con $state 0
type-con $token 0
type-con $token 0
type-con $ptr 0
type-con $ctype 0
bool
fun-decl $read_ptr_m 4 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
type-con $ptr 0
fun-decl $type_code_is 3 0
int
type-con $ctype 0
bool
fun-decl $function_arg_type 4 0
type-con $pure_function 0
int
type-con $ctype 0
bool
fun-decl $ver_domain 2 0
type-con $version 0
type-con $ptrset 0
fun-decl $read_version 3 1
type-con $state 0
type-con $ptr 0
type-con $version 0
attribute weight 1
expr-attr
int-num 0
fun-decl $domain 3 1
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
attribute weight 1
expr-attr
int-num 0
fun-decl $in_domain 4 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
fun-decl $in_vdomain 4 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
fun-decl $in_domain_lab 5 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $label 0
bool
fun-decl $in_vdomain_lab 5 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $label 0
bool
fun-decl $inv_lab 4 0
type-con $state 0
type-con $ptr 0
type-con $label 0
bool
fun-decl $dom_thread_local 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $fetch_from_domain 3 0
type-con $version 0
type-con $ptr 0
int
fun-decl $in_claim_domain 3 0
type-con $ptr 0
type-con $ptr 0
bool
fun-decl $by_claim 5 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $ptr 0
type-con $ptr 0
attribute weight 1
expr-attr
int-num 0
fun-decl $claim_version 2 0
type-con $ptr 0
type-con $version 0
fun-decl $read_vol_version 3 1
type-con $state 0
type-con $ptr 0
type-con $vol_version 0
attribute weight 1
expr-attr
int-num 0
fun-decl $fetch_from_vv 3 0
type-con $vol_version 0
type-con $ptr 0
int
fun-decl $fetch_vol_field 4 1
type-con $state 0
type-con $ptr 0
type-con $field 0
int
attribute inline 1
expr-attr
true
fun-decl $is_approved_by 4 0
type-con $ctype 0
type-con $field 0
type-con $field 0
bool
fun-decl $inv_is_approved_by_ptr 6 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $field 0
bool
attribute inline 1
expr-attr
true
fun-decl $inv_is_approved_by 6 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $field 0
type-con $field 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_owner_approved 3 0
type-con $ctype 0
type-con $field 0
bool
fun-decl $inv_is_owner_approved 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $field 0
bool
attribute inline 1
expr-attr
true
fun-decl $good_for_admissibility 2 0
type-con $state 0
bool
fun-decl $good_for_post_admissibility 2 0
type-con $state 0
bool
fun-decl $stuttering_pre 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $admissibility_pre 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $mutable_increases 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $meta_eq 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_stuttering_check 1 0
bool
fun-decl $is_unwrap_check 1 0
bool
fun-decl $is_admissibility_check 1 1
bool
attribute inline 1
expr-attr
true
fun-decl $good_for_pre_can_unwrap 2 0
type-con $state 0
bool
fun-decl $good_for_post_can_unwrap 2 0
type-con $state 0
bool
fun-decl $unwrap_check_pre 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $update_int 4 0
type-con $state 0
type-con $ptr 0
int
type-con $state 0
fun-decl $timestamp_is_now 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $now_writable 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $timestamp_post 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $timestamp_post_strict 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $pre_wrap 2 0
type-con $state 0
bool
fun-decl $pre_unwrap 2 0
type-con $state 0
bool
fun-decl $pre_static_wrap 2 0
type-con $state 0
bool
fun-decl $pre_static_unwrap 2 0
type-con $state 0
bool
fun-decl $unwrap_post 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $unwrap_post_claimable 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $keeps 4 2
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
attribute expand 1
expr-attr
true
fun-decl $expect_unreachable 1 0
bool
fun-decl $taken_over 4 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $status 0
fun-decl $take_over 4 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $state 0
fun-decl $released 4 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $status 0
fun-decl $release 5 0
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $state 0
fun-decl $post_unwrap 3 0
type-con $state 0
type-con $state 0
bool
fun-decl $new_ownees 4 1
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
type-con $ptrset 0
attribute inline 1
expr-attr
true
fun-decl $get_memory_allocator 1 0
type-con $ptr 0
fun-decl $memory_allocator_type 1 1
type-con $ctype 0
attribute unique 0
fun-decl $memory_allocator_ref 1 0
int
fun-decl $program_entry_point 2 0
type-con $state 0
bool
fun-decl $program_entry_point_ch 2 0
type-con $state 0
bool
fun-decl $is_global 3 1
type-con $ptr 0
type-con $ctype 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_global_array 4 1
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $active_option 3 1
type-con $state 0
type-con $ptr 0
type-con $field 0
attribute inline 1
expr-attr
true
fun-decl $ts_active_option 2 0
type-con $type_state 0
type-con $field 0
fun-decl $union_active 4 1
type-con $state 0
type-con $ptr 0
type-con $field 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_union_field 3 0
type-con $ctype 0
type-con $field 0
bool
fun-decl $union_havoced 4 1
type-con $state 0
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $full_extent 2 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $extent 3 0
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $span 2 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $in_span_of 3 1
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $first_option_typed 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $struct_extent 2 1
type-con $ptr 0
type-con $ptrset 0
attribute inline 1
expr-attr
true
fun-decl $in_struct_extent_of 3 1
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $volatile_span 3 0
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $left_split 3 0
type-con $ptr 0
int
type-con $ptr 0
fun-decl $right_split 3 0
type-con $ptr 0
int
type-con $ptr 0
fun-decl $joined_array 3 0
type-con $ptr 0
type-con $ptr 0
type-con $ptr 0
fun-decl $mutable_root 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $set_in 3 0
type-con $ptr 0
type-con $ptrset 0
bool
fun-decl $set_empty 1 0
type-con $ptrset 0
fun-decl $set_singleton 2 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $non_null_set_singleton 2 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $set_union 3 0
type-con $ptrset 0
type-con $ptrset 0
type-con $ptrset 0
fun-decl $set_difference 3 0
type-con $ptrset 0
type-con $ptrset 0
type-con $ptrset 0
fun-decl $set_intersection 3 0
type-con $ptrset 0
type-con $ptrset 0
type-con $ptrset 0
fun-decl $set_subset 3 0
type-con $ptrset 0
type-con $ptrset 0
bool
fun-decl $set_eq 3 0
type-con $ptrset 0
type-con $ptrset 0
bool
fun-decl $set_cardinality 2 0
type-con $ptrset 0
int
fun-decl $set_universe 1 0
type-con $ptrset 0
fun-decl $set_disjoint 3 0
type-con $ptrset 0
type-con $ptrset 0
bool
fun-decl $id_set_disjoint 4 0
type-con $ptr 0
type-con $ptrset 0
type-con $ptrset 0
int
fun-decl $set_in3 3 0
type-con $ptr 0
type-con $ptrset 0
bool
fun-decl $set_in2 3 0
type-con $ptr 0
type-con $ptrset 0
bool
fun-decl $in_some_owns 2 0
type-con $ptr 0
bool
fun-decl $set_in0 3 0
type-con $ptr 0
type-con $ptrset 0
bool
fun-decl sk_hack 2 0
bool
bool
fun-decl $writes_nothing 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $array 3 0
type-con $ctype 0
int
type-con $ctype 0
fun-decl $element_type 2 0
type-con $ctype 0
type-con $ctype 0
fun-decl $array_length 2 0
type-con $ctype 0
int
fun-decl $is_array_elt 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $inlined_array 3 1
type-con $ptr 0
type-con $ctype 0
type-con $ptr 0
attribute weight 1
expr-attr
int-num 0
fun-decl $idx 4 0
type-con $ptr 0
int
type-con $ctype 0
type-con $ptr 0
fun-decl $add.mul 4 2
int
int
int
int
attribute inline 1
expr-attr
true
attribute expand 1
expr-attr
true
fun-decl $add 3 2
int
int
int
attribute inline 1
expr-attr
true
attribute expand 1
expr-attr
true
fun-decl $is_array_vol_or_nonvol 6 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
bool
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $is_array 5 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $is_thread_local_array 5 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $is_mutable_array 5 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $is_array_emb 6 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $is_array_emb_path 8 1
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
type-con $ptr 0
type-con $field 0
bool
bool
attribute inline 1
expr-attr
true
fun-decl $array_field_properties 6 1
type-con $field 0
type-con $ctype 0
int
bool
bool
bool
attribute inline 1
expr-attr
true
fun-decl $no_inline_array_field_properties 6 1
type-con $field 0
type-con $ctype 0
int
bool
bool
bool
attribute inline 1
expr-attr
true
fun-decl $array_elt_emb 4 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $array_members 4 0
type-con $ptr 0
type-con $ctype 0
int
type-con $ptrset 0
fun-decl $array_range 4 0
type-con $ptr 0
type-con $ctype 0
int
type-con $ptrset 0
fun-decl $non_null_array_range 4 0
type-con $ptr 0
type-con $ctype 0
int
type-con $ptrset 0
fun-decl $non_null_extent 3 0
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
fun-decl $as_array 4 1
type-con $ptr 0
type-con $ctype 0
int
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $array_eq 6 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $index_within 3 0
type-con $ptr 0
type-con $ptr 0
int
fun-decl $in_array 5 1
type-con $ptr 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_array_full_extent_of 5 1
type-con $ptr 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_array_extent_of 6 1
type-con $state 0
type-con $ptr 0
type-con $ptr 0
type-con $ctype 0
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range 4 1
int
int
int
bool
attribute inline 1
expr-attr
true
fun-decl $bool_to_int 2 1
bool
int
attribute inline 1
expr-attr
true
fun-decl $int_to_bool 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $read_bool 3 1
type-con $state 0
type-con $ptr 0
bool
attribute inline 1
expr-attr
true
fun-decl $ite.int 4 3
bool
int
int
int
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $ite.bool 4 3
bool
bool
bool
bool
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $ite.ptr 4 3
bool
type-con $ptr 0
type-con $ptr 0
type-con $ptr 0
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $ite.struct 4 3
bool
type-con $struct 0
type-con $struct 0
type-con $struct 0
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $ite.ptrset 4 3
bool
type-con $ptrset 0
type-con $ptrset 0
type-con $ptrset 0
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $ite.primitive 4 3
bool
type-con $primitive 0
type-con $primitive 0
type-con $primitive 0
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $ite.record 4 3
bool
type-con $record 0
type-con $record 0
type-con $record 0
attribute external 1
string-attr ITE
attribute bvz 1
string-attr ITE
attribute bvint 1
string-attr ITE
fun-decl $bool_id 2 1
bool
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $min.i1 1 0
int
fun-decl $max.i1 1 0
int
fun-decl $min.i2 1 0
int
fun-decl $max.i2 1 0
int
fun-decl $min.i4 1 0
int
fun-decl $max.i4 1 0
int
fun-decl $min.i8 1 0
int
fun-decl $max.i8 1 0
int
fun-decl $max.u1 1 0
int
fun-decl $max.u2 1 0
int
fun-decl $max.u4 1 0
int
fun-decl $max.u8 1 0
int
fun-decl $in_range_i1 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_i2 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_i4 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_i8 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_u1 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_u2 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_u4 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_u8 2 1
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_div_i1 3 1
int
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_div_i2 3 1
int
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_div_i4 3 1
int
int
bool
attribute inline 1
expr-attr
true
fun-decl $in_range_div_i8 3 1
int
int
bool
attribute inline 1
expr-attr
true
fun-decl $read_i1 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_i2 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_i4 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_i8 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_u1 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_u2 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_u4 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $read_u8 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $ptr_to_u8 2 0
type-con $ptr 0
int
fun-decl $ptr_to_i8 2 0
type-con $ptr 0
int
fun-decl $ptr_to_u4 2 0
type-con $ptr 0
int
fun-decl $ptr_to_i4 2 0
type-con $ptr 0
int
fun-decl $u8_to_ptr 2 1
int
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $i8_to_ptr 2 1
int
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $u4_to_ptr 2 1
int
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $i4_to_ptr 2 1
int
type-con $ptr 0
attribute inline 1
expr-attr
true
fun-decl $byte_ptr_subtraction 3 1
type-con $ptr 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $_pow2 2 0
int
int
fun-decl $_or 4 0
type-con $ctype 0
int
int
int
fun-decl $_xor 4 0
type-con $ctype 0
int
int
int
fun-decl $_and 4 0
type-con $ctype 0
int
int
int
fun-decl $_not 3 0
type-con $ctype 0
int
int
fun-decl $unchk_add 4 1
type-con $ctype 0
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $unchk_sub 4 1
type-con $ctype 0
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $unchk_mul 4 1
type-con $ctype 0
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $unchk_div 4 1
type-con $ctype 0
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $unchk_mod 4 1
type-con $ctype 0
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $_shl 4 1
type-con $ctype 0
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $_shr 3 1
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $bv_extract_signed 5 0
int
int
int
int
int
fun-decl $bv_extract_unsigned 5 0
int
int
int
int
int
fun-decl $bv_update 6 0
int
int
int
int
int
int
fun-decl $unchecked 3 0
type-con $ctype 0
int
int
fun-decl $in_range_t 3 0
type-con $ctype 0
int
bool
fun-decl $_mul 3 1
int
int
int
attribute weight 1
expr-attr
int-num 0
fun-decl $get_string_literal 3 0
int
int
type-con $ptr 0
fun-decl $get_fnptr 3 0
int
type-con $ctype 0
type-con $ptr 0
fun-decl $get_fnptr_ref 2 0
int
int
fun-decl $get_fnptr_inv 2 0
int
int
fun-decl $is_fnptr_type 2 0
type-con $ctype 0
bool
fun-decl $is_math_type 2 0
type-con $ctype 0
bool
fun-decl $claims_obj 3 0
type-con $ptr 0
type-con $ptr 0
bool
fun-decl $valid_claim 3 0
type-con $state 0
type-con $ptr 0
bool
fun-decl $claim_initial_assumptions 4 1
type-con $state 0
type-con $ptr 0
type-con $token 0
bool
attribute inline 1
expr-attr
true
fun-decl $claim_transitivity_assumptions 5 1
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $token 0
bool
attribute inline 1
expr-attr
true
fun-decl $valid_claim_impl 3 1
type-con $state 0
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $claims_claim 3 0
type-con $ptr 0
type-con $ptr 0
bool
fun-decl $not_shared 3 1
type-con $state 0
type-con $ptr 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $claimed_closed 3 1
type-con $state 0
type-con $ptr 0
bool
attribute weight 1
expr-attr
int-num 0
fun-decl $no_claim 1 1
type-con $ptr 0
attribute unique 0
fun-decl $ref_cnt 3 1
type-con $state 0
type-con $ptr 0
int
attribute weight 1
expr-attr
int-num 0
fun-decl $is_claimable 2 0
type-con $ctype 0
bool
fun-decl $is_thread_local_storage 2 0
type-con $ctype 0
bool
fun-decl $frame_level 2 0
type-con $pure_function 0
int
fun-decl $current_frame_level 1 0
int
fun-decl $can_use_all_frame_axioms 2 1
type-con $state 0
bool
attribute inline 1
expr-attr
true
fun-decl $can_use_frame_axiom_of 2 1
type-con $pure_function 0
bool
attribute inline 1
expr-attr
true
fun-decl $reads_check_pre 2 0
type-con $state 0
bool
fun-decl $reads_check_post 2 0
type-con $state 0
bool
fun-decl $start_here 1 0
bool
fun-decl $ptrset_to_int 2 0
type-con $ptrset 0
int
fun-decl $int_to_ptrset 2 0
int
type-con $ptrset 0
fun-decl $version_to_int 2 0
type-con $version 0
int
fun-decl $int_to_version 2 0
int
type-con $version 0
fun-decl $vol_version_to_int 2 0
type-con $vol_version 0
int
fun-decl $int_to_vol_version 2 0
int
type-con $vol_version 0
fun-decl $ptr_to_int 2 0
type-con $ptr 0
int
fun-decl $int_to_ptr 2 0
int
type-con $ptr 0
fun-decl $precise_test 2 0
type-con $ptr 0
bool
fun-decl $updated_only_values 4 0
type-con $state 0
type-con $state 0
type-con $ptrset 0
bool
fun-decl $updated_only_domains 4 0
type-con $state 0
type-con $state 0
type-con $ptrset 0
bool
fun-decl $domain_updated_at 5 0
type-con $state 0
type-con $state 0
type-con $ptr 0
type-con $ptrset 0
bool
fun-decl l#public 1 1
type-con $label 0
attribute unique 0
fun-decl #tok$1^16.24 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^24.47 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^23.7 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^16.3 1 1
type-con $token 0
attribute unique 0
fun-decl #loc.p 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^16.8 1 1
type-con $token 0
attribute unique 0
fun-decl #loc.witness 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^14.3 1 1
type-con $token 0
attribute unique 0
fun-decl #loc.max 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^12.3 1 1
type-con $token 0
attribute unique 0
fun-decl #loc.len 1 1
type-con $token 0
attribute unique 0
fun-decl #distTp1 1 1
type-con $ctype 0
attribute unique 0
fun-decl #loc.arr 1 1
type-con $token 0
attribute unique 0
fun-decl #tok$1^6.1 1 1
type-con $token 0
attribute unique 0
fun-decl #file^Z?3A?5CC?5Cmax.c 1 1
type-con $token 0
attribute unique 0
axiom 0
=
fun $sizeof 1
fun ^^i1 0
int-num 1
axiom 0
=
fun $sizeof 1
fun ^^i2 0
int-num 2
axiom 0
=
fun $sizeof 1
fun ^^i4 0
int-num 4
axiom 0
=
fun $sizeof 1
fun ^^i8 0
int-num 8
axiom 0
=
fun $sizeof 1
fun ^^u1 0
int-num 1
axiom 0
=
fun $sizeof 1
fun ^^u2 0
int-num 2
axiom 0
=
fun $sizeof 1
fun ^^u4 0
int-num 4
axiom 0
=
fun $sizeof 1
fun ^^u8 0
int-num 8
axiom 0
=
fun $sizeof 1
fun ^^f4 0
int-num 4
axiom 0
=
fun $sizeof 1
fun ^^f8 0
int-num 8
axiom 0
=
fun $sizeof 1
fun ^$#thread_id_t 0
int-num 1
axiom 0
=
fun $sizeof 1
fun ^$#ptrset 0
int-num 1
axiom 0
=
fun $ptr_level 1
fun ^^i1 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^i2 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^i4 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^i8 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^u1 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^u2 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^u4 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^u8 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^f4 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^f8 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^mathint 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^bool 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^void 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^claim 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^^root_emb 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^$#ptrset 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^$#thread_id_t 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^$#state_t 0
int-num 0
axiom 0
=
fun $ptr_level 1
fun ^$#struct 0
int-num 0
axiom 0
fun $is_composite 1
fun ^^claim 0
axiom 0
fun $is_composite 1
fun ^^root_emb 0
axiom 0
forall 1 1 3
var #n
type-con $ctype 0
pat 1
fun $ptr_to 1
var #n
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.145:15
attribute uniqueId 1
string-attr 4
attribute bvZ3Native 1
string-attr False
=
fun $unptr_to 1
fun $ptr_to 1
var #n
type-con $ctype 0
var #n
type-con $ctype 0
axiom 0
forall 1 1 3
var #n
type-con $ctype 0
pat 1
fun $ptr_to 1
var #n
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.146:15
attribute uniqueId 1
string-attr 5
attribute bvZ3Native 1
string-attr False
=
fun $sizeof 1
fun $ptr_to 1
var #n
type-con $ctype 0
int-num 8
axiom 0
forall 2 1 3
var #r
type-con $ctype 0
var #d
type-con $ctype 0
pat 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.152:15
attribute uniqueId 1
string-attr 6
attribute bvZ3Native 1
string-attr False
=
fun $map_domain 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
var #d
type-con $ctype 0
axiom 0
forall 2 1 3
var #r
type-con $ctype 0
var #d
type-con $ctype 0
pat 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.153:15
attribute uniqueId 1
string-attr 7
attribute bvZ3Native 1
string-attr False
=
fun $map_range 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
var #r
type-con $ctype 0
axiom 0
forall 1 1 3
var #n
type-con $ctype 0
pat 1
fun $ptr_to 1
var #n
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.158:15
attribute uniqueId 1
string-attr 8
attribute bvZ3Native 1
string-attr False
=
fun $ptr_level 1
fun $ptr_to 1
var #n
type-con $ctype 0
+
fun $ptr_level 1
var #n
type-con $ctype 0
int-num 17
axiom 0
forall 2 1 3
var #r
type-con $ctype 0
var #d
type-con $ctype 0
pat 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.159:15
attribute uniqueId 1
string-attr 9
attribute bvZ3Native 1
string-attr False
=
fun $ptr_level 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
+
fun $ptr_level 1
var #r
type-con $ctype 0
int-num 23
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_primitive 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.167:36
attribute uniqueId 1
string-attr 10
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $is_primitive 1
var t
type-con $ctype 0
=
fun $kind_of 1
var t
type-con $ctype 0
fun $kind_primitive 0
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_composite 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.173:36
attribute uniqueId 1
string-attr 11
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $is_composite 1
var t
type-con $ctype 0
=
fun $kind_of 1
var t
type-con $ctype 0
fun $kind_composite 0
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_arraytype 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.179:36
attribute uniqueId 1
string-attr 12
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $is_arraytype 1
var t
type-con $ctype 0
=
fun $kind_of 1
var t
type-con $ctype 0
fun $kind_array 0
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_threadtype 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.185:37
attribute uniqueId 1
string-attr 13
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $is_threadtype 1
var t
type-con $ctype 0
=
fun $kind_of 1
var t
type-con $ctype 0
fun $kind_thread 0
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_composite 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.198:15
attribute uniqueId 1
string-attr 14
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
implies
fun $is_composite 1
var t
type-con $ctype 0
fun $is_non_primitive 1
var t
type-con $ctype 0
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_arraytype 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.199:15
attribute uniqueId 1
string-attr 15
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
implies
fun $is_arraytype 1
var t
type-con $ctype 0
fun $is_non_primitive 1
var t
type-con $ctype 0
axiom 0
forall 1 1 4
var t
type-con $ctype 0
pat 1
fun $is_threadtype 1
var t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.200:15
attribute uniqueId 1
string-attr 16
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
implies
fun $is_threadtype 1
var t
type-con $ctype 0
fun $is_non_primitive 1
var t
type-con $ctype 0
axiom 0
forall 2 1 3
var #r
type-con $ctype 0
var #d
type-con $ctype 0
pat 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.208:15
attribute uniqueId 1
string-attr 17
attribute bvZ3Native 1
string-attr False
fun $is_primitive 1
fun $map_t 2
var #r
type-con $ctype 0
var #d
type-con $ctype 0
axiom 0
forall 1 1 3
var #n
type-con $ctype 0
pat 1
fun $ptr_to 1
var #n
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.209:15
attribute uniqueId 1
string-attr 18
attribute bvZ3Native 1
string-attr False
fun $is_primitive 1
fun $ptr_to 1
var #n
type-con $ctype 0
axiom 0
forall 1 1 3
var #n
type-con $ctype 0
pat 1
fun $is_primitive 1
var #n
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.210:15
attribute uniqueId 1
string-attr 19
attribute bvZ3Native 1
string-attr False
implies
fun $is_primitive 1
var #n
type-con $ctype 0
not
fun $is_claimable 1
var #n
type-con $ctype 0
axiom 0
fun $is_primitive 1
fun ^^void 0
axiom 0
fun $is_primitive 1
fun ^^bool 0
axiom 0
fun $is_primitive 1
fun ^^mathint 0
axiom 0
fun $is_primitive 1
fun ^$#ptrset 0
axiom 0
fun $is_primitive 1
fun ^$#state_t 0
axiom 0
fun $is_threadtype 1
fun ^$#thread_id_t 0
axiom 0
fun $is_primitive 1
fun ^^i1 0
axiom 0
fun $is_primitive 1
fun ^^i2 0
axiom 0
fun $is_primitive 1
fun ^^i4 0
axiom 0
fun $is_primitive 1
fun ^^i8 0
axiom 0
fun $is_primitive 1
fun ^^u1 0
axiom 0
fun $is_primitive 1
fun ^^u2 0
axiom 0
fun $is_primitive 1
fun ^^u4 0
axiom 0
fun $is_primitive 1
fun ^^u8 0
axiom 0
fun $is_primitive 1
fun ^^f4 0
axiom 0
fun $is_primitive 1
fun ^^f8 0
axiom 0
=
fun $me 0
fun $ptr 2
fun ^$#thread_id_t 0
fun $me_ref 0
axiom 0
forall 3 0 4
var M
type-con $memory_t 0
var p
type-con $ptr 0
var v
int
attribute qid 1
string-attr VccPrelu.238:15
attribute uniqueId 1
string-attr 20
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $select.mem 2
fun $store.mem 3
var M
type-con $memory_t 0
var p
type-con $ptr 0
var v
int
var p
type-con $ptr 0
var v
int
axiom 0
forall 4 0 4
var M
type-con $memory_t 0
var p
type-con $ptr 0
var q
type-con $ptr 0
var v
int
attribute qid 1
string-attr VccPrelu.240:15
attribute uniqueId 1
string-attr 21
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
or 2
=
var p
type-con $ptr 0
var q
type-con $ptr 0
=
fun $select.mem 2
fun $store.mem 3
var M
type-con $memory_t 0
var p
type-con $ptr 0
var v
int
var q
type-con $ptr 0
fun $select.mem 2
var M
type-con $memory_t 0
var q
type-con $ptr 0
axiom 0
forall 3 0 4
var M
type-con $typemap_t 0
var p
type-con $ptr 0
var v
type-con $type_state 0
attribute qid 1
string-attr VccPrelu.249:15
attribute uniqueId 1
string-attr 22
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $select.tm 2
fun $store.tm 3
var M
type-con $typemap_t 0
var p
type-con $ptr 0
var v
type-con $type_state 0
var p
type-con $ptr 0
var v
type-con $type_state 0
axiom 0
forall 4 0 4
var M
type-con $typemap_t 0
var p
type-con $ptr 0
var q
type-con $ptr 0
var v
type-con $type_state 0
attribute qid 1
string-attr VccPrelu.251:15
attribute uniqueId 1
string-attr 23
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
or 2
=
var p
type-con $ptr 0
var q
type-con $ptr 0
=
fun $select.tm 2
fun $store.tm 3
var M
type-con $typemap_t 0
var p
type-con $ptr 0
var v
type-con $type_state 0
var q
type-con $ptr 0
fun $select.tm 2
var M
type-con $typemap_t 0
var q
type-con $ptr 0
axiom 0
forall 3 0 4
var M
type-con $statusmap_t 0
var p
type-con $ptr 0
var v
type-con $status 0
attribute qid 1
string-attr VccPrelu.260:15
attribute uniqueId 1
string-attr 24
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $select.sm 2
fun $store.sm 3
var M
type-con $statusmap_t 0
var p
type-con $ptr 0
var v
type-con $status 0
var p
type-con $ptr 0
var v
type-con $status 0
axiom 0
forall 4 0 4
var M
type-con $statusmap_t 0
var p
type-con $ptr 0
var q
type-con $ptr 0
var v
type-con $status 0
attribute qid 1
string-attr VccPrelu.262:15
attribute uniqueId 1
string-attr 25
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
or 2
=
var p
type-con $ptr 0
var q
type-con $ptr 0
=
fun $select.sm 2
fun $store.sm 3
var M
type-con $statusmap_t 0
var p
type-con $ptr 0
var v
type-con $status 0
var q
type-con $ptr 0
fun $select.sm 2
var M
type-con $statusmap_t 0
var q
type-con $ptr 0
axiom 0
forall 3 1 3
var p
type-con $ptr 0
var q
type-con $ptr 0
var r
type-con $ptr 0
pat 2
fun $extent_hint 2
var p
type-con $ptr 0
var q
type-con $ptr 0
fun $extent_hint 2
var q
type-con $ptr 0
var r
type-con $ptr 0
attribute qid 1
string-attr VccPrelu.288:15
attribute uniqueId 1
string-attr 26
attribute bvZ3Native 1
string-attr False
implies
and 2
fun $extent_hint 2
var p
type-con $ptr 0
var q
type-con $ptr 0
fun $extent_hint 2
var q
type-con $ptr 0
var r
type-con $ptr 0
fun $extent_hint 2
var p
type-con $ptr 0
var r
type-con $ptr 0
axiom 0
forall 1 1 3
var p
type-con $ptr 0
pat 1
fun $typ 1
var p
type-con $ptr 0
attribute qid 1
string-attr VccPrelu.290:15
attribute uniqueId 1
string-attr 27
attribute bvZ3Native 1
string-attr False
fun $extent_hint 2
var p
type-con $ptr 0
var p
type-con $ptr 0
axiom 0
forall 4 1 3
var t
type-con $ctype 0
var s
type-con $ctype 0
var min
int
var max
int
pat 1
fun $is_nested_range 4
var t
type-con $ctype 0
var s
type-con $ctype 0
var min
int
var max
int
attribute qid 1
string-attr VccPrelu.297:27
attribute uniqueId 1
string-attr 28
attribute bvZ3Native 1
string-attr False
=
fun $is_nested_range 4
var t
type-con $ctype 0
var s
type-con $ctype 0
var min
int
var max
int
and 3
fun $is_nested 2
var t
type-con $ctype 0
var s
type-con $ctype 0
=
fun $nesting_min 2
var t
type-con $ctype 0
var s
type-con $ctype 0
var min
int
=
fun $nesting_max 2
var t
type-con $ctype 0
var s
type-con $ctype 0
var max
int
axiom 0
forall 2 0 4
var #t
type-con $ctype 0
var #b
int
attribute qid 1
string-attr VccPrelu.334:15
attribute uniqueId 1
string-attr 29
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $typ 1
fun $ptr 2
var #t
type-con $ctype 0
var #b
int
var #t
type-con $ctype 0
axiom 0
forall 2 0 4
var #t
type-con $ctype 0
var #b
int
attribute qid 1
string-attr VccPrelu.335:15
attribute uniqueId 1
string-attr 30
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $ref 1
fun $ptr 2
var #t
type-con $ctype 0
var #b
int
var #b
int
axiom 0
forall 2 1 4
var p
type-con $ptr 0
var f
type-con $field 0
pat 1
fun $ghost_ref 2
var p
type-con $ptr 0
var f
type-con $field 0
attribute qid 1
string-attr VccPrelu.344:15
attribute uniqueId 1
string-attr 31
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
and 2
=
fun $ghost_emb 1
fun $ghost_ref 2
var p
type-con $ptr 0
var f
type-con $field 0
var p
type-con $ptr 0
=
fun $ghost_path 1
fun $ghost_ref 2
var p
type-con $ptr 0
var f
type-con $field 0
var f
type-con $field 0
axiom 0
forall 2 1 4
var fld
type-con $field 0
var off
int
pat 1
fun $array_path 2
var fld
type-con $field 0
var off
int
attribute qid 1
string-attr VccPrelu.355:15
attribute uniqueId 1
string-attr 32
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
and 3
not
fun $is_base_field 1
fun $array_path 2
var fld
type-con $field 0
var off
int
=
fun $array_path_1 1
fun $array_path 2
var fld
type-con $field 0
var off
int
var fld
type-con $field 0
=
fun $array_path_2 1
fun $array_path 2
var fld
type-con $field 0
var off
int
var off
int
axiom 0
=
fun $null 0
fun $ptr 2
fun ^^void 0
int-num 0
axiom 0
forall 2 0 4
var #p
type-con $ptr 0
var #t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.368:15
attribute uniqueId 1
string-attr 33
attribute bvZ3Native 1
string-attr False
attribute weight 1
expr-attr
int-num 0
=
fun $is 2
var #p
type-con $ptr 0
var #t
type-con $ctype 0
=
fun $typ 1
var #p
type-con $ptr 0
var #t
type-con $ctype 0
axiom 0
forall 2 1 3
var #p
type-con $ptr 0
var #t
type-con $ctype 0
pat 1
fun $is 2
var #p
type-con $ptr 0
var #t
type-con $ctype 0
attribute qid 1
string-attr VccPrelu.370:15
attribute uniqueId 1
string-attr 34
attribute bvZ3Native 1
string-attr False
implies
fun $is 2
var #p
type-con $ptr 0
var #t
type-con $ctype 0
=
var #p
type-con $ptr 0
fun $ptr 2
var #t
type-con $ctype 0
fun $ref 1
var #p
type-con $ptr 0
axiom 0
forall 2 1 3
var r
int
var f
type-con $field 0
pat 1
fun $containing_struct 2
fun $dot 2
fun $ptr 2
fun $field_parent_type 1
var f
type-con $field 0
var r
int
var f
type-con $field 0
var f
type-con $field 0
attribute qid 1
string-attr VccPrelu.388:15
attribute uniqueId 1
string-attr 35
attribute bvZ3Native 1
string-attr False
=
fun $containing_struct 2
fun $dot 2
fun $ptr 2
fun $field_parent_type 1
var f
type-con $field 0
var r
int
var f
type-con $field 0
var f
type-con $field 0
fun $ptr 2
fun $field_parent_type 1
var f
type-con $field 0
var r
int
axiom 0
forall 2 1 3
var p
type-con $ptr 0
var f
type-con $field 0
pat 1
fun $containing_struct 2
var p
type-con $ptr 0
var f
type-con $field 0
attribute qid 1
string-attr VccPrelu.392:15
attribute uniqueId 1
string-attr 36
attribute bvZ3Native 1
string-attr False
=
fun $containing_struct 2
var p
type-con $ptr 0
var f
type-con $field 0
fun $ptr 2
fun $field_parent_type 1
var f
type-con $field 0
fun $containing_struct_ref 2
var p
type-con $ptr 0
var f
type-con $field 0
axiom 0
forall 2 1 3
var p
type-con $ptr 0
var f
type-con $field 0
pat 1
fun $dot 2
fun $containing_struct 2
var p
type-con $ptr 0
var f
type-con $field 0
var f
type-con $field 0
attribute qid 1
string-attr VccPrelu.396:15
attribute uniqueId 1
string-attr 37
attribute bvZ3Native 1
string-attr False
implies
>=
fun $field_offset 1
var f
type-con $field 0
int-num 0
=
fun $ref 1
fun $dot 2
fun $containing_struct 2
var p
type-con $ptr 0
var f
type-con $field 0
var f
type-con $field 0
fun $ref 1
var p
type-con $ptr 0
axiom 0
forall 1 1 3
var ts
type-con $type_state 0
pat 1
fun $ts_emb 1
var ts
type-con $type_state 0
attribute qid 1
string-attr VccPrelu.427:15
attribute uniqueId 1
string-attr 38
attribute bvZ3Native 1
string-attr False
and 2
not
=
fun $kind_of 1
fun $typ 1
fun $ts_emb 1
var ts
type-con $type_state 0
fun $kind_primitive 0
fun $is_non_primitive 1
fun $typ 1
fun $ts_emb 1
var ts
type-con $type_state 0
axiom 0
forall 2 1 3
var S
type-con $state 0
var p
type-con $ptr 0
pat 2
fun $typed 2
var S
type-con $state 0
var p
type-con $ptr 0
fun $select.tm 2
fun $typemap 1
var S
type-con $state 0
fun $ts_emb 1
fun $select.tm 2
fun $typemap 1
var S
type-con $state 0
var p
type-con $ptr 0
attribute qid 1
string-attr VccPrelu.430:15
--> --------------------
--> maximum size reached
--> --------------------
[ 0.70Quellennavigators
Projekt
]
|
2026-03-28
|
|
|
|
|
