Loading...

Searching...

No Matches

initialize_goto_model.cpp File Reference

Get a Goto Program. More...

#include "initialize_goto_model.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/message.h>
#include <util/options.h>
#include <util/unicode.h>
#include <goto-programs/rebuild_goto_start_function.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include <langapi/language.h>
#include <langapi/language_file.h>
#include <langapi/mode.h>
#include <linking/static_lifetime_init.h>
#include "read_goto_binary.h"
#include <fstream>

+ Include dependency graph for initialize_goto_model.cpp:

[フレーム]

Go to the source code of this file.

Functions

static bool generate_entry_point_for_function (const optionst &options, symbol_tablet &symbol_table, message_handlert &message_handler)

Generate an entry point that calls a function with the given name, based on the functions language mode in the symbol table.

void initialize_from_source_files (const std::list< std::string > &sources, const optionst &options, language_filest &language_files, symbol_tablet &symbol_table, message_handlert &message_handler)

Populate symbol_table from sources by parsing and type checking via language_files.

void set_up_custom_entry_point (language_filest &language_files, symbol_tablet &symbol_table, const std::function< std::size_t(const irep_idt &)> &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler)

Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.

goto_modelt initialize_goto_model (const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)

void update_max_malloc_size (goto_modelt &goto_model, message_handlert &message_handler)

Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.

Detailed Description

Get a Goto Program.

Definition in file initialize_goto_model.cpp.

Function Documentation

◆ generate_entry_point_for_function()

static bool generate_entry_point_for_function ( const optionst & options,

symbol_tablet & symbol_table,

message_handlert & message_handler

)

static

Generate an entry point that calls a function with the given name, based on the functions language mode in the symbol table.

Definition at line 36 of file initialize_goto_model.cpp.

◆ initialize_from_source_files()

void initialize_from_source_files ( const std::list< std::string > & sources,

const optionst & options,

language_filest & language_files,

symbol_tablet & symbol_table,

message_handlert & message_handler

)

Populate symbol_table from sources by parsing and type checking via language_files.

Throws exceptions if processing fails.

Parameters: sources Collection of input source files. No operation is performed if the collection is empty.

options Configuration options.

language_files Language parsing and type checking facilities.

[out] symbol_table Symbol table to be populated.

message_handler Message handler.

Definition at line 63 of file initialize_goto_model.cpp.

◆ initialize_goto_model()

goto_modelt initialize_goto_model ( const std::vector< std::string > & files,

message_handlert & message_handler,

const optionst & options

)

Definition at line 175 of file initialize_goto_model.cpp.

◆ set_up_custom_entry_point()

void set_up_custom_entry_point ( language_filest & language_files,

symbol_tablet & symbol_table,

const std::function< std::size_t(const irep_idt &)> & unload,

const optionst & options,

bool try_mode_lookup,

message_handlert & message_handler

)

Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.

Parameters: language_files Language parsing and type checking facilities.

symbol_table Symbol table for mode lookup and removal of an existing entry point.

unload Functor to remove an existing entry point.

options Configuration options.

try_mode_lookup Try to infer the entry point's mode from the symbol table.

message_handler Message handler.

Definition at line 114 of file initialize_goto_model.cpp.

◆ update_max_malloc_size()

void update_max_malloc_size ( goto_modelt & goto_model,

message_handlert & message_handler

)

Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.

Definition at line 243 of file initialize_goto_model.cpp.