create_array_with_type_intrinsic.cpp File Reference

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>

Include dependency graph for create_array_with_type_intrinsic.cpp:

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 More...
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. More...

Detailed Description

Implementation of CProver.createArrayWithType intrinsic.

Definition in file create_array_with_type_intrinsic.cpp.

Function Documentation

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.

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.

Parameters

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

Returns

new GOTO program body for org.cprover.CProver.createArrayWithType.

Definition at line 41 of file create_array_with_type_intrinsic.cpp.

get_create_array_with_type_name()

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.