cprover
|
Implementation of CProver.createArrayWithType intrinsic. More...
#include "create_array_with_type_intrinsic.h"
#include <java_bytecode/java_types.h>
#include <util/fresh_symbol.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/symbol_table_base.h>
Go to the source code of this file.
Functions | |
irep_idt | get_create_array_with_type_name () |
Returns the symbol name for org.cprover.CProver.createArrayWithType | |
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. |
Implementation of CProver.createArrayWithType intrinsic.
Definition in file create_array_with_type_intrinsic.cpp.
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.
Our implementation copies the internal type information maintained by jbmc that tracks the runtime type of an array object rather than using reflection to achieve similar type cloning.
function_id | identifier of the function being produced. Currently always get_create_array_with_type_name() |
symbol_table | global symbol table |
message_handler | any GOTO program conversion errors are logged here |
Definition at line 41 of file create_array_with_type_intrinsic.cpp.
irep_idt get_create_array_with_type_name | ( | ) |
Returns the symbol name for org.cprover.CProver.createArrayWithType
Definition at line 23 of file create_array_with_type_intrinsic.cpp.