nondet.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Non-deterministic object init and choice for JBMC
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#ifndef CPROVER_JAVA_BYTECODE_NONDET_H
#define CPROVER_JAVA_BYTECODE_NONDET_H
 
#include <util/std_code.h>
 
class allocate_objectst;
class symbol_table_baset;
 
using allocate_local_symbolt =
  std::function<symbol_exprt(const typet &type, std::string)>;

symbol_exprt generate_nondet_int(
  const exprt &min_value_expr,
  const exprt &max_value_expr,
  const std::string &basename_prefix,
  const source_locationt &source_location,
  allocate_objectst &allocate_objects,
  code_blockt &instructions);

symbol_exprt generate_nondet_int(
  const exprt &min_value_expr,
  const exprt &max_value_expr,
  const std::string &basename_prefix,
  const source_locationt &source_location,
  const allocate_local_symbolt &alocate_local_symbol,
  code_blockt &instructions);

symbol_exprt generate_nondet_int(
  const mp_integer &min_value,
  const mp_integer &max_value,
  const std::string &basename_prefix,
  const typet &int_type,
  const source_locationt &source_location,
  allocate_objectst &allocate_objects,
  code_blockt &instructions);
 
typedef std::vector<codet> alternate_casest;

code_blockt generate_nondet_switch(
  const irep_idt &name_prefix,
  const alternate_casest &switch_cases,
  const typet &int_type,
  const irep_idt &mode,
  const source_locationt &source_location,
  symbol_table_baset &symbol_table);
 
#endif // CPROVER_JAVA_BYTECODE_NONDET_H