require_type.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Unit test utilities
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
#define CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
 
#include <util/std_types.h>
#include <java_bytecode/java_types.h>
 
// NOLINTNEXTLINE(readability/namespace)
namespace require_type
{
pointer_typet
require_pointer(const typet &type, const std::optional<typet> &subtype);
 
#if defined(__GNUC__) && __GNUC__ >= 14
[[gnu::no_dangling]]
#endif
const struct_tag_typet &
require_struct_tag(const typet &type, const irep_idt &identifier = "");
 
pointer_typet require_pointer_to_tag(
  const typet &type,
  const irep_idt &identifier = irep_idt());
 
java_class_typet::componentt require_component(
  const java_class_typet &java_class_type,
  const irep_idt &component_name);
 
struct_typet::componentt require_component(
  const struct_typet &struct_type,
  const irep_idt &component_name);
 
code_typet require_code(const typet &type);
java_method_typet require_java_method(const typet &type);
 
code_typet::parametert
require_parameter(const code_typet &function_type, const irep_idt &param_name);
 
code_typet require_code(const typet &type, const size_t num_params);
java_method_typet
require_java_method(const typet &type, const size_t num_params);
 
// A mini DSL for describing an expected set of type arguments for a
// java_generic_typet
enum class type_argument_kindt
{
  Inst,
  Var
};
struct expected_type_argumentt
{
  type_argument_kindt kind;
  irep_idt description;
};
typedef std::initializer_list<expected_type_argumentt>
  expected_type_argumentst;
 
java_generic_typet require_java_generic_type(const typet &type);
 
java_generic_typet require_java_generic_type(
  const typet &type,
  const require_type::expected_type_argumentst &type_expectations);
 
java_generic_parametert require_java_generic_parameter(const typet &type);
 
java_generic_parametert require_java_generic_parameter(
  const typet &type,
  const irep_idt &parameter);
 
const typet &require_java_non_generic_type(
  const typet &type,
  const std::optional<struct_tag_typet> &expect_subtype);
 
class_typet require_complete_class(const typet &class_type);
 
class_typet require_incomplete_class(const typet &class_type);
 
java_generic_class_typet require_java_generic_class(const typet &class_type);
 
java_generic_class_typet require_java_generic_class(
  const typet &class_type,
  const std::initializer_list<irep_idt> &type_variables);
 
java_generic_class_typet
require_complete_java_generic_class(const typet &class_type);
 
java_generic_class_typet require_complete_java_generic_class(
  const typet &class_type,
  const std::initializer_list<irep_idt> &type_parameters);
 
java_implicitly_generic_class_typet
require_java_implicitly_generic_class(const typet &class_type);
 
java_implicitly_generic_class_typet require_java_implicitly_generic_class(
  const typet &class_type,
  const std::initializer_list<irep_idt> &implicit_type_variables);
 
java_implicitly_generic_class_typet
require_complete_java_implicitly_generic_class(const typet &class_type);
 
java_implicitly_generic_class_typet
require_complete_java_implicitly_generic_class(
  const typet &class_type,
  const std::initializer_list<irep_idt> &implicit_type_variables);
 
java_class_typet require_java_non_generic_class(const typet &class_type);
 
java_class_typet
require_complete_java_non_generic_class(const typet &class_type);
 
java_generic_struct_tag_typet require_java_generic_struct_tag_type(
  const typet &type,
  const std::string &identifier);
 
java_generic_struct_tag_typet require_java_generic_struct_tag_type(
  const typet &type,
  const std::string &identifier,
  const require_type::expected_type_argumentst &type_expectations);
 
typedef java_class_typet::java_lambda_method_handlest
  java_lambda_method_handlest;
 
java_lambda_method_handlest require_lambda_method_handles(
  const java_class_typet &class_type,
  const std::vector<std::string> &expected_identifiers);
}
 
#endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H