cbmc/create__array__with__type__intrinsic_8h_source.html

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


Module: Implementation of CProver.createArrayWithType intrinsic


Author: Diffblue Ltd.


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


#ifndef CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H

#define CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H


#include <util/std_code_base.h>


class message_handlert;

class symbol_table_baset;


irep_idt get_create_array_with_type_name();


codet create_array_with_type_body(

  const irep_idt &function_id,

  symbol_table_baset &symbol_table,

  message_handlert &message_handler);


#endif

codet
Data structure for representing an arbitrary statement in a program.
Definition std_code_base.h:29

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38

message_handlert
Definition message.h:27

symbol_table_baset
The symbol table base class interface.
Definition symbol_table_base.h:23

get_create_array_with_type_name
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType
Definition create_array_with_type_intrinsic.cpp:23

create_array_with_type_body
codet create_array_with_type_body(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Returns the internal implementation for org.cprover.CProver.createArrayWithType.
Definition create_array_with_type_intrinsic.cpp:41

std_code_base.h