cprover
Loading...
Searching...
No Matches
irep_ids.cpp File Reference

Internal Representation. More...

#include "irep_ids.h"
#include "invariant.h"
#include "string_container.h"
#include "irep_ids.def"
+ Include dependency graph for irep_ids.cpp:

Go to the source code of this file.

Macros

#define IREP_ID_ONE(id)
 
#define IREP_ID_TWO(id, str)
 
#define IREP_ID_ONE(the_id)
 
#define IREP_ID_TWO(the_id, str)
 
#define IREP_ID_ONE(the_id)
 
#define IREP_ID_TWO(the_id, str)
 

Enumerations

enum class  idt : unsigned {
  IREP_ID_ONE , IREP_ID_TWO , /builddir/build/BUILD/cbmc-6.4.1-build/cbmc-cbmc-6.4.1/src/util/irep_ids.cpp , id_empty_string ,
  id_let , id_let_binding , id_nil , id_type ,
  id_bool , id_c_bool , id_proper_bool , id_signedbv ,
  id_unsignedbv , id_verilog_signedbv , id_verilog_unsignedbv , id_floatbv ,
  id_fixedbv , id_x86_extended , id_C_source_location , id_C_end_location ,
  id_C_is_padding , id_C_do_not_dump , id_file , id_line ,
  id_column , id_comment , id_property_class , id_property_fatal ,
  id_property_id , id_function , id_mathematical_function , id_code ,
  id_typecast , id_static_cast , id_dynamic_cast , id_const_cast ,
  id_reinterpret_cast , id_index , id_ptrmember , id_member ,
  id_member_name , id_C_member_name , id_equal , id_implies ,
  id_and , id_nand , id_or , id_nor ,
  id_xor , id_not , id_bitand , id_bitor ,
  id_bitnot , id_bitxor , id_bitnand , id_bitnor ,
  id_bitxnor , id_notequal , id_if , id_symbol ,
  id_nondet_symbol , id_predicate_symbol , id_predicate_next_symbol , id_nondet_bool ,
  id_empty , id_side_effect , id_statement , id_statement_expression ,
  id_value , id_constant , id_block , id_decl ,
  id_dead , id_assign , id_assign_div , id_assign_mult ,
  id_assign_plus , id_assign_minus , id_assign_mod , id_assign_shl ,
  id_assign_shr , id_assign_ashr , id_assign_lshr , id_assign_bitand ,
  id_assign_bitxor , id_assign_bitor , id_assume , id_assert ,
  id_assertion , id_precondition , id_postcondition , id_precondition_instance ,
  id_goto , id_gcc_computed_goto , id_ifthenelse , id_label ,
  id_break , id_continue , id_function_call , id_return ,
  id_skip , id_arguments , id_array , id_C_index_type ,
  id_size , id_frontend_pointer , id_pointer , id_block_pointer ,
  id_switch , id_switch_case , id_gcc_switch_case_range , id_for ,
  id_while , id_dowhile , id_int , id_integer ,
  id_natural , id_real , id_rational , id_complex ,
  id_signed , id_unsigned , id_asm , id_gcc_asm_input ,
  id_gcc_asm_output , id_gcc_asm_clobbered_register , id_incomplete , id_incomplete_class ,
  id_C_incomplete , id_identifier , id_name , id_inner_name ,
  id_cpp_name , id_component_cpp_name , id_C_id_class , id_declaration ,
  id_declaration_list , id_declarator , id_struct , id_c_bit_field ,
  id_union , id_class , id_merged_type , id_range ,
  id_from , id_to , id_module , id_parameter ,
  id_component_name , id_component_number , id_tag , id_default ,
  id_C_default_value , id_base_name , id_C_base_name , id_string ,
  id_is_cstring , id_C_string_constant , id_string_constant , id_cstrlen ,
  id_is_sentinel_dll , id_width , id_components , id_bv ,
  id_f , id_with , id_trans , id_throw ,
  id_try_catch , id_noexcept , id_CPROVER_throw , id_CPROVER_try_catch ,
  id_CPROVER_try_finally , id_protection , id_private , id_public ,
  id_protected , id_virtual , id_volatile , id_const ,
  id_constexpr , id_inline , id_forall , id_exists ,
  id_repeat , id_extractbit , id_extractbits , id_update_bit ,
  id_update_bits , id_zero_extend , id_C_reference , id_C_rvalue_reference ,
  id_true , id_false , id_address_of , id_object_address ,
  id_field_address , id_element_address , id_dereference , id_C_lvalue ,
  id_C_base , id_destination , id_main , id_expression ,
  id_allocate , id_reallocate , id_C_cxx_alloc_type , id_cpp_new ,
  id_cpp_delete , id_cpp_new_array , id_cpp_delete_array , id_java_new ,
  id_java_new_array , id_java_new_array_data , id_java_string_literal , id_printf ,
  id_input , id_output , id_nondet , id_NULL ,
  id_nullptr , id_c_enum , id_enum_underlying_type , id_enumeration ,
  id_elements , id_unknown , id_uninitialized , id_invalid ,
  id_C_invalid_object , id_pointer_offset , id_pointer_object , id_is_invalid_pointer ,
  id_ieee_float_equal , id_ieee_float_notequal , id_isnan , id_lambda ,
  id_named_term , id_array_comprehension , id_array_of , id_array_equal ,
  id_array_set , id_array_copy , id_array_list , id_euclidean_mod ,
  id_mod , id_shr , id_ashr , id_lshr ,
  id_shl , id_rol , id_ror , id_comma ,
  id_concatenation , id_infinity , id_return_type , id_typedef ,
  id_typedef_type , id_C_typedef , id_extern , id_static ,
  id_auto , id_register , id_thread_local , id_thread ,
  id_C_thread_local , id_C_static_lifetime , id_mutable , id_void ,
  id_int8 , id_int16 , id_int32 , id_int64 ,
  id_ptr32 , id_ptr64 , id_char , id_short ,
  id_long , id_float , id_double , id_byte ,
  id_boolean , id_long_double , id_signed_char , id_unsigned_char ,
  id_signed_int , id_unsigned_int , id_signed_long_int , id_unsigned_long_int ,
  id_signed_short_int , id_unsigned_short_int , id_signed_long_long_int , id_unsigned_long_long_int ,
  id_signed_int128 , id_unsigned_int128 , id_case , id_C_inlined ,
  id_hide , id_abs , id_sign , id_access ,
  id_C_access , id_postincrement , id_postdecrement , id_preincrement ,
  id_predecrement , id_integer_bits , id_KnR , id_C_KnR ,
  id_constraint_select_one , id_cond , id_isfinite , id_isinf ,
  id_isnormal , id_alignof , id_clang_builtin_convertvector , id_gcc_builtin_va_arg ,
  id_gcc_builtin_types_compatible_p , id_va_start , id_gcc_float16 , id_gcc_float32 ,
  id_gcc_float32x , id_gcc_float64 , id_gcc_float64x , id_gcc_float80 ,
  id_gcc_float128 , id_gcc_float128x , id_gcc_int128 , id_gcc_decimal32 ,
  id_gcc_decimal64 , id_gcc_decimal128 , id_builtin_offsetof , id_0 ,
  id_1 , id_sizeof , id_type_arg , id_expr_arg ,
  id_expression_list , id_initializer_list , id_gcc_conditional_expression , id_gcc_local_label ,
  id_gcc , id_msc , id_typeof , id_ellipsis ,
  id_flavor , id_ge , id_le , id_gt ,
  id_lt , id_plus , id_minus , id_unary_minus ,
  id_unary_plus , id_mult , id_div , id_power ,
  id_factorial_power , id_C_pretty_name , id_C_class , id_C_field ,
  id_C_interface , id_designated_initializer , id_designator , id_member_designator ,
  id_index_designator , id_C_constant , id_C_volatile , id_C_restricted ,
  id_C_identifier , id_C_implicit , id_C_ptr32 , id_C_ptr64 ,
  id_C_atomic , id_restrict , id_byte_extract_big_endian , id_byte_extract_little_endian ,
  id_byte_update_big_endian , id_byte_update_little_endian , id_replication , id_cprover_atomic ,
  id_atomic , id_atomic_type_specifier , id_atomic_begin , id_atomic_end ,
  id_start_thread , id_end_thread , id_coverage_criterion , id_initializer ,
  id_anonymous , id_C_is_anonymous , id_is_enum_constant , id_is_inline ,
  id_is_extern , id_is_synchronized , id_is_native_method , id_is_varargs_method ,
  id_is_global , id_is_thread_local , id_is_parameter , id_is_member ,
  id_is_type , id_is_register , id_is_typedef , id_is_static ,
  id_is_template , id_is_static_assert , id_is_virtual , id_C_is_virtual ,
  id_literal , id_literal_vector , id_literals , id_member_initializers ,
  id_member_initializer , id_method_qualifier , id_methods , id_static_members ,
  id_constructor , id_destructor , id_bases , id_base ,
  id_from_base , id_operator , id_template , id_template_class_instance ,
  id_template_function_instance , id_template_type , id_template_args , id_template_parameter ,
  id_template_parameter_symbol_type , id_template_parameters , id_C_template , id_C_template_arguments ,
  id_C_template_case , id_typename , id_C , id_cpp ,
  id_java , id_decl_block , id_decl_type , id_parameters ,
  id_wchar_t , id_char16_t , id_char32_t , id_size_t ,
  id_ssize_t , id_mode , id_this , id_C_this ,
  id_reduction_and , id_reduction_or , id_reduction_nand , id_reduction_nor ,
  id_reduction_xor , id_reduction_xnor , id_body , id_temporary_object ,
  id_overflow_plus , id_overflow_minus , id_overflow_mult , id_overflow_unary_minus ,
  id_object_descriptor , id_is_dynamic_object , id_dynamic_object , id_C_dynamic ,
  id_pointer_in_range , id_object_size , id_separate , id_live_object ,
  id_writeable_object , id_integer_address , id_integer_address_object , id_null_object ,
  id_static_object , id_stack_object , id_C_is_failed_symbol , id_C_failed_symbol ,
  id_friend , id_C_friends , id_explicit , id_storage_spec ,
  id_member_spec , id_msc_declspec , id_packed , id_C_packed ,
  id_transparent_union , id_C_transparent_union , id_aligned , id_C_alignment ,
  id_frontend_vector , id_vector , id_abstract , id_function_application ,
  id_cpp_declarator , id_cpp_linkage_spec , id_cpp_namespace_spec , id_cpp_storage_spec ,
  id_cpp_using , id_cpp_declaration , id_cpp_static_assert , id_cpp_member_spec ,
  id_C_c_type , id_namespace , id_linkage , id_decltype ,
  id_C_tag_only_declaration , id_struct_tag , id_union_tag , id_c_enum_tag ,
  id_verilog_case_equality , id_verilog_case_inequality , id_user_specified_predicate , id_user_specified_parameter_predicates ,
  id_user_specified_return_predicates , id_unassigned , id_new_object , id_complex_real ,
  id_complex_imag , id_imag , id_msc_try_except , id_msc_try_finally ,
  id_msc_leave , id_msc_uuidof , id_msc_if_exists , id_msc_if_not_exists ,
  id_msc_underlying_type , id_msc_based , id_alias , id_ptr_object ,
  id_C_c_sizeof_type , id_array_update , id_update , id_static_assert ,
  id_gcc_attribute_mode , id_built_in , id_exception_list , id_exception_id ,
  id_predicate_passive_symbol , id_cw_va_arg_typeof , id_fence , id_sync ,
  id_lwsync , id_isync , id_WRfence , id_RRfence ,
  id_RWfence , id_WWfence , id_RRcumul , id_RWcumul ,
  id_WWcumul , id_WRcumul , id_generic_selection , id_generic_associations ,
  id_generic_association , id_floatbv_plus , id_floatbv_minus , id_floatbv_mult ,
  id_floatbv_div , id_floatbv_mod , id_floatbv_rem , id_floatbv_typecast ,
  id_compound_literal , id_custom_bv , id_custom_unsignedbv , id_custom_signedbv ,
  id_custom_fixedbv , id_custom_floatbv , id_C_SSA_symbol , id_L0 ,
  id_L1 , id_L2 , id_L1_object_identifier , id_already_typechecked ,
  id_C_va_arg_type , id_smt2_symbol , id_onehot , id_onehot0 ,
  id_popcount , id_function_type , id_nodiscard , id_C_nodiscard ,
  id_noreturn , id_C_noreturn , id_weak , id_is_weak ,
  id_used , id_is_used , id_C_spec_loop_invariant , id_C_spec_decreases ,
  id_C_spec_requires , id_C_spec_ensures , id_C_spec_assigns , id_C_spec_frees ,
  id_target_list , id_conditional_target_group , id_virtual_function , id_element_type ,
  id_working_directory , id_section , id_bswap , id_java_bytecode_index ,
  id_java_instanceof , id_java_super_method_call , id_java_enum_static_unwind , id_push_catch ,
  id_pop_catch , id_exception_landingpad , id_length_upper_bound , id_cprover_associate_array_to_pointer_func ,
  id_cprover_associate_length_to_array_func , id_cprover_char_literal_func , id_cprover_string_literal_func , id_cprover_string_char_at_func ,
  id_cprover_string_char_set_func , id_cprover_string_code_point_at_func , id_cprover_string_code_point_before_func , id_cprover_string_code_point_count_func ,
  id_cprover_string_offset_by_code_point_func , id_cprover_string_compare_to_func , id_cprover_string_concat_func , id_cprover_string_concat_char_func ,
  id_cprover_string_concat_code_point_func , id_cprover_string_constrain_characters_func , id_cprover_string_contains_func , id_cprover_string_copy_func ,
  id_cprover_string_delete_func , id_cprover_string_delete_char_at_func , id_cprover_string_equal_func , id_cprover_string_equals_ignore_case_func ,
  id_cprover_string_empty_string_func , id_cprover_string_endswith_func , id_cprover_string_format_func , id_cprover_string_index_of_func ,
  id_cprover_string_insert_func , id_cprover_string_is_prefix_func , id_cprover_string_is_suffix_func , id_cprover_string_is_empty_func ,
  id_cprover_string_last_index_of_func , id_cprover_string_length_func , id_cprover_string_of_int_func , id_cprover_string_of_int_hex_func ,
  id_cprover_string_of_long_func , id_cprover_string_of_float_func , id_cprover_string_of_float_scientific_notation_func , id_cprover_string_of_double_func ,
  id_cprover_string_parse_int_func , id_cprover_string_is_valid_int_func , id_cprover_string_is_valid_long_func , id_cprover_string_replace_func ,
  id_cprover_string_set_length_func , id_cprover_string_startswith_func , id_cprover_string_substring_func , id_cprover_string_to_lower_case_func ,
  id_cprover_string_to_upper_case_func , id_cprover_string_trim_func , id_skip_initialize , id_basic_block_source_lines ,
  id_is_nondet_nullable , id_array_replace , id_switch_case_number , id_java_array_access ,
  id_java_member_access , id_C_java_generic_parameter , id_C_java_generics_class_type , id_C_java_implicitly_generic_class_type ,
  id_C_java_generic_symbol , id_generic_types , id_implicit_generic_types , id_type_variables ,
  id_handle_type , id_java_lambda_method_handle , id_java_lambda_method_handle_index , id_java_lambda_method_handles ,
  id_havoc_object , id_overflow_shl , id_C_no_initialization_required , id_C_no_nondet_initialization ,
  id_overlay_class , id_overlay_method , id_ignored_method , id_is_annotation ,
  id_C_annotations , id_final , id_bits_per_byte , id_C_abstract ,
  id_synthetic , id_interface , id_C_must_not_throw , id_is_inner_class ,
  id_is_anonymous , id_outer_class , id_is_bridge_method , id_C_is_operator ,
  id_C_not_accessible , id_C_override_constantness , id_C_bound , id_C_is_static ,
  id_C_call_by_value , id_C_virtual_name , id_C_unnamed_object , id_C_temporary_avoided ,
  id_C_qualifier , id_C_array_ini , id_r_ok , id_w_ok ,
  id_rw_ok , id_old , id_loop_entry , id_super_class ,
  id_exceptions_thrown_list , id_C_java_method_type , id_compiled , id_partial_specialization_args ,
  id_specialization_of , id_init_args , id_ambiguous , id_specialization_template_args ,
  id_full_template_args , id_instantiated_with , id_template_methods , id_cpp_not_typechecked ,
  id_noaccess , id_is_operator , id_is_cast_operator , id_is_explicit ,
  id_is_mutable , id_virtual_name , id_is_pure_virtual , id_is_vtptr ,
  id_prefix , id_cv , id_cpp_dummy_destructor , id_cast_expression ,
  id_pod_constructor , id_template_decls , id_throw_decl , id_typeid ,
  id_C_quoted , id_to_member , id_pointer_to_member , id_tuple ,
  id_function_body , id_get_may , id_set_may , id_clear_may ,
  id_get_must , id_set_must , id_clear_must , id_pragma ,
  id___atomic_add_fetch , id___atomic_and_fetch , id___atomic_compare_exchange , id___atomic_compare_exchange_n ,
  id___atomic_exchange , id___atomic_exchange_n , id___atomic_fetch_add , id___atomic_fetch_and ,
  id___atomic_fetch_nand , id___atomic_fetch_or , id___atomic_fetch_sub , id___atomic_fetch_xor ,
  id___atomic_load , id___atomic_load_n , id___atomic_nand_fetch , id___atomic_or_fetch ,
  id___atomic_store , id___atomic_store_n , id___atomic_sub_fetch , id___atomic_xor_fetch ,
  id___sync_add_and_fetch , id___sync_and_and_fetch , id___sync_bool_compare_and_swap , id___sync_fetch_and_add ,
  id___sync_fetch_and_and , id___sync_fetch_and_nand , id___sync_fetch_and_or , id___sync_fetch_and_sub ,
  id___sync_fetch_and_xor , id___sync_lock_release , id___sync_lock_test_and_set , id___sync_nand_and_fetch ,
  id___sync_or_and_fetch , id___sync_sub_and_fetch , id___sync_val_compare_and_swap , id___sync_xor_and_fetch ,
  id_statement_list , id_statement_list_type , id_statement_list_function , id_statement_list_function_block ,
  id_statement_list_main_function , id_statement_list_data_block , id_statement_list_version , id_statement_list_var_input ,
  id_statement_list_var_inout , id_statement_list_var_output , id_statement_list_var_constant , id_statement_list_var_temp ,
  id_statement_list_var_static , id_statement_list_return , id_statement_list_return_value_id , id_statement_list_var_entry ,
  id_statement_list_var_decls , id_statement_list_network , id_statement_list_networks , id_statement_list_title ,
  id_statement_list_identifier , id_statement_list_load , id_statement_list_transfer , id_statement_list_call ,
  id_statement_list_nop , id_statement_list_const_add , id_statement_list_accu_int_add , id_statement_list_accu_int_sub ,
  id_statement_list_accu_int_mul , id_statement_list_accu_int_div , id_statement_list_accu_int_eq , id_statement_list_accu_int_neq ,
  id_statement_list_accu_int_gt , id_statement_list_accu_int_lt , id_statement_list_accu_int_gte , id_statement_list_accu_int_lte ,
  id_statement_list_accu_real_add , id_statement_list_accu_real_sub , id_statement_list_accu_real_mul , id_statement_list_accu_real_div ,
  id_statement_list_accu_real_eq , id_statement_list_accu_real_neq , id_statement_list_accu_real_gt , id_statement_list_accu_real_lt ,
  id_statement_list_accu_real_gte , id_statement_list_accu_real_lte , id_statement_list_accu_dint_add , id_statement_list_accu_dint_sub ,
  id_statement_list_accu_dint_mul , id_statement_list_accu_dint_div , id_statement_list_accu_dint_eq , id_statement_list_accu_dint_neq ,
  id_statement_list_accu_dint_gt , id_statement_list_accu_dint_lt , id_statement_list_accu_dint_gte , id_statement_list_accu_dint_lte ,
  id_statement_list_and , id_statement_list_and_not , id_statement_list_or , id_statement_list_or_not ,
  id_statement_list_xor , id_statement_list_xor_not , id_statement_list_and_nested , id_statement_list_and_not_nested ,
  id_statement_list_or_nested , id_statement_list_or_not_nested , id_statement_list_xor_nested , id_statement_list_xor_not_nested ,
  id_statement_list_nesting_closed , id_statement_list_assign , id_statement_list_set_rlo , id_statement_list_clr_rlo ,
  id_statement_list_set , id_statement_list_reset , id_statement_list_not , id_statement_list_jump_unconditional ,
  id_statement_list_jump_conditional , id_statement_list_jump_conditional_not , id_statement_list_instruction , id_statement_list_instructions ,
  id_max_value , id_min_value , id_constant_interval , id_C_bounds_check ,
  id_count_leading_zeros , id_vector_equal , id_vector_notequal , id_vector_ge ,
  id_vector_le , id_vector_gt , id_vector_lt , id_shuffle_vector ,
  id_count_trailing_zeros , id_find_first_set , id_empty_union , id_bitreverse ,
  id_saturating_minus , id_saturating_plus , id_annotated_pointer_constant , id_C_flexible_array_member ,
  id_state , id_initial_state , id_evaluate , id_allocate_state ,
  id_reallocate_state , id_deallocate_state , id_update_state , id_enter_scope_state ,
  id_exit_scope_state , id_state_r_ok , id_state_w_ok , id_state_rw_ok ,
  id_state_type_compatible , id_state_cstrlen , id_state_is_cstring , id_state_is_dynamic_object ,
  id_state_is_sentinel_dll , id_state_live_object , id_state_writeable_object , id_state_object_size ,
  id_overflow_result_plus , id_overflow_result_minus , id_overflow_result_mult , id_overflow_result_shl ,
  id_overflow_result_unary_minus , id_field_sensitive_ssa , id_checked_assigns , id_enum_is_in_range ,
  id_prophecy_rw_ok , id_prophecy_r_ok , id_prophecy_w_ok , id_prophecy_pointer_in_range ,
  id_bit_cast
}
 

