Modify/add symbol table lookup and get_writeable
This commit is contained in:
parent
d19e7378b1
commit
a9ba0f90aa
|
@ -182,6 +182,11 @@ Here a few minimalistic coding rules for the CPROVER source tree.
|
|||
- Avoid `assert`. If the condition is an actual invariant, use INVARIANT,
|
||||
PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If
|
||||
there are possible reasons why it might fail, throw an exception.
|
||||
- All raw pointers (such as those returned by `symbol_tablet::lookup`) are
|
||||
assumed to be non-owning, and should not be `delete`d. Raw pointers that
|
||||
point to heap-allocated memory should be private data members of an object
|
||||
which safely manages the pointer. As such, `new` should only be used in
|
||||
constructors, and `delete` in destructors. Never use `malloc` or `free`.
|
||||
|
||||
# Architecture-specific code
|
||||
- Avoid if possible.
|
||||
|
|
|
@ -208,7 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
|
|||
{
|
||||
const irep_idt &tag_name=
|
||||
to_c_enum_tag_type(type.subtype()).get_identifier();
|
||||
symbol_table.get_writeable(tag_name)->get().type.subtype()=result;
|
||||
symbol_table.get_writeable_ref(tag_name).type.subtype()=result;
|
||||
}
|
||||
|
||||
type=result;
|
||||
|
@ -782,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
|
|||
type.set(ID_tag, base_name);
|
||||
|
||||
typecheck_compound_body(type);
|
||||
symbol_table.get_writeable(s_it->first)->get().type.swap(type);
|
||||
symbol_table.get_writeable_ref(s_it->first).type.swap(type);
|
||||
}
|
||||
}
|
||||
else if(have_body)
|
||||
|
@ -1220,7 +1220,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
|
|||
{
|
||||
// Ok, overwrite the type in the symbol table.
|
||||
// This gives us the members and the subtype.
|
||||
symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type;
|
||||
symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
|
||||
}
|
||||
else if(symbol.type.id()==ID_c_enum)
|
||||
{
|
||||
|
|
|
@ -98,7 +98,7 @@ symbolt &cpp_declarator_convertert::convert(
|
|||
}
|
||||
|
||||
// try static first
|
||||
symbol_tablet::opt_symbol_reft maybe_symbol=
|
||||
auto maybe_symbol=
|
||||
cpp_typecheck.symbol_table.get_writeable(final_identifier);
|
||||
|
||||
if(!maybe_symbol)
|
||||
|
@ -191,7 +191,7 @@ symbolt &cpp_declarator_convertert::convert(
|
|||
}
|
||||
|
||||
// already there?
|
||||
symbol_tablet::opt_symbol_reft maybe_symbol=
|
||||
const auto maybe_symbol=
|
||||
cpp_typecheck.symbol_table.get_writeable(final_identifier);
|
||||
if(!maybe_symbol)
|
||||
return convert_new_symbol(storage_spec, member_spec, declarator);
|
||||
|
|
|
@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
|
|||
|
||||
// Make it nil to get zero initialization by
|
||||
// __CPROVER_initialize
|
||||
symbol_table.get_writeable(d_it)->get().value.make_nil();
|
||||
symbol_table.get_writeable_ref(d_it).value.make_nil();
|
||||
}
|
||||
else
|
||||
{
|
||||
|
@ -260,7 +260,7 @@ void cpp_typecheckt::do_not_typechecked()
|
|||
for(const auto &named_symbol : symbol_table.symbols)
|
||||
{
|
||||
if(named_symbol.second.value.id()=="cpp_not_typechecked")
|
||||
symbol_table.get_writeable(named_symbol.first)->get().value.make_nil();
|
||||
symbol_table.get_writeable_ref(named_symbol.first).value.make_nil();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -286,7 +286,7 @@ void cpp_typecheckt::clean_up()
|
|||
{
|
||||
// remove methods from 'components'
|
||||
struct_union_typet &struct_union_type=to_struct_union_type(
|
||||
symbol_table.get_writeable(cur_it->first)->get().type);
|
||||
symbol_table.get_writeable_ref(cur_it->first).type);
|
||||
|
||||
const struct_union_typet::componentst &components=
|
||||
struct_union_type.components();
|
||||
|
|
|
@ -159,9 +159,7 @@ void cpp_typecheckt::typecheck_compound_type(
|
|||
|
||||
// check if we have it already
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(symbol_name);
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.lookup(symbol_name))
|
||||
{
|
||||
// we do!
|
||||
const symbolt &symbol=*maybe_symbol;
|
||||
|
@ -553,7 +551,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
|
|||
put_compound_into_scope(compo);
|
||||
}
|
||||
|
||||
typet &vt=symbol_table.get_writeable(vt_name)->get().type;
|
||||
typet &vt=symbol_table.get_writeable_ref(vt_name).type;
|
||||
INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct");
|
||||
struct_typet &virtual_table=to_struct_type(vt);
|
||||
|
||||
|
|
|
@ -105,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union(
|
|||
id.is_member=true;
|
||||
}
|
||||
|
||||
symbol_table.get_writeable(union_symbol.name)->get().type.set(
|
||||
symbol_table.get_writeable_ref(union_symbol.name).type.set(
|
||||
"#unnamed_object", symbol.base_name);
|
||||
|
||||
code.swap(new_code);
|
||||
|
|
|
@ -1244,8 +1244,7 @@ void cpp_typecheckt::typecheck_expr_member(
|
|||
assert(it!=symbol_table.symbols.end());
|
||||
|
||||
if(it->second.value.id()=="cpp_not_typechecked")
|
||||
symbol_table.get_writeable(component_name)->get()
|
||||
.value.set("is_used", true);
|
||||
symbol_table.get_writeable_ref(component_name).value.set("is_used", true);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2203,7 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
|
|||
type.id()==ID_code &&
|
||||
type.find(ID_return_type).id()==ID_destructor)
|
||||
{
|
||||
add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get());
|
||||
add_method_body(&symbol_table.get_writeable_ref(it->get(ID_name)));
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
@ -2372,7 +2371,7 @@ void cpp_typecheckt::typecheck_method_application(
|
|||
member_expr.swap(expr.function());
|
||||
|
||||
const symbolt &symbol=lookup(member_expr.get(ID_component_name));
|
||||
add_method_body(&symbol_table.get_writeable(symbol.name)->get());
|
||||
add_method_body(&symbol_table.get_writeable_ref(symbol.name));
|
||||
|
||||
// build new function expression
|
||||
exprt new_function(cpp_symbol_expr(symbol));
|
||||
|
@ -2414,7 +2413,7 @@ void cpp_typecheckt::typecheck_method_application(
|
|||
if(symbol.value.id()=="cpp_not_typechecked" &&
|
||||
!symbol.value.get_bool("is_used"))
|
||||
{
|
||||
symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true);
|
||||
symbol_table.get_writeable_ref(symbol.name).value.set("is_used", true);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2683,7 +2682,7 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr)
|
|||
assert(it != symbol_table.symbols.end());
|
||||
|
||||
if(it->second.value.id()=="cpp_not_typechecked")
|
||||
symbol_table.get_writeable(it->first)->get().value.set("is_used", true);
|
||||
symbol_table.get_writeable_ref(it->first).value.set("is_used", true);
|
||||
}
|
||||
|
||||
c_typecheck_baset::typecheck_expr_function_identifier(expr);
|
||||
|
|
|
@ -107,9 +107,7 @@ void cpp_typecheckt::typecheck_class_template(
|
|||
|
||||
// check if we have it already
|
||||
|
||||
symbol_tablet::opt_symbol_reft maybe_symbol=
|
||||
symbol_table.get_writeable(symbol_name);
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))
|
||||
{
|
||||
// there already
|
||||
symbolt &previous_symbol=*maybe_symbol;
|
||||
|
@ -265,7 +263,7 @@ void cpp_typecheckt::typecheck_function_template(
|
|||
|
||||
if(has_value)
|
||||
{
|
||||
symbol_table.get_writeable(symbol_name)->get().type.swap(declaration);
|
||||
symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);
|
||||
cpp_scopes.id_map[symbol_name]=&template_scope;
|
||||
}
|
||||
|
||||
|
|
|
@ -725,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest)
|
|||
{
|
||||
debug() << "Compiling " << s_it->first << eom;
|
||||
converter.convert_function(s_it->first);
|
||||
symbol_table.get_writeable(*it)->get().value=exprt("compiled");
|
||||
symbol_table.get_writeable_ref(*it).value=exprt("compiled");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -168,8 +168,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
|
|||
// First, pointerize the actual linker-defined symbols
|
||||
for(const auto &pair : linker_values)
|
||||
{
|
||||
symbol_tablet::opt_symbol_reft maybe_symbol=
|
||||
symbol_table.get_writeable(pair.first);
|
||||
const auto maybe_symbol=symbol_table.get_writeable(pair.first);
|
||||
if(!maybe_symbol)
|
||||
continue;
|
||||
symbolt &entry=*maybe_symbol;
|
||||
|
@ -190,7 +189,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
|
|||
debug() << "Pointerizing the symbol-table value of symbol " << pair.first
|
||||
<< eom;
|
||||
int fail=pointerize_subexprs_of(
|
||||
symbol_table.get_writeable(pair.first)->get().value,
|
||||
symbol_table.get_writeable_ref(pair.first).value,
|
||||
to_pointerize,
|
||||
linker_values);
|
||||
if(to_pointerize.empty() && fail==0)
|
||||
|
|
|
@ -55,7 +55,7 @@ void dump_ct::operator()(std::ostream &os)
|
|||
continue;
|
||||
|
||||
code_typet &code_type=to_code_type(
|
||||
copied_symbol_table.get_writeable(named_symbol.first)->get().type);
|
||||
copied_symbol_table.get_writeable_ref(named_symbol.first).type);
|
||||
code_typet::parameterst ¶meters=code_type.parameters();
|
||||
|
||||
for(code_typet::parameterst::iterator
|
||||
|
|
|
@ -134,7 +134,7 @@ void goto_program2codet::scan_for_varargs()
|
|||
system_headers.insert("stdarg.h");
|
||||
|
||||
code_typet &code_type=
|
||||
to_code_type(symbol_table.get_writeable(func_name)->get().type);
|
||||
to_code_type(symbol_table.get_writeable_ref(func_name).type);
|
||||
code_typet::parameterst ¶meters=code_type.parameters();
|
||||
|
||||
for(code_typet::parameterst::iterator
|
||||
|
|
|
@ -51,7 +51,7 @@ void remove_function(
|
|||
message.status() << "Removing body of " << identifier
|
||||
<< messaget::eom;
|
||||
entry->second.clear();
|
||||
goto_model.symbol_table.get_writeable(identifier)->get().value.make_nil();
|
||||
goto_model.symbol_table.get_writeable_ref(identifier).value.make_nil();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -158,11 +158,10 @@ public:
|
|||
|
||||
irep_idt choice(const irep_idt &function, const std::string &suffix)
|
||||
{
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(function);
|
||||
const auto maybe_symbol=symbol_table.lookup(function);
|
||||
const std::string function_base_name =
|
||||
maybe_symbol
|
||||
? id2string(maybe_symbol->get().base_name)
|
||||
? id2string(maybe_symbol->base_name)
|
||||
: "main";
|
||||
return add(function_base_name+"_weak_choice",
|
||||
function_base_name+"_weak_choice", suffix, bool_typet());
|
||||
|
|
|
@ -444,7 +444,7 @@ typet interpretert::get_type(const irep_idt &id) const
|
|||
{
|
||||
dynamic_typest::const_iterator it=dynamic_types.find(id);
|
||||
if(it==dynamic_types.end())
|
||||
return symbol_table.lookup(id)->get().type;
|
||||
return symbol_table.lookup_ref(id).type;
|
||||
return it->second;
|
||||
}
|
||||
|
||||
|
@ -1041,7 +1041,7 @@ exprt interpretert::get_value(const irep_idt &id)
|
|||
if(findit!=dynamic_types.end())
|
||||
get_type=findit->second;
|
||||
else
|
||||
get_type=symbol_table.lookup(id)->get().type;
|
||||
get_type=symbol_table.lookup_ref(id).type;
|
||||
|
||||
symbol_exprt symbol_expr(id, get_type);
|
||||
mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
|
||||
|
|
|
@ -118,13 +118,13 @@ void mm_io(
|
|||
irep_idt id_r=CPROVER_PREFIX "mm_io_r";
|
||||
irep_idt id_w=CPROVER_PREFIX "mm_io_w";
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id_r);
|
||||
auto maybe_symbol=symbol_table.lookup(id_r);
|
||||
if(maybe_symbol)
|
||||
mm_io_r=maybe_symbol->get().symbol_expr();
|
||||
mm_io_r=maybe_symbol->symbol_expr();
|
||||
|
||||
maybe_symbol=symbol_table.lookup(id_w);
|
||||
if(maybe_symbol)
|
||||
mm_io_w=maybe_symbol->get().symbol_expr();
|
||||
mm_io_w=maybe_symbol->symbol_expr();
|
||||
|
||||
for(auto & f : goto_functions.function_map)
|
||||
mm_io(mm_io_r, mm_io_w, f.second, ns);
|
||||
|
|
|
@ -134,8 +134,7 @@ void remove_exceptionst::add_exceptional_returns(
|
|||
const irep_idt &function_id=func_it->first;
|
||||
goto_programt &goto_program=func_it->second.body;
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(function_id);
|
||||
auto maybe_symbol=symbol_table.lookup(function_id);
|
||||
INVARIANT(maybe_symbol, "functions should be recorded in the symbol table");
|
||||
const symbolt &function_symbol=*maybe_symbol;
|
||||
|
||||
|
@ -255,11 +254,9 @@ void remove_exceptionst::instrument_exception_handler(
|
|||
to_code_landingpad(instr_it->code).catch_expr();
|
||||
irep_idt thrown_exception_global=id2string(function_id)+EXC_SUFFIX;
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(thrown_exception_global);
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.lookup(thrown_exception_global))
|
||||
{
|
||||
const symbol_exprt thrown_global_symbol=maybe_symbol->get().symbol_expr();
|
||||
const symbol_exprt thrown_global_symbol=maybe_symbol->symbol_expr();
|
||||
// next we reset the exceptional return to NULL
|
||||
null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
|
||||
|
||||
|
@ -425,9 +422,9 @@ void remove_exceptionst::instrument_function_call(
|
|||
const irep_idt &callee_id=
|
||||
to_symbol_expr(function_call.function()).get_identifier();
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft callee_inflight_exception=
|
||||
const auto callee_inflight_exception=
|
||||
symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX);
|
||||
symbol_tablet::opt_const_symbol_reft local_inflight_exception=
|
||||
const auto local_inflight_exception=
|
||||
symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
|
||||
|
||||
if(callee_inflight_exception && local_inflight_exception)
|
||||
|
@ -436,9 +433,9 @@ void remove_exceptionst::instrument_function_call(
|
|||
func_it, instr_it, stack_catch, locals);
|
||||
|
||||
const symbol_exprt callee_inflight_exception_expr=
|
||||
callee_inflight_exception->get().symbol_expr();
|
||||
callee_inflight_exception->symbol_expr();
|
||||
const symbol_exprt local_inflight_exception_expr=
|
||||
local_inflight_exception->get().symbol_expr();
|
||||
local_inflight_exception->symbol_expr();
|
||||
|
||||
// add a null check (so that instanceof can be applied)
|
||||
equal_exprt eq_null(
|
||||
|
|
|
@ -58,8 +58,7 @@ void remove_static_init_loopst::unwind_enum_static(
|
|||
const std::string &fname=id2string(ins.function);
|
||||
size_t class_prefix_length=fname.find_last_of('.');
|
||||
// is the function symbol in the symbol table?
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(ins.function);
|
||||
const auto maybe_symbol=symbol_table.lookup(ins.function);
|
||||
if(!maybe_symbol)
|
||||
{
|
||||
message.warning() << "function `" << id2string(ins.function)
|
||||
|
|
|
@ -144,7 +144,7 @@ bool ci_lazy_methodst::operator()(
|
|||
method_converter(
|
||||
*parsed_method.first, *parsed_method.second, new_lazy_methods);
|
||||
gather_virtual_callsites(
|
||||
symbol_table.lookup(mname)->get().value,
|
||||
symbol_table.lookup_ref(mname).value,
|
||||
virtual_callsites);
|
||||
any_new_methods=true;
|
||||
}
|
||||
|
|
|
@ -893,8 +893,7 @@ bool java_bytecode_convert_methodt::class_needs_clinit(
|
|||
findit_any.first->second=true;
|
||||
return true;
|
||||
}
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(classname);
|
||||
const auto maybe_symbol=symbol_table.lookup(classname);
|
||||
// Stub class?
|
||||
if(!maybe_symbol)
|
||||
{
|
||||
|
|
|
@ -617,5 +617,5 @@ void java_bytecode_instrument(
|
|||
// instrument(...) can add symbols to the table, so it's
|
||||
// not safe to hold a reference to a symbol across a call.
|
||||
for(const auto &symbol : symbols_to_instrument)
|
||||
instrument(symbol_table.get_writeable(symbol)->get().value);
|
||||
instrument(symbol_table.get_writeable_ref(symbol).value);
|
||||
}
|
||||
|
|
|
@ -796,8 +796,8 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
|
|||
|
||||
typet deref_type;
|
||||
if(rhs.type().subtype().id()==ID_symbol)
|
||||
deref_type=symbol_table.lookup(
|
||||
to_symbol_type(rhs.type().subtype()).get_identifier())->get().type;
|
||||
deref_type=symbol_table.lookup_ref(
|
||||
to_symbol_type(rhs.type().subtype()).get_identifier()).type;
|
||||
else
|
||||
deref_type=rhs.type().subtype();
|
||||
|
||||
|
@ -1252,11 +1252,9 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
|
|||
|
||||
// Check that the type of the object is in the symbol table,
|
||||
// otherwise there is no safe way of finding its value.
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(object_type.get_identifier());
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier()))
|
||||
{
|
||||
struct_typet struct_type=to_struct_type(maybe_symbol->get().type);
|
||||
struct_typet struct_type=to_struct_type(maybe_symbol->type);
|
||||
// Check that the type has a value field
|
||||
const struct_union_typet::componentt value_comp=
|
||||
struct_type.get_component("value");
|
||||
|
@ -1502,7 +1500,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
|
|||
// > Class class1;
|
||||
pointer_typet class_type=
|
||||
java_reference_type(
|
||||
symbol_table.lookup("java::java.lang.Class")->get().type);
|
||||
symbol_table.lookup_ref("java::java.lang.Class").type);
|
||||
symbolt class1_sym=get_fresh_aux_symbol(
|
||||
class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
|
||||
symbol_exprt class1=class1_sym.symbol_expr();
|
||||
|
@ -1539,7 +1537,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
|
|||
|
||||
// string1 = (String*) string_expr
|
||||
pointer_typet string_ptr_type=java_reference_type(
|
||||
symbol_table.lookup("java::java.lang.String")->get().type);
|
||||
symbol_table.lookup_ref("java::java.lang.String").type);
|
||||
exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code);
|
||||
code.add(
|
||||
code_assign_string_expr_to_new_java_string(
|
||||
|
|
|
@ -48,9 +48,7 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree)
|
|||
if(convert_code(new_symbol, to_code(new_symbol.value)))
|
||||
return true;
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(new_symbol.name);
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.lookup(new_symbol.name))
|
||||
{
|
||||
const symbolt &s=*maybe_symbol;
|
||||
if(s.value.id()=="no-body-just-yet")
|
||||
|
|
|
@ -42,8 +42,7 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type)
|
|||
{
|
||||
const irep_idt &id=to_symbol_expr(expr).get_identifier();
|
||||
|
||||
symbol_tablet::opt_symbol_reft maybe_symbol=
|
||||
symbol_table.get_writeable(id);
|
||||
const auto maybe_symbol=symbol_table.get_writeable(id);
|
||||
if(!maybe_symbol)
|
||||
{
|
||||
error() << "unexpected symbol: " << id << eom;
|
||||
|
@ -749,8 +748,7 @@ void jsil_typecheckt::typecheck_function_call(
|
|||
{
|
||||
const irep_idt &id=to_symbol_expr(f).get_identifier();
|
||||
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id);
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.lookup(id))
|
||||
{
|
||||
const symbolt &s=*maybe_symbol;
|
||||
|
||||
|
|
|
@ -1290,7 +1290,7 @@ void linkingt::copy_symbols()
|
|||
named_symbol.second.value.is_not_nil())
|
||||
{
|
||||
object_type_updates(
|
||||
main_symbol_table.get_writeable(named_symbol.first)->get().value);
|
||||
main_symbol_table.get_writeable_ref(named_symbol.first).value);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -31,8 +31,7 @@ bool static_lifetime_init(
|
|||
{
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
symbol_tablet::opt_symbol_reft maybe_symbol=
|
||||
symbol_table.get_writeable(INITIALIZE_FUNCTION);
|
||||
const auto maybe_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION);
|
||||
if(!maybe_symbol)
|
||||
return false;
|
||||
symbolt &init_symbol=*maybe_symbol;
|
||||
|
|
|
@ -1177,9 +1177,7 @@ void configt::set_object_bits_from_symbol_table(
|
|||
return;
|
||||
|
||||
// set object_bits according to entry point language
|
||||
symbol_tablet::opt_const_symbol_reft maybe_symbol=
|
||||
symbol_table.lookup(CPROVER_PREFIX "_start");
|
||||
if(maybe_symbol)
|
||||
if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
|
||||
{
|
||||
const symbolt &entry_point_symbol=*maybe_symbol;
|
||||
|
||||
|
|
|
@ -148,30 +148,6 @@ void symbol_tablet::show(std::ostream &out) const
|
|||
out << it->second;
|
||||
}
|
||||
|
||||
/// Find a symbol in the symbol table for read-only access.
|
||||
/// \param identifier: The name of the symbol to look for
|
||||
/// \return an optional reference, set if found, unset otherwise.
|
||||
symbol_tablet::opt_const_symbol_reft symbol_tablet::lookup(
|
||||
const irep_idt &identifier) const
|
||||
{
|
||||
symbolst::const_iterator it=symbols.find(identifier);
|
||||
if(it==symbols.end())
|
||||
return opt_const_symbol_reft();
|
||||
return std::ref(it->second);
|
||||
}
|
||||
|
||||
/// Find a symbol in the symbol table for read-write access.
|
||||
/// \param identifier: The name of the symbol to look for
|
||||
/// \return an optional reference, set if found, unset otherwise.
|
||||
symbol_tablet::opt_symbol_reft symbol_tablet::get_writeable(
|
||||
const irep_idt &identifier)
|
||||
{
|
||||
symbolst::iterator it=internal_symbols.find(identifier);
|
||||
if(it==symbols.end())
|
||||
return opt_symbol_reft();
|
||||
return std::ref(it->second);
|
||||
}
|
||||
|
||||
/// Print the contents of the symbol table
|
||||
/// \param out: The ostream to direct output to
|
||||
/// \param symbol_table: The symbol table to print out
|
||||
|
|
|
@ -41,9 +41,6 @@ class symbol_tablet
|
|||
{
|
||||
public:
|
||||
typedef std::unordered_map<irep_idt, symbolt, irep_id_hash> symbolst;
|
||||
typedef optionalt<std::reference_wrapper<const symbolt>>
|
||||
opt_const_symbol_reft;
|
||||
typedef optionalt<std::reference_wrapper<symbolt>> opt_symbol_reft;
|
||||
|
||||
private:
|
||||
symbolst internal_symbols;
|
||||
|
@ -101,9 +98,29 @@ public:
|
|||
return symbols.find(name)!=symbols.end();
|
||||
}
|
||||
|
||||
opt_const_symbol_reft lookup(const irep_idt &identifier) const;
|
||||
/// Find a symbol in the symbol table for read-only access.
|
||||
/// \param id: The name of the symbol to look for
|
||||
/// \return an optional reference, set if found, nullptr otherwise.
|
||||
const symbolt *lookup(const irep_idt &id) const { return lookup_impl(id); }
|
||||
|
||||
opt_symbol_reft get_writeable(const irep_idt &identifier);
|
||||
/// Find a symbol in the symbol table for read-write access.
|
||||
/// \param id: The name of the symbol to look for
|
||||
/// \return an optional reference, set if found, unset otherwise.
|
||||
symbolt *get_writeable(const irep_idt &id) { return lookup_impl(id); }
|
||||
|
||||
/// Find a symbol in the symbol table for read-only access.
|
||||
/// \param id: The name of the symbol to look for
|
||||
/// \return A reference to the symbol
|
||||
/// \throw `std::out_of_range` if no such symbol exists
|
||||
const symbolt &lookup_ref(const irep_idt &id) const
|
||||
{ return internal_symbols.at(id); }
|
||||
|
||||
/// Find a symbol in the symbol table for read-write access.
|
||||
/// \param id: The name of the symbol to look for
|
||||
/// \return A reference to the symbol
|
||||
/// \throw `std::out_of_range` if no such symbol exists
|
||||
symbolt &get_writeable_ref(const irep_idt &id)
|
||||
{ return internal_symbols.at(id); }
|
||||
|
||||
bool add(const symbolt &symbol);
|
||||
|
||||
|
@ -130,6 +147,21 @@ public:
|
|||
internal_symbol_base_map.swap(other.internal_symbol_base_map);
|
||||
internal_symbol_module_map.swap(other.internal_symbol_module_map);
|
||||
}
|
||||
|
||||
private:
|
||||
const symbolt *lookup_impl(const irep_idt &id) const
|
||||
{ return lookup_impl(*this, id); }
|
||||
|
||||
symbolt *lookup_impl(const irep_idt &id)
|
||||
{ return lookup_impl(*this, id); }
|
||||
|
||||
template<typename T>
|
||||
static auto lookup_impl(T &t, const irep_idt &id)
|
||||
-> decltype(std::declval<T>().lookup_impl(id))
|
||||
{
|
||||
const auto it=t.internal_symbols.find(id);
|
||||
return it==t.internal_symbols.end()?nullptr:&it->second;
|
||||
}
|
||||
};
|
||||
|
||||
std::ostream &operator << (
|
||||
|
|
|
@ -32,8 +32,7 @@ SCENARIO(
|
|||
std::string class_prefix="java::DerivedGeneric";
|
||||
REQUIRE(new_symbol_table.has_symbol(class_prefix));
|
||||
|
||||
const symbolt &derived_symbol=new_symbol_table.lookup(class_prefix).value
|
||||
().get();
|
||||
const symbolt &derived_symbol=new_symbol_table.lookup_ref(class_prefix);
|
||||
REQUIRE(derived_symbol.is_type);
|
||||
const typet &derived_type=derived_symbol.type;
|
||||
REQUIRE(derived_type.id()==ID_struct);
|
||||
|
|
|
@ -32,8 +32,7 @@ SCENARIO(
|
|||
REQUIRE(new_symbol_table.has_symbol(class_prefix));
|
||||
|
||||
const struct_typet &type=to_struct_type(
|
||||
new_symbol_table.lookup(class_prefix)
|
||||
.value().get().type);
|
||||
new_symbol_table.lookup_ref(class_prefix).type);
|
||||
|
||||
THEN("There should be a component with name t")
|
||||
{
|
||||
|
@ -48,8 +47,7 @@ SCENARIO(
|
|||
THEN("The t component is a valid java array")
|
||||
{
|
||||
const struct_typet &subtype_type=to_struct_type(
|
||||
new_symbol_table.lookup(subtype.get_identifier())
|
||||
.value().get().type);
|
||||
new_symbol_table.lookup_ref(subtype.get_identifier()).type);
|
||||
REQUIRE(is_valid_java_array(subtype_type));
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in New Issue