cprover
Loading...
Searching...
No Matches
util Directory Reference

Files

 
arith_tools.cpp
 
arith_tools.h
 
array_element_from_pointer.cpp
 
array_element_from_pointer.h
 
array_name.cpp
 Misc Utilities.
 
array_name.h
 Misc Utilities.
 
as_const.h
 
base_exceptions.h
 Generic exception types primarily designed for use with invariants.
 
bitvector_expr.cpp
 
bitvector_expr.h
 API to expression classes for bitvectors.
 
bitvector_types.cpp
 Pre-defined bitvector types.
 
bitvector_types.h
 Pre-defined bitvector types.
 
bv_arithmetic.cpp
 
bv_arithmetic.h
 
byte_operators.cpp
 
byte_operators.h
 Expression classes for byte-level operators.
 
c_types.cpp
 
c_types.h
 
c_types_util.h
 This file contains functions, that should support test for underlying c types, in cases where this is required for analysis purpose.
 
cmdline.cpp
 
cmdline.h
 
config.cpp
 
config.h
 
console.cpp
 
console.h
 Console.
 
constructor_of.h
 
container_utils.h
 
cout_message.cpp
 
cout_message.h
 
cow.h
 
cprover_prefix.h
 
dense_integer_map.h
 Dense integer map.
 
deprecate.h
 
dstring.cpp
 Container for C-Strings.
 
dstring.h
 Container for C-Strings.
 
edit_distance.cpp
 
edit_distance.h
 
endianness_map.cpp
 
endianness_map.h
 
exception_utils.cpp
 
exception_utils.h
 
exit_codes.h
 Document and give macros for the exit codes of CPROVER binaries.
 
expanding_vector.h
 
expr.cpp
 Expression Representation.
 
expr.h
 
expr_cast.h
 Templated functions to cast to specific exprt-derived classes.
 
expr_initializer.cpp
 Expression Initialization.
 
expr_initializer.h
 Expression Initialization.
 
expr_iterator.h
 Forward depth-first search iterators These iterators' copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
 
expr_util.cpp
 
expr_util.h
 Deprecated expression utility functions.
 
find_macros.cpp
 
find_macros.h
 
find_symbols.cpp
 
find_symbols.h
 
fixed_keys_map_wrapper.h
 A wrapper for maps that gives read-write access to elements but without allowing addition or removal of elements.
 
fixedbv.cpp
 
fixedbv.h
 
floatbv_expr.cpp
 
floatbv_expr.h
 API to expression classes for floating-point arithmetic.
 
format.h
 
format_constant.cpp
 
format_constant.h
 
format_expr.cpp
 Expression Pretty Printing.
 
format_expr.h
 
format_number_range.cpp
 Format vector of numbers into a compressed range.
 
format_number_range.h
 Format vector of numbers into a compressed range.
 
format_spec.h
 
format_type.cpp
 
format_type.h
 
forward_list_as_map.h
 
freer.h
 
fresh_symbol.cpp
 Fresh auxiliary symbol creation.
 
fresh_symbol.h
 Fresh auxiliary symbol creation.
 
get_base_name.cpp
 
get_base_name.h
 
get_module.cpp
 Find module symbol using name.
 
get_module.h
 Find module symbol using name.
 
graph.h
 A Template Class for Graphs.
 
help_formatter.cpp
 
help_formatter.h
 Help Formatter.
 
identifier.cpp
 
identifier.h
 
ieee_float.cpp
 
ieee_float.h
 
infix.h
 String infix shorthand.
 
integer_interval.h
 
interval.cpp
 
interval.h
 
interval_constraint.cpp
 
interval_constraint.h
 
interval_template.h
 
interval_union.cpp
 
interval_union.h
 Union of intervals.
 
invariant.cpp
 
invariant.h
 
invariant_utils.cpp
 Invariant helper utilities.
 
invariant_utils.h
 
irep.cpp
 Internal Representation.
 
irep.h
 
irep_hash.cpp
 irep hash functions
 
irep_hash.h
 irep hash functions
 
irep_hash_container.cpp
 Hashing IREPs.
 
irep_hash_container.h
 IREP Hash Container.
 
irep_ids.cpp
 Internal Representation.
 
irep_ids.h
 util
 
irep_serialization.cpp
 binary irep conversions with hashing
 
irep_serialization.h
 binary irep conversions with hashing
 
journalling_symbol_table.h
 Author: Diffblue Ltd.
 
json.cpp
 
json.h
 
json_irep.cpp
 Util.
 
json_irep.h
 Util.
 
json_stream.cpp
 
json_stream.h
 
lazy.h
 
lispexpr.cpp
 
lispexpr.h
 
lispirep.cpp
 
lispirep.h
 
lower_byte_operators.cpp
 
magic.h
 Magic numbers used throughout the codebase.
 
mathematical_expr.cpp
 
mathematical_expr.h
 API to expression classes for 'mathematical' expressions.
 
mathematical_types.cpp
 Mathematical types.
 
mathematical_types.h
 Mathematical types.
 
memory_info.cpp
 
memory_info.h
 
memory_units.cpp
 
memory_units.h
 