Variables

const char * irep_ids_table []
 

Detailed Description

Internal Representation.

List of irep id names and values.

For an explanation of how this works, see irep_ids.h.

Definition in file irep_ids.cpp.

Macro Definition Documentation

◆ IREP_ID_ONE [1/3]

#define IREP_ID_ONE ( id)
Value:
#id,

Definition at line 30 of file irep_ids.cpp.

◆ IREP_ID_ONE [2/3]

#define IREP_ID_ONE ( the_id)
Value:
id_##the_id,

Definition at line 30 of file irep_ids.cpp.

◆ IREP_ID_ONE [3/3]

#define IREP_ID_ONE ( the_id)
Value:
static_cast<unsigned>(idt::id_##the_id));
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
static dstringt make_from_table_index(unsigned no)
Definition dstring.h:52

Definition at line 30 of file irep_ids.cpp.

◆ IREP_ID_TWO [1/3]

#define IREP_ID_TWO ( id,
str )
Value:
#str,

Definition at line 31 of file irep_ids.cpp.

◆ IREP_ID_TWO [2/3]

#define IREP_ID_TWO ( the_id,
str )
Value:
id_##the_id,

Definition at line 31 of file irep_ids.cpp.

◆ IREP_ID_TWO [3/3]

#define IREP_ID_TWO ( the_id,
str )
Value:
static_cast<unsigned>(idt::id_##the_id));

Definition at line 31 of file irep_ids.cpp.

Enumeration Type Documentation

◆ idt

enum class idt : unsigned
strong
Enumerator
IREP_ID_ONE 
IREP_ID_TWO 
/builddir/build/BUILD/cbmc-6.4.1-build/cbmc-cbmc-6.4.1/src/util/irep_ids.cpp 

List of irep id names and values.

For an explanation of how this works, see irep_ids.h.

id_empty_string 
id_let 
id_let_binding 
id_nil 
id_type 
id_bool 
id_c_bool 
id_proper_bool 
id_signedbv 
id_unsignedbv 
id_verilog_signedbv 
id_verilog_unsignedbv 
id_floatbv 
id_fixedbv 
id_x86_extended 
id_C_source_location 
id_C_end_location 
id_C_is_padding 
id_C_do_not_dump 
id_file 
id_line 
id_column 
id_comment 
id_property_class 
id_property_fatal 
id_property_id 
id_function 
id_mathematical_function 
id_code 
id_typecast 
id_static_cast 
id_dynamic_cast 
id_const_cast 
id_reinterpret_cast 
id_index 
id_ptrmember 
id_member 
id_member_name 
id_C_member_name 
id_equal 
id_implies 
id_and 
id_nand 
id_or 
id_nor 
id_xor 
id_not 
id_bitand 
id_bitor 
id_bitnot 
id_bitxor 
id_bitnand 
id_bitnor 
id_bitxnor 
id_notequal 
id_if 
id_symbol 
id_nondet_symbol 
id_predicate_symbol 
id_predicate_next_symbol 
id_nondet_bool 
id_empty 
id_side_effect 
id_statement 
id_statement_expression 
id_value 
id_constant 
id_block 
id_decl 
id_dead 
id_assign 
id_assign_div 
id_assign_mult 
id_assign_plus 
id_assign_minus 
id_assign_mod 
id_assign_shl 
id_assign_shr 
id_assign_ashr 
id_assign_lshr 
id_assign_bitand 
id_assign_bitxor 
id_assign_bitor 
id_assume 
id_assert 
id_assertion 
id_precondition 
id_postcondition 
id_precondition_instance 
id_goto 
id_gcc_computed_goto 
id_ifthenelse 
id_label 
id_break 
id_continue 
id_function_call 
id_return 
id_skip 
id_arguments 
id_array 
id_C_index_type 
id_size 
id_frontend_pointer 
id_pointer 
id_block_pointer 
id_switch 
id_switch_case 
id_gcc_switch_case_range 
id_for 
id_while 
id_dowhile 
id_int 
id_integer 
id_natural 
id_real 
id_rational 
id_complex 
id_signed 
id_unsigned 
id_asm 
id_gcc_asm_input 
id_gcc_asm_output 
id_gcc_asm_clobbered_register 
id_incomplete 
id_incomplete_class 
id_C_incomplete 
id_identifier 
id_name 
id_inner_name 
id_cpp_name 
id_component_cpp_name 
id_C_id_class 
id_declaration 
id_declaration_list 
id_declarator 
id_struct 
id_c_bit_field 
id_union 
id_class 
id_merged_type 
id_range 
id_from 
id_to 
id_module 
id_parameter 
id_component_name 
id_component_number 
id_tag 
id_default 
id_C_default_value 
id_base_name 
id_C_base_name 
id_string 
id_is_cstring 
id_C_string_constant 
id_string_constant 
id_cstrlen 
id_is_sentinel_dll 
id_width 
id_components 
id_bv 
id_f 
id_with 
id_trans 
id_throw 
id_try_catch 
id_noexcept 
id_CPROVER_throw 
id_CPROVER_try_catch 
id_CPROVER_try_finally 
id_protection 
id_private 
id_public 
id_protected 
id_virtual 
id_volatile 
id_const 
id_constexpr 
id_inline 
id_forall 
id_exists 
id_repeat 
id_extractbit 
id_extractbits 
id_update_bit 
id_update_bits 
id_zero_extend 
id_C_reference 
id_C_rvalue_reference 
id_true 
id_false 
id_address_of 
id_object_address 
id_field_address 
id_element_address 
id_dereference 
id_C_lvalue 
id_C_base 
id_destination 
id_main 
id_expression 
id_allocate 
id_reallocate 
id_C_cxx_alloc_type 
id_cpp_new 
id_cpp_delete 
id_cpp_new_array 
id_cpp_delete_array 
id_java_new 
id_java_new_array 
id_java_new_array_data 
id_java_string_literal 
id_printf 
id_input 
id_output 
id_nondet 
id_NULL 
id_nullptr 
id_c_enum 
id_enum_underlying_type 
id_enumeration 
id_elements 
id_unknown 
id_uninitialized 
id_invalid 
id_C_invalid_object 
id_pointer_offset 
id_pointer_object 
id_is_invalid_pointer 
id_ieee_float_equal 
id_ieee_float_notequal 
id_isnan 
id_lambda 
id_named_term 
id_array_comprehension 
id_array_of 
id_array_equal 
id_array_set 
id_array_copy 
id_array_list 
id_euclidean_mod 
id_mod 
id_shr 
id_ashr 
id_lshr 
id_shl 
id_rol 
id_ror 
id_comma 
id_concatenation 
id_infinity 
id_return_type 
id_typedef 
id_typedef_type 
id_C_typedef 
id_extern 
id_static 
id_auto 
id_register 
id_thread_local 
id_thread 
id_C_thread_local 
id_C_static_lifetime 
id_mutable 
id_void 
id_int8 
id_int16 
id_int32 
id_int64 
id_ptr32 
id_ptr64 
id_char 
id_short 
id_long 
id_float 
id_double 
id_byte 
id_boolean 
id_long_double 
id_signed_char 
id_unsigned_char 
id_signed_int 
id_unsigned_int 
id_signed_long_int 
id_unsigned_long_int 
id_signed_short_int 
id_unsigned_short_int 
id_signed_long_long_int 
id_unsigned_long_long_int 
id_signed_int128 
id_unsigned_int128 
id_case 
id_C_inlined 
id_hide 
id_abs 
id_sign 
id_access 
id_C_access 
id_postincrement 
id_postdecrement 
id_preincrement 
id_predecrement 
id_integer_bits 
id_KnR 
id_C_KnR 
id_constraint_select_one 
id_cond 
id_isfinite 
id_isinf 
id_isnormal 
id_alignof 
id_clang_builtin_convertvector 
id_gcc_builtin_va_arg 
id_gcc_builtin_types_compatible_p 
id_va_start 
id_gcc_float16 
id_gcc_float32 
id_gcc_float32x 
id_gcc_float64 
id_gcc_float64x 
id_gcc_float80 
id_gcc_float128 
id_gcc_float128x 
id_gcc_int128 
id_gcc_decimal32 
id_gcc_decimal64 
id_gcc_decimal128 
id_builtin_offsetof 
id_0 
id_1 
id_sizeof 
id_type_arg 
id_expr_arg 
id_expression_list 
id_initializer_list 
id_gcc_conditional_expression 
id_gcc_local_label 
id_gcc 
id_msc 
id_typeof 
id_ellipsis 
id_flavor 
id_ge 
id_le 
id_gt 
id_lt 
id_plus 
id_minus 
id_unary_minus 
id_unary_plus 
id_mult 
id_div 
id_power 
id_factorial_power 
id_C_pretty_name 
id_C_class 
id_C_field 
id_C_interface 
id_designated_initializer 
id_designator 
id_member_designator 
id_index_designator 
id_C_constant 
id_C_volatile 
id_C_restricted 
id_C_identifier 
id_C_implicit 
id_C_ptr32 
id_C_ptr64 
id_C_atomic 
id_restrict 
id_byte_extract_big_endian 
id_byte_extract_little_endian 
id_byte_update_big_endian 
id_byte_update_little_endian 
id_replication 
id_cprover_atomic 
id_atomic 
id_atomic_type_specifier 
id_atomic_begin 
id_atomic_end 
id_start_thread 
id_end_thread 
id_coverage_criterion 
id_initializer 
id_anonymous 
id_C_is_anonymous 
id_is_enum_constant 
id_is_inline 
id_is_extern 
id_is_synchronized 
id_is_native_method 
id_is_varargs_method 
id_is_global 
id_is_thread_local 
id_is_parameter 
id_is_member 
id_is_type 
id_is_register 
id_is_typedef 
id_is_static 
id_is_template 
id_is_static_assert 
id_is_virtual 
id_C_is_virtual 
id_literal 
id_literal_vector 
id_literals 
id_member_initializers 
id_member_initializer 
id_method_qualifier 
id_methods 
id_static_members 
id_constructor 
id_destructor 
id_bases 
id_base 
id_from_base 
id_operator 
id_template 
id_template_class_instance 
id_template_function_instance 
id_template_type 
id_template_args 
id_template_parameter 
id_template_parameter_symbol_type 
id_template_parameters 
id_C_template 
id_C_template_arguments 
id_C_template_case 
id_typename 
id_C 
id_cpp 
id_java 
id_decl_block 
id_decl_type 
id_parameters 
id_wchar_t 
id_char16_t 
id_char32_t 
id_size_t 
id_ssize_t 
id_mode 
id_this 
id_C_this 
id_reduction_and 
id_reduction_or 
id_reduction_nand 
id_reduction_nor 
id_reduction_xor 
id_reduction_xnor 
id_body 
id_temporary_object 
id_overflow_plus 
id_overflow_minus 
id_overflow_mult 
id_overflow_unary_minus 
id_object_descriptor 
id_is_dynamic_object 
id_dynamic_object 
id_C_dynamic 
id_pointer_in_range 
id_object_size 
id_separate 
id_live_object 
id_writeable_object 
id_integer_address 
id_integer_address_object 
id_null_object 
id_static_object 
id_stack_object 
id_C_is_failed_symbol 
id_C_failed_symbol 
id_friend 
id_C_friends 
id_explicit 
id_storage_spec 
id_member_spec 
id_msc_declspec 
id_packed 
id_C_packed 
id_transparent_union 
id_C_transparent_union 
id_aligned 
id_C_alignment 
id_frontend_vector 
id_vector 
id_abstract 
id_function_application 
id_cpp_declarator 
id_cpp_linkage_spec 
id_cpp_namespace_spec 
id_cpp_storage_spec 
id_cpp_using 
id_cpp_declaration 
id_cpp_static_assert 
id_cpp_member_spec 
id_C_c_type 
id_namespace 
id_linkage 
id_decltype 
id_C_tag_only_declaration 
id_struct_tag 
id_union_tag 
id_c_enum_tag 
id_verilog_case_equality 
id_verilog_case_inequality 
id_user_specified_predicate 
id_user_specified_parameter_predicates 
id_user_specified_return_predicates 
id_unassigned 
id_new_object 
id_complex_real 
id_complex_imag 
id_imag 
id_msc_try_except 
id_msc_try_finally 
id_msc_leave 
id_msc_uuidof 
id_msc_if_exists 
id_msc_if_not_exists 
id_msc_underlying_type 
id_msc_based 
id_alias 
id_ptr_object 
id_C_c_sizeof_type 
id_array_update 
id_update 
id_static_assert 
id_gcc_attribute_mode 
id_built_in 
id_exception_list 
id_exception_id 
id_predicate_passive_symbol 
id_cw_va_arg_typeof 
id_fence 
id_sync 
id_lwsync 
id_isync 
id_WRfence 
id_RRfence 
id_RWfence 
id_WWfence 
id_RRcumul 
id_RWcumul 
id_WWcumul 
id_WRcumul 
id_generic_selection 
id_generic_associations 
id_generic_association 
id_floatbv_plus 
id_floatbv_minus 
id_floatbv_mult 
id_floatbv_div 
id_floatbv_mod 
id_floatbv_rem 
id_floatbv_typecast 
id_compound_literal 
id_custom_bv 
id_custom_unsignedbv 
id_custom_signedbv 
id_custom_fixedbv 
id_custom_floatbv 
id_C_SSA_symbol 
id_L0 
id_L1 
id_L2 
id_L1_object_identifier 
id_already_typechecked 
id_C_va_arg_type 
id_smt2_symbol 
id_onehot 
id_onehot0 
id_popcount 
id_function_type 
id_nodiscard 
id_C_nodiscard 
id_noreturn 
id_C_noreturn 
id_weak 
id_is_weak 
id_used 
id_is_used 
id_C_spec_loop_invariant 
id_C_spec_decreases 
id_C_spec_requires 
id_C_spec_ensures 
id_C_spec_assigns 
id_C_spec_frees 
id_target_list 
id_conditional_target_group 
id_virtual_function 
id_element_type 
id_working_directory 
id_section 
id_bswap 
id_java_bytecode_index 
id_java_instanceof 
id_java_super_method_call 
id_java_enum_static_unwind 
id_push_catch 
id_pop_catch 
id_exception_landingpad 
id_length_upper_bound 
id_cprover_associate_array_to_pointer_func 
id_cprover_associate_length_to_array_func 
id_cprover_char_literal_func 
id_cprover_string_literal_func 
id_cprover_string_char_at_func 
id_cprover_string_char_set_func 
id_cprover_string_code_point_at_func 
id_cprover_string_code_point_before_func 
id_cprover_string_code_point_count_func 
id_cprover_string_offset_by_code_point_func 
id_cprover_string_compare_to_func 
id_cprover_string_concat_func 
id_cprover_string_concat_char_func 
id_cprover_string_concat_code_point_func 
id_cprover_string_constrain_characters_func 
id_cprover_string_contains_func 
id_cprover_string_copy_func 
id_cprover_string_delete_func 
id_cprover_string_delete_char_at_func 
id_cprover_string_equal_func 
id_cprover_string_equals_ignore_case_func 
id_cprover_string_empty_string_func 
id_cprover_string_endswith_func 
id_cprover_string_format_func 
id_cprover_string_index_of_func 
id_cprover_string_insert_func 
id_cprover_string_is_prefix_func 
id_cprover_string_is_suffix_func 
id_cprover_string_is_empty_func 
id_cprover_string_last_index_of_func 
id_cprover_string_length_func 
id_cprover_string_of_int_func 
id_cprover_string_of_int_hex_func 
id_cprover_string_of_long_func 
id_cprover_string_of_float_func 
id_cprover_string_of_float_scientific_notation_func 
id_cprover_string_of_double_func 
id_cprover_string_parse_int_func 
id_cprover_string_is_valid_int_func 
id_cprover_string_is_valid_long_func 
id_cprover_string_replace_func 
id_cprover_string_set_length_func 
id_cprover_string_startswith_func 
id_cprover_string_substring_func 
id_cprover_string_to_lower_case_func 
id_cprover_string_to_upper_case_func 
id_cprover_string_trim_func 
id_skip_initialize 
id_basic_block_source_lines 
id_is_nondet_nullable 
id_array_replace 
id_switch_case_number 
id_java_array_access 
id_java_member_access 
id_C_java_generic_parameter 
id_C_java_generics_class_type 
id_C_java_implicitly_generic_class_type 
id_C_java_generic_symbol 
id_generic_types 
id_implicit_generic_types 
id_type_variables 
id_handle_type 
id_java_lambda_method_handle 
id_java_lambda_method_handle_index 
id_java_lambda_method_handles 
id_havoc_object 
id_overflow_shl 
id_C_no_initialization_required 
id_C_no_nondet_initialization 
id_overlay_class 
id_overlay_method 
id_ignored_method 
id_is_annotation 
id_C_annotations 
id_final 
id_bits_per_byte 
id_C_abstract 
id_synthetic 
id_interface 
id_C_must_not_throw 
id_is_inner_class 
id_is_anonymous 
id_outer_class 
id_is_bridge_method 
id_C_is_operator 
id_C_not_accessible 
id_C_override_constantness 
id_C_bound 
id_C_is_static 
id_C_call_by_value 
id_C_virtual_name 
id_C_unnamed_object 
id_C_temporary_avoided 
id_C_qualifier 
id_C_array_ini 
id_r_ok 
id_w_ok 
id_rw_ok 
id_old 
id_loop_entry 
id_super_class 
id_exceptions_thrown_list 
id_C_java_method_type 
id_compiled 
id_partial_specialization_args 
id_specialization_of 
id_init_args 
id_ambiguous 
id_specialization_template_args 
id_full_template_args 
id_instantiated_with 
id_template_methods 
id_cpp_not_typechecked 
id_noaccess 
id_is_operator 
id_is_cast_operator 
id_is_explicit 
id_is_mutable 
id_virtual_name 
id_is_pure_virtual 
id_is_vtptr 
id_prefix 
id_cv 
id_cpp_dummy_destructor 
id_cast_expression 
id_pod_constructor 
id_template_decls 
id_throw_decl 
id_typeid 
id_C_quoted 
id_to_member 
id_pointer_to_member 
id_tuple 
id_function_body 
id_get_may 
id_set_may 
id_clear_may 
id_get_must 
id_set_must 
id_clear_must 
id_pragma 
id___atomic_add_fetch 
id___atomic_and_fetch 
id___atomic_compare_exchange 
id___atomic_compare_exchange_n 
id___atomic_exchange 
id___atomic_exchange_n 
id___atomic_fetch_add 
id___atomic_fetch_and 
id___atomic_fetch_nand 
id___atomic_fetch_or 
id___atomic_fetch_sub 
id___atomic_fetch_xor 
id___atomic_load 
id___atomic_load_n 
id___atomic_nand_fetch 
id___atomic_or_fetch 
id___atomic_store 
id___atomic_store_n 
id___atomic_sub_fetch 
id___atomic_xor_fetch 
id___sync_add_and_fetch 
id___sync_and_and_fetch 
id___sync_bool_compare_and_swap 
id___sync_fetch_and_add 
id___sync_fetch_and_and 
id___sync_fetch_and_nand 
id___sync_fetch_and_or 
id___sync_fetch_and_sub 
id___sync_fetch_and_xor 
id___sync_lock_release 
id___sync_lock_test_and_set 
id___sync_nand_and_fetch 
id___sync_or_and_fetch 
id___sync_sub_and_fetch 
id___sync_val_compare_and_swap 
id___sync_xor_and_fetch 
id_statement_list 
id_statement_list_type 
id_statement_list_function 
id_statement_list_function_block 
id_statement_list_main_function 
id_statement_list_data_block 
id_statement_list_version 
id_statement_list_var_input 
id_statement_list_var_inout 
id_statement_list_var_output 
id_statement_list_var_constant 
id_statement_list_var_temp 
id_statement_list_var_static 
id_statement_list_return 
id_statement_list_return_value_id 
id_statement_list_var_entry 
id_statement_list_var_decls 
id_statement_list_network 
id_statement_list_networks 
id_statement_list_title 
id_statement_list_identifier 
id_statement_list_load 
id_statement_list_transfer 
id_statement_list_call 
id_statement_list_nop 
id_statement_list_const_add 
id_statement_list_accu_int_add 
id_statement_list_accu_int_sub 
id_statement_list_accu_int_mul 
id_statement_list_accu_int_div 
id_statement_list_accu_int_eq 
id_statement_list_accu_int_neq 
id_statement_list_accu_int_gt 
id_statement_list_accu_int_lt 
id_statement_list_accu_int_gte 
id_statement_list_accu_int_lte 
id_statement_list_accu_real_add 
id_statement_list_accu_real_sub 
id_statement_list_accu_real_mul 
id_statement_list_accu_real_div 
id_statement_list_accu_real_eq 
id_statement_list_accu_real_neq 
id_statement_list_accu_real_gt 
id_statement_list_accu_real_lt 
id_statement_list_accu_real_gte 
id_statement_list_accu_real_lte 
id_statement_list_accu_dint_add 
id_statement_list_accu_dint_sub 
id_statement_list_accu_dint_mul 
id_statement_list_accu_dint_div 
id_statement_list_accu_dint_eq 
id_statement_list_accu_dint_neq 
id_statement_list_accu_dint_gt 
id_statement_list_accu_dint_lt 
id_statement_list_accu_dint_gte 
id_statement_list_accu_dint_lte 
id_statement_list_and 
id_statement_list_and_not 
id_statement_list_or 
id_statement_list_or_not 
id_statement_list_xor 
id_statement_list_xor_not 
id_statement_list_and_nested 
id_statement_list_and_not_nested 
id_statement_list_or_nested 
id_statement_list_or_not_nested 
id_statement_list_xor_nested 
id_statement_list_xor_not_nested 
id_statement_list_nesting_closed 
id_statement_list_assign 
id_statement_list_set_rlo 
id_statement_list_clr_rlo 
id_statement_list_set 
id_statement_list_reset 
id_statement_list_not 
id_statement_list_jump_unconditional 
id_statement_list_jump_conditional 
id_statement_list_jump_conditional_not 
id_statement_list_instruction 
id_statement_list_instructions 
id_max_value 
id_min_value 
id_constant_interval 
id_C_bounds_check 
id_count_leading_zeros 
id_vector_equal 
id_vector_notequal 
id_vector_ge 
id_vector_le 
id_vector_gt 
id_vector_lt 
id_shuffle_vector 
id_count_trailing_zeros 
id_find_first_set 
id_empty_union 
id_bitreverse 
id_saturating_minus 
id_saturating_plus 
id_annotated_pointer_constant 
id_C_flexible_array_member 
id_state 
id_initial_state 
id_evaluate 
id_allocate_state 
id_reallocate_state 
id_deallocate_state 
id_update_state 
id_enter_scope_state 
id_exit_scope_state 
id_state_r_ok 
id_state_w_ok 
id_state_rw_ok 
id_state_type_compatible 
id_state_cstrlen 
id_state_is_cstring 
id_state_is_dynamic_object 
id_state_is_sentinel_dll 
id_state_live_object 
id_state_writeable_object 
id_state_object_size 
id_overflow_result_plus 
id_overflow_result_minus 
id_overflow_result_mult 
id_overflow_result_shl 
id_overflow_result_unary_minus 
id_field_sensitive_ssa 
id_checked_assigns 
id_enum_is_in_range 
id_prophecy_rw_ok 
id_prophecy_r_ok 
id_prophecy_w_ok 
id_prophecy_pointer_in_range 
id_bit_cast 

Definition at line 28 of file irep_ids.cpp.

Variable Documentation

◆ irep_ids_table

const char* irep_ids_table[]

Definition at line 18 of file irep_ids.cpp.