CBMC
util Directory Reference

Files

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