cbmc-documentation/nondet_8h_source.html

/*******************************************************************\


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