merge_irep.cpp
 
merge_irep.h
 
message.cpp
 
message.h
 
mp_arith.cpp
 
mp_arith.h
 
namespace.cpp
 Namespace.
 
namespace.h
 
narrow.h
 
nfa.h
 
nondet_bool.h
 Nondeterministic boolean helper.
 
numbering.h
 
object_factory_parameters.cpp
 
object_factory_parameters.h
 
optional_utils.h
 
options.cpp
 Options.
 
options.h
 Options.
 
parse_options.cpp
 
parse_options.h
 
parser.cpp
 
parser.h
 Parser utilities.
 
piped_process.cpp
 Subprocess communication with pipes.
 
piped_process.h
 Subprocess communication with pipes.
 
pointer_expr.cpp
 
pointer_expr.h
 API to expression classes for Pointers.
 
pointer_offset_size.cpp
 Pointer Logic.
 
pointer_offset_size.h
 Pointer Logic.
 
pointer_offset_sum.cpp
 Pointer Analysis.
 
pointer_offset_sum.h
 Pointer Dereferencing.
 
pointer_predicates.cpp
 Various predicates over pointers in programs.
 
pointer_predicates.h
 Various predicates over pointers in programs.
 
prefix.h
 
prefix_filter.cpp
 Prefix Filtering.
 
prefix_filter.h
 Prefix Filtering.
 
preprocessor.h
 Preprocessing Base Class.
 
range.h
 Ranges: pair of begin and end iterators, which can be initialized from containers, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for.
 
rational.cpp
 Rational Numbers.
 
rational.h
 
rational_tools.cpp
 Rational Numbers.
 
rational_tools.h
 
ref_expr_set.cpp
 Value Set.
 
ref_expr_set.h
 Value Set.
 
reference_counting.h
 Reference Counting.
 
refined_string_type.cpp
 Type for string expressions used by the string solver.
 
refined_string_type.h
 Type for string expressions used by the string solver.
 
rename.cpp
 
rename.h
 
rename_symbol.cpp
 
rename_symbol.h
 
replace_expr.cpp
 
replace_expr.h
 
replace_symbol.cpp
 
replace_symbol.h
 
run.cpp
 
run.h
 
sharing_map.h
 Sharing map.
 
sharing_node.h
 Sharing node.
 
signal_catcher.cpp
 
signal_catcher.h
 
simplify_expr.cpp
 
simplify_expr.h
 
simplify_expr_array.cpp
 
simplify_expr_boolean.cpp
 
simplify_expr_class.h
 
simplify_expr_floatbv.cpp
 
simplify_expr_if.cpp
 
simplify_expr_int.cpp
 
simplify_expr_pointer.cpp
 
simplify_expr_struct.cpp
 
simplify_utils.cpp
 
simplify_utils.h
 
small_map.h
 Small map.
 
small_shared_n_way_ptr.h
 
small_shared_ptr.h
 
source_location.cpp
 
source_location.h
 
sparse_vector.h
 Sparse Vectors.
 
ssa_expr.cpp
 
ssa_expr.h
 
std_code.cpp
 Data structure representing different types of statements in a program.
 
std_code.h
 
std_code_base.h
 
std_expr.cpp
 
std_expr.h
 API to expression classes.
 
std_types.cpp
 Pre-defined types.
 
std_types.h
 Pre-defined types.
 
string2int.cpp
 
string2int.h
 
string_constant.cpp
 
string_constant.h
 
string_container.cpp
 Container for C-Strings.
 
string_container.h
 Container for C-Strings.
 
string_expr.h
 String expressions for the string solver.
 
string_hash.cpp
 string hashing
 
string_hash.h
 string hashing
 
string_utils.cpp
 
string_utils.h
 
structured_data.cpp
 
structured_data.h
 
substitute_symbols.cpp
 Free Symbols.
 
substitute_symbols.h
 Symbol Substitution.
 
suffix.h
 
symbol.cpp
 
symbol.h
 Symbol table entry.
 
symbol_table.cpp
 
symbol_table.h
 Author: Diffblue Ltd.
 
symbol_table_base.cpp
 
symbol_table_base.h
 Author: Diffblue Ltd.
 
symbol_table_builder.h
 
tempdir.cpp
 
tempdir.h
 
tempfile.cpp
 
tempfile.h
 
threeval.cpp
 
threeval.h
 
timestamper.cpp
 
timestamper.h
 Emit timestamps.
 
type.cpp
 Implementations of some functions of typet.
 
type.h
 Defines typet, type_with_subtypet and type_with_subtypest.
 
typecheck.cpp
 
typecheck.h
 
ui_message.cpp
 
ui_message.h
 
unicode.cpp
 
unicode.h
 
union_find.cpp
 
union_find.h
 
union_find_replace.cpp
 
union_find_replace.h
 
validate.h
 
validate_expressions.cpp
 
validate_expressions.h
 
validate_helpers.h
 
validate_types.cpp
 
validate_types.h
 
validation_interface.h
 
validation_mode.h
 
version.h
 
xml.cpp
 
xml.h
 
xml_irep.cpp
 
xml_irep.h