CBMC
create_array_with_type_intrinsic.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Implementation of CProver.createArrayWithType intrinsic
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
13 #define CPROVER_JAVA_BYTECODE_CREATE_ARRAY_WITH_TYPE_INTRINSIC_H
14 
15 #include <util/std_code.h>
16 
17 class message_handlert;
18 class symbol_table_baset;
19 
20 irep_idt get_create_array_with_type_name();
21 
22 codet create_array_with_type_body(
23  const irep_idt &function_id,
24  symbol_table_baset &symbol_table,
25  message_handlert &message_handler);
26 
27 #endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
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
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
message_handlert
Definition: message.h:27
std_code.h
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
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:28