cprover
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/message.h
>
16
#include <
util/std_code.h
>
17
#include <
util/symbol_table_base.h
>
18
19
irep_idt
get_create_array_with_type_name
();
20
21
codet
create_array_with_type_body
(
22
const
irep_idt
&
function_id
,
23
symbol_table_baset
&symbol_table,
24
message_handlert
&message_handler);
25
26
#endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition:
object_factory_parameters.h:82
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:39
symbol_table_baset
The symbol table base class interface.
Definition:
symbol_table_base.h:22
message_handlert
Definition:
message.h:28
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:21
symbol_table_base.h
Author: Diffblue Ltd.
message.h
codet
Data structure for representing an arbitrary statement in a program.
Definition:
std_code.h:35
jbmc
src
java_bytecode
create_array_with_type_intrinsic.h
Generated by
1.8.20