cprover
|
util More...
Go to the source code of this file.
Macros | |
#define | USE_DSTRING |
#define | IREP_ID_ONE(the_id) id_##the_id, |
#define | IREP_ID_TWO(the_id, str) id_##the_id, |
#define | IREP_ID_ONE(the_id) extern const dstringt ID_##the_id; |
#define | IREP_ID_TWO(the_id, str) extern const dstringt ID_##the_id; |
util
Definition in file irep_ids.h.
#define IREP_ID_ONE | ( | the_id | ) | id_##the_id, |
Definition at line 42 of file irep_ids.h.
#define IREP_ID_ONE | ( | the_id | ) | extern const dstringt ID_##the_id; |
Definition at line 42 of file irep_ids.h.
#define IREP_ID_TWO | ( | the_id, | |
str | |||
) | id_##the_id, |
Definition at line 43 of file irep_ids.h.
#define IREP_ID_TWO | ( | the_id, | |
str | |||
) | extern const dstringt ID_##the_id; |
Definition at line 43 of file irep_ids.h.
#define USE_DSTRING |
Definition at line 15 of file irep_ids.h.
|
strong |
Enumerator | |
---|---|
IREP_ID_ONE | |
IREP_ID_TWO | |
List | of irep id names and values. For an explanation of how this works, see irep_ids.h. |
id_empty_string | |
id_let | |
id_nil | |
id_type | |
id_operands | |
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_file | |
id_line | |
id_column | |
id_comment | |
id_property | |
id_property_class | |
id_property_id | |
id_function | |
id_code | |
id_typecast | |
id_static_cast | |
id_dynamic_cast | |
id_const_cast | |
id_reinterpret_cast | |
id_index | |
id_index_range | |
id_ptrmember | |
id_member | |
id_member_name | |
id_C_member_name | |
id_equal | |
id_implies | |
id_iff | |
id_and | |
id_nand | |
id_or | |
id_nor | |
id_xor | |
id_xnor | |
id_not | |
id_bitand | |
id_bitor | |
id_bitnot | |
id_bitxor | |
id_bitnand | |
id_bitnor | |
id_bitxnor | |
id_notequal | |
id_if | |
id_symbol | |
id_next_symbol | |
id_nondet_symbol | |
id_predicate | |
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_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_size | |
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_array | |
id_incomplete_struct | |
id_incomplete_union | |
id_incomplete_class | |
id_incomplete_c_enum | |
id_C_incomplete | |
id_identifier | |
id_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_module_instance | |
id_macromodule | |
id_primitive_module_instance | |
id_module_items | |
id_module_source | |
id_parameter_decl | |
id_local_parameter_decl | |
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_C_string_constant | |
id_string_constant | |
id_width | |
id_components | |
id_bv | |
id_f | |
id_ports | |
id_port | |
id_offset | |
id_with | |
id_trans | |
id_throw | |
id_catch | |
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_forever | |
id_repeat | |
id_extractbit | |
id_extractbits | |
id_reference | |
id_C_reference | |
id_C_rvalue_reference | |
id_true | |
id_false | |
id_address_of | |
id_dereference | |
id_C_lvalue | |
id_C_base | |
id_destination | |
id_main | |
id_expression | |
id_free | |
id_malloc | |
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_string_literal | |
id_printf | |
id_input | |
id_output | |
id_output_register | |
id_inout | |
id_nondet | |
id_NULL | |
id_null | |
id_nullptr | |
id_c_enum | |
id_enumeration | |
id_elements | |
id_unknown | |
id_uninitialized | |
id_invalid | |
id_C_invalid_object | |
id_pointer_offset | |
id_pointer_object | |
id_invalid_pointer | |
id_ieee_float_equal | |
id_ieee_float_notequal | |
id_isnan | |
id_lambda | |
id_array_of | |
id_array_equal | |
id_array_set | |
id_array_copy | |
id_mod | |
id_rem | |
id_shr | |
id_ashr | |
id_lshr | |
id_shl | |
id_rol | |
id_ror | |
id_comma | |
id_concatenation | |
id_infinity | |
id_return_type | |
id_typedef | |
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_longlong | |
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_casex | |
id_casez | |
id_case_item | |
id_C_inlined | |
id_C_hide | |
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_bv_literals | |
id_isfinite | |
id_isinf | |
id_isnormal | |
id_AG | |
id_AF | |
id_AX | |
id_EG | |
id_EF | |
id_EX | |
id_U | |
id_R | |
id_A | |
id_F | |
id_E | |
id_G | |
id_X | |
id_continuous_assign | |
id_blocking_assign | |
id_non_blocking_assign | |
id_alignof | |
id_clang_builtin_convertvector | |
id_gcc_builtin_va_arg | |
id_gcc_builtin_types_compatible_p | |
id_gcc_builtin_va_arg_next | |
id_gcc_builtin_va_list | |
id_gcc_float80 | |
id_gcc_float128 | |
id_gcc_int128 | |
id_gcc_decimal32 | |
id_gcc_decimal64 | |
id_gcc_decimal128 | |
id_builtin_offsetof | |
id_0 | |
id_1 | |
id_8 | |
id_16 | |
id_32 | |
id_64 | |
id_128 | |
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_component | |
id_pretty_name | |
id_C_class | |
id_C_interface | |
id_interface | |
id_targets | |
id_location | |
id_labels | |
id_event | |
id_guard | |
id_designated_initializer | |
id_designator | |
id_member_designator | |
id_index_designator | |
id_offset_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_dummy | |
id_init | |
id_cprover_atomic | |
id_atomic | |
id_atomic_type_specifier | |
id_atomic_begin | |
id_atomic_end | |
id_start_thread | |
id_end_thread | |
id_specc_notify | |
id_specc_par | |
id_specc_wait | |
id_specc_event | |
id_bp_enforce | |
id_bp_abortif | |
id_bp_constrain | |
id_bp_schoose | |
id_bp_dead | |
id_instance | |
id_cover | |
id_coverage_criterion | |
id_initializer | |
id_anonymous | |
id_C_is_anonymous | |
id_is_macro | |
id_is_enum_constant | |
id_is_inline | |
id_is_extern | |
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_member_initializers | |
id_member_initializer | |
id_method_qualifier | |
id_methods | |
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_parameters | |
id_C_template | |
id_C_template_arguments | |
id_typename | |
id_C | |
id_cpp | |
id_java | |
id_SpecC | |
id_SystemC | |
id_decl_block | |
id_decl_type | |
id_genvar | |
id_realtime | |
id_parameters | |
id_parameter_assignments | |
id_named_parameter_assignment | |
id_specify | |
id_pullup | |
id_pulldown | |
id_automatic | |
id_rcmos | |
id_cmos | |
id_nmos | |
id_pmos | |
id_rnmos | |
id_rpmos | |
id_wchar_t | |
id_char16_t | |
id_char32_t | |
id_size_t | |
id_ssize_t | |
id_inst | |
id_inst_builtin | |
id_always | |
id_initial | |
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_C_zero_initializer | |
id_body | |
id_entity | |
id_temporary_object | |
id_overflow_plus | |
id_overflow_minus | |
id_overflow_mult | |
id_overflow_unary_minus | |
id_object_descriptor | |
id_dynamic_object | |
id_object_size | |
id_good_pointer | |
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_list | |
id_map | |
id_set | |
id_storage | |
id_friend | |
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_vector | |
id_abstract | |
id_bit | |
id_logic | |
id_chandle | |
id_reg | |
id_wire | |
id_tri | |
id_tri1 | |
id_supply0 | |
id_wand | |
id_triand | |
id_tri0 | |
id_supply1 | |
id_wor | |
id_trior | |
id_trireg | |
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_buf | |
id_bufif0 | |
id_bufif1 | |
id_notif0 | |
id_notif1 | |
id_task | |
id_C_little_endian | |
id_C_offset | |
id_C_tag_only_declaration | |
id_struct_tag | |
id_union_tag | |
id_c_enum_tag | |
id_enum_constant | |
id_bit_select | |
id_part_select | |
id_indexed_part_select_plus | |
id_indexed_part_select_minus | |
id_generate_block | |
id_generate_assign | |
id_generate_skip | |
id_generate_case | |
id_generate_if | |
id_generate_for | |
id_delay | |
id_verilog_cycle_delay | |
id_sva_cycle_delay | |
id_sva_sequence_throughout | |
id_sva_sequence_concatenation | |
id_sva_sequence_first_match | |
id_sva_always | |
id_sva_nexttime | |
id_sva_s_nexttime | |
id_sva_eventually | |
id_sva_s_eventually | |
id_sva_until | |
id_sva_s_until | |
id_sva_until_with | |
id_sva_s_until_with | |
id_sva_overlapped_implication | |
id_sva_non_overlapped_implication | |
id_hierarchical_identifier | |
id_named_port_connection | |
id_named_block | |
id_verilog_primitive_module | |
id_verilog_module | |
id_verilog_case_equality | |
id_verilog_case_inequality | |
id_event_guard | |
id_posedge | |
id_negedge | |
id_pointer_and_address_pair | |
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_auto_object | |
id_ssa_object | |
id_ptr_object | |
id_C_c_sizeof_type | |
id_array_update | |
id_struct_update | |
id_union_update | |
id_update | |
id_float_debug1 | |
id_float_debug2 | |
id_static_assert | |
id_gcc_attribute_mode | |
id_built_in | |
id_exception_list | |
id_exception_id | |
id_priority | |
id_predicate_passive_symbol | |
id_all | |
id_when | |
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_claim | |
id_generic_selection | |
id_generic_associations | |
id_generic_association | |
id_floatbv_plus | |
id_floatbv_minus | |
id_floatbv_mult | |
id_floatbv_div | |
id_floatbv_rem | |
id_floatbv_sin | |
id_floatbv_cos | |
id_floatbv_typecast | |
id_read | |
id_write | |
id_native | |
id_final | |
id_compound_literal | |
id_custom_bv | |
id_custom_unsignedbv | |
id_custom_signedbv | |
id_custom_fixedbv | |
id_custom_floatbv | |
id_C_SSA_symbol | |
id_C_full_identifier | |
id_L0 | |
id_L1 | |
id_L2 | |
id_L1_object_identifier | |
id_already_typechecked | |
id_C_va_arg_type | |
id_smt2_symbol | |
id_VHDL | |
id_Verilog | |
id_verilog_realtime | |
id_onehot | |
id_onehot0 | |
id_verilog_star_event | |
id_verilog_attribute | |
id_time | |
id_fork | |
id_disable | |
id_wait | |
id_deassign | |
id_force | |
id_release | |
id_popcount | |
id_function_type | |
id_noreturn | |
id_C_noreturn | |
id_process | |
id_signal | |
id_weak | |
id_is_weak | |
id_C_spec_loop_invariant | |
id_C_spec_requires | |
id_C_spec_ensures | |
id_virtual_function | |
id_C_element_type | |
id_working_directory | |
id_section | |
id_msb | |
id_lsb | |
id_verilog_signed_vector | |
id_verilog_unsigned_vector | |
id_verilog_array | |
id_low | |
id_high | |
id_bswap | |
id_java_bytecode_index | |
id_java_instanceof | |
id_java_super_method_call | |
id_java_enum_static_unwind | |
id_push_catch | |
id_length_upper_bound | |
id_string_constraint | |
id_string_not_contains_constraint | |
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_int_func | |
id_cprover_string_concat_long_func | |
id_cprover_string_concat_char_func | |
id_cprover_string_concat_bool_func | |
id_cprover_string_concat_double_func | |
id_cprover_string_concat_float_func | |
id_cprover_string_concat_code_point_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_hash_code_func | |
id_cprover_string_index_of_func | |
id_cprover_string_intern_func | |
id_cprover_string_insert_func | |
id_cprover_string_insert_int_func | |
id_cprover_string_insert_long_func | |
id_cprover_string_insert_bool_func | |
id_cprover_string_insert_char_func | |
id_cprover_string_insert_float_func | |
id_cprover_string_insert_double_func | |
id_cprover_string_insert_char_array_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_data_func | |
id_cprover_string_of_int_func | |
id_cprover_string_of_int_hex_func | |
id_cprover_string_of_long_func | |
id_cprover_string_of_bool_func | |
id_cprover_string_of_float_func | |
id_cprover_string_of_double_func | |
id_cprover_string_of_char_func | |
id_cprover_string_of_char_array_func | |
id_cprover_string_parse_int_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_char_array_func | |
id_cprover_string_to_lower_case_func | |
id_cprover_string_to_upper_case_func | |
id_cprover_string_trim_func | |
id_cprover_string_value_of_func | |
id_array_replace |
Definition at line 32 of file irep_ids.h.