cprover
|
Jsil Language. More...
#include "jsil_entry_point.h"
#include <util/arith_tools.h>
#include <util/config.h>
#include <util/symbol_table.h>
#include <util/message.h>
#include <util/std_types.h>
#include <util/cprover_prefix.h>
#include <goto-programs/goto_functions.h>
Go to the source code of this file.
Macros | |
#define | INITIALIZE CPROVER_PREFIX "initialize" |
Functions | |
static void | create_initialize (symbol_tablet &symbol_table) |
bool | jsil_entry_point (symbol_tablet &symbol_table, message_handlert &message_handler) |
Jsil Language.
Definition in file jsil_entry_point.cpp.
#define INITIALIZE CPROVER_PREFIX "initialize" |
Definition at line 23 of file jsil_entry_point.cpp.
|
static |
Definition at line 25 of file jsil_entry_point.cpp.
References symbol_tablet::add(), code_blockt::add(), symbolt::base_name, CPROVER_PREFIX, from_integer(), namespacet::lookup(), symbolt::mode, symbolt::name, code_typet::return_type(), symbolt::type, exprt::type(), and symbolt::value.
Referenced by jsil_entry_point().
bool jsil_entry_point | ( | symbol_tablet & | symbol_table, |
message_handlert & | message_handler | ||
) |
Definition at line 52 of file jsil_entry_point.cpp.
References exprt::add_source_location(), config, CPROVER_PREFIX, create_initialize(), goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), messaget::error(), forall_symbol_base_map, code_function_callt::function(), id2string(), irept::is_nil(), code_function_callt::lhs(), symbolt::location, configt::main, irept::make_nil(), symbol_tablet::move(), exprt::move_to_operands(), symbolt::name, code_typet::return_type(), messaget::set_message_handler(), irept::swap(), symbol_tablet::symbol_base_map, symbolt::symbol_expr(), symbol_tablet::symbols, symbolt::type, and symbolt::value.
Referenced by jsil_languaget::final().