cprover
Loading...
Searching...
No Matches
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_base.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
codet
Data structure for representing an arbitrary statement in a program.
Definition
std_code_base.h:29
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
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
jbmc
src
java_bytecode
create_array_with_type_intrinsic.h
Generated by
1.13.2