create_array_with_type_intrinsic.h File Reference
Implementation of CProver.createArrayWithType intrinsic. More...
#include <util/std_code_base.h>
Include dependency graph for create_array_with_type_intrinsic.h: This graph shows which files directly or indirectly include this file: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.h.
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.
