context -> symbol_table
This commit is contained in:
parent
0e973cc8fd
commit
c1907f7ca0
|
@ -231,7 +231,7 @@ void bmc_cegart::make_netlist()
|
|||
try
|
||||
{
|
||||
convert_trans_to_netlist(
|
||||
context, main_module,
|
||||
symbol_table, main_module,
|
||||
properties, concrete_netlist, message);
|
||||
}
|
||||
|
||||
|
|
|
@ -17,13 +17,13 @@ class bmc_cegart
|
|||
{
|
||||
public:
|
||||
bmc_cegart(
|
||||
contextt &_context,
|
||||
symbol_tablet &_symbol_table,
|
||||
const irep_idt &_main_module,
|
||||
messaget &_message,
|
||||
const std::list<exprt> &_properties,
|
||||
bool _verbose):
|
||||
context(_context),
|
||||
ns(_context),
|
||||
symbol_table(_symbol_table),
|
||||
ns(_symbol_table),
|
||||
main_module(_main_module),
|
||||
message(_message),
|
||||
properties(_properties),
|
||||
|
@ -34,7 +34,7 @@ public:
|
|||
void bmc_cegar();
|
||||
|
||||
protected:
|
||||
contextt &context;
|
||||
symbol_tablet &symbol_table;
|
||||
const namespacet ns;
|
||||
const irep_idt &main_module;
|
||||
messaget &message;
|
||||
|
|
|
@ -271,7 +271,7 @@ void induction_coveraget::remove_covered(const bmc_mapt &bmc_map,
|
|||
|
||||
solver.set_assumptions(assumptions);
|
||||
propt::resultt dec_result = solver.prop_solve();
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
switch(dec_result)
|
||||
{
|
||||
|
@ -388,7 +388,7 @@ void induction_coveraget::remove_not_covered_from_scratch(const bmc_mapt &bmc_ma
|
|||
induction_test_from_scratch.total_tests++;
|
||||
propt::resultt dec_result = solver.prop_solve();
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
switch(dec_result)
|
||||
{
|
||||
|
@ -544,7 +544,7 @@ induction_resultt induction_coveraget::is_inductive(bool force,
|
|||
satcheckt &interpolator,
|
||||
bool assume)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
bmc_mapt netlist_bmc_map_induction;
|
||||
netlist_bmc_map_induction.map_timeframes(netlist, 2, interpolator); //vars in tf 0 and 1
|
||||
|
@ -681,7 +681,7 @@ literalt induction_coveraget::unwind(
|
|||
induction_resultt induction_coveraget::is_inductive1(bool force,
|
||||
satcheck_minisat_normal_prooft &interpolator)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
interpolator.set_partition_id(1);
|
||||
bmc_mapt netlist_bmc_map_induction;
|
||||
|
|
|
@ -166,7 +166,7 @@ int interpolation_coveraget::iteration()
|
|||
status("Iteration "+i2string(iteration_number)+
|
||||
", bound="+i2string(bound));
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
solver.equality_propagation=false;
|
||||
|
@ -314,7 +314,7 @@ int interpolation_coveraget::induction_step()
|
|||
{
|
||||
status("Induction Step");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort satcheck;
|
||||
boolbvt solver(ns, satcheck);
|
||||
|
||||
|
@ -379,7 +379,7 @@ int interpolation_coveraget::induction_step()
|
|||
|
||||
bool interpolation_coveraget::check_partition_one_implies_interpolant(const bit_interpolantt ¤t_inter)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
|
||||
|
@ -417,7 +417,7 @@ bool interpolation_coveraget::check_partition_one_implies_interpolant(const bit_
|
|||
|
||||
bool interpolation_coveraget::check_partition_two_and_interpolant(const bit_interpolantt ¤t_inter)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
|
||||
|
@ -494,7 +494,7 @@ else {
|
|||
|
||||
|
||||
propt::resultt dec_result = solver.prop_solve();
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
switch(dec_result)
|
||||
{
|
||||
|
|
|
@ -69,7 +69,7 @@ Function: ebmc_baset::show_trace
|
|||
|
||||
void ebmc_baset::show_trace(const trans_tracet &trans_trace)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
if(cmdline.isset("vcd"))
|
||||
{
|
||||
|
@ -125,7 +125,7 @@ int ebmc_baset::finish(prop_convt &solver)
|
|||
{
|
||||
result("SAT: bug found");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
trans_tracet trans_trace;
|
||||
|
||||
compute_trans_trace(
|
||||
|
@ -189,7 +189,7 @@ int ebmc_baset::finish(const bmc_mapt &bmc_map, propt &solver)
|
|||
{
|
||||
result("SAT: bug found");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
trans_tracet trans_trace;
|
||||
|
||||
compute_trans_trace(
|
||||
|
@ -255,7 +255,7 @@ void ebmc_baset::unwind(
|
|||
unsigned _bound,
|
||||
bool initial_state)
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
::unwind(*trans_expr, *this, solver, _bound, ns, initial_state);
|
||||
}
|
||||
|
||||
|
@ -281,7 +281,7 @@ void ebmc_baset::check_property(prop_convt &solver, bool convert_only)
|
|||
|
||||
unwind(solver);
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
property(
|
||||
prop_expr_list,
|
||||
|
@ -336,7 +336,7 @@ Function: ebmc_baset::parse_property
|
|||
bool ebmc_baset::parse_property(
|
||||
const std::string &property)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
languagest languages(ns,
|
||||
get_language_from_mode(main_symbol->mode));
|
||||
|
@ -388,10 +388,10 @@ bool ebmc_baset::get_model_properties()
|
|||
{
|
||||
forall_symbol_module_map(
|
||||
it,
|
||||
context.symbol_module_map,
|
||||
symbol_table.symbol_module_map,
|
||||
main_symbol->name)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
const symbolt &symbol=ns.lookup(it->second);
|
||||
|
||||
if(symbol.is_property)
|
||||
|
@ -506,7 +506,7 @@ bool ebmc_baset::get_main()
|
|||
|
||||
try
|
||||
{
|
||||
main_symbol=&get_module(context, module, get_message_handler());
|
||||
main_symbol=&get_module(symbol_table, module, get_message_handler());
|
||||
trans_expr=&to_trans_expr(main_symbol->value);
|
||||
}
|
||||
|
||||
|
@ -639,15 +639,6 @@ void ebmc_baset::report_success()
|
|||
|
||||
switch(get_ui())
|
||||
{
|
||||
case ui_message_handlert::OLD_GUI:
|
||||
std::cout << "SUCCESS" << std::endl
|
||||
<< "Verification successful" << std::endl
|
||||
<< "" << std::endl
|
||||
<< "" << std::endl
|
||||
<< "" << std::endl
|
||||
<< "" << std::endl;
|
||||
break;
|
||||
|
||||
case ui_message_handlert::PLAIN:
|
||||
break;
|
||||
|
||||
|
@ -683,9 +674,6 @@ void ebmc_baset::report_failure()
|
|||
|
||||
switch(get_ui())
|
||||
{
|
||||
case ui_message_handlert::OLD_GUI:
|
||||
break;
|
||||
|
||||
case ui_message_handlert::PLAIN:
|
||||
break;
|
||||
|
||||
|
@ -742,7 +730,7 @@ int ebmc_baset::get_model()
|
|||
|
||||
if(cmdline.isset("show-modules"))
|
||||
{
|
||||
show_modules(context, get_ui());
|
||||
show_modules(symbol_table, get_ui());
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
@ -893,7 +881,7 @@ void ebmc_baset::make_netlist(netlistt &netlist)
|
|||
try
|
||||
{
|
||||
convert_trans_to_netlist(
|
||||
context, main_symbol->name, prop_expr_list, netlist, *this);
|
||||
symbol_table, main_symbol->name, prop_expr_list, netlist, *this);
|
||||
}
|
||||
|
||||
catch(const std::string &error_str)
|
||||
|
|
|
@ -89,7 +89,7 @@ Function: ebmc_baset::do_dplib
|
|||
|
||||
int ebmc_baset::do_dplib()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
if(cmdline.isset("outfile"))
|
||||
{
|
||||
|
@ -126,7 +126,7 @@ Function: ebmc_baset::do_smt1
|
|||
|
||||
int ebmc_baset::do_smt1()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
if(cmdline.isset("outfile"))
|
||||
{
|
||||
|
@ -175,7 +175,7 @@ Function: ebmc_baset::do_smt2
|
|||
|
||||
int ebmc_baset::do_smt2()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
if(cmdline.isset("outfile"))
|
||||
{
|
||||
|
@ -224,7 +224,7 @@ Function: ebmc_baset::do_z3
|
|||
|
||||
int ebmc_baset::do_z3()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
smt1_dect smt1_dec(
|
||||
ns,
|
||||
|
@ -250,7 +250,7 @@ Function: ebmc_baset::do_cvc3
|
|||
|
||||
int ebmc_baset::do_cvc3()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
smt1_dect smt1_dec(
|
||||
ns,
|
||||
|
@ -276,7 +276,7 @@ Function: ebmc_baset::do_yices
|
|||
|
||||
int ebmc_baset::do_yices()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
smt1_dect smt1_dec(
|
||||
ns,
|
||||
|
@ -302,7 +302,7 @@ Function: ebmc_baset::do_boolector
|
|||
|
||||
int ebmc_baset::do_boolector()
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
smt1_dect smt1_dec(
|
||||
ns,
|
||||
|
@ -332,7 +332,7 @@ int ebmc_baset::do_sat()
|
|||
|
||||
if(cmdline.isset("no-netlist"))
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
boolbvt boolbv(ns, satcheck);
|
||||
return do_ebmc(boolbv, false);
|
||||
}
|
||||
|
@ -355,7 +355,7 @@ Function: ebmc_baset::do_prover
|
|||
int ebmc_baset::do_prover()
|
||||
{
|
||||
#ifdef HAVE_PROVER
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
prover_satt prover_sat(ns);
|
||||
return do_ebmc(prover_sat, false);
|
||||
#else
|
||||
|
@ -379,7 +379,7 @@ Function: ebmc_baset::do_lifter
|
|||
int ebmc_baset::do_lifter()
|
||||
{
|
||||
#ifdef HAVE_PROVER
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
liftert lifter(ns);
|
||||
return do_ebmc(lifter.prop_conv(), false);
|
||||
#else
|
||||
|
|
|
@ -53,7 +53,7 @@ static void reverse_partitions(
|
|||
std::cout << i_bit_2 << std::endl;
|
||||
|
||||
satcheckt solver1;
|
||||
// namespacet ns(context);
|
||||
// namespacet ns(symbol_table);
|
||||
i_bit_1.add_variables(solver1);
|
||||
i_bit_2.add_variables(solver1);
|
||||
|
||||
|
@ -78,7 +78,7 @@ static void reverse_partitions(
|
|||
}
|
||||
|
||||
satcheckt solver2;
|
||||
// namespacet ns(context);
|
||||
// namespacet ns(symbol_table);
|
||||
i_bit_1.add_variables(solver2);
|
||||
i_bit_2.add_variables(solver2);
|
||||
|
||||
|
|
|
@ -91,7 +91,7 @@ int interpolationt::check_initial_state()
|
|||
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(satcheck);
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
// check if I AND !P is satisfiable
|
||||
|
||||
|
@ -222,7 +222,7 @@ void interpolationt::build_variable_map(
|
|||
it!=symbols.end();
|
||||
it++)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
//const symbolt &symbol=ns.lookup(*it);
|
||||
|
||||
//exprt e0(symbol_expr(symbol));
|
||||
|
@ -283,7 +283,7 @@ int interpolationt::iteration()
|
|||
return 1;
|
||||
}
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(interpolator);
|
||||
solver.equality_propagation=false;
|
||||
|
@ -411,7 +411,7 @@ bool interpolationt::reached_fixedpoint()
|
|||
if(new_interpolant.is_false()) return true;
|
||||
|
||||
satcheckt solver;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
// "old" set of states
|
||||
status("interpolants.size() " + i2string(interpolants.size()));
|
||||
|
||||
|
@ -587,7 +587,7 @@ void interpolationt::build_partition1(
|
|||
prop_convt &solver)
|
||||
{
|
||||
status("build_partition1");
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
if(interpolants.empty())
|
||||
{
|
||||
|
@ -629,7 +629,7 @@ void interpolationt::build_partition2(
|
|||
prop_convt &solver)
|
||||
{
|
||||
status("build_partition2");
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
unsigned no_timeframes=bound+1;
|
||||
|
||||
const exprt &op_invar=trans_expr->invar();
|
||||
|
@ -664,7 +664,7 @@ void interpolationt::build_property(
|
|||
|
||||
status("build_property");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
unsigned no_timeframes=bound+1;
|
||||
unsigned start;
|
||||
|
||||
|
@ -755,7 +755,7 @@ bool interpolationt::check_partition_one_implies_interpolant()
|
|||
|
||||
if(new_interpolant.is_false()) return false;
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt solver;
|
||||
boolbvt boolbv(solver);
|
||||
boolbv.equality_propagation=false;
|
||||
|
@ -825,7 +825,7 @@ bool interpolationt::check_partition_two_and_interpolant()
|
|||
|
||||
if(new_interpolant.is_false()) return false;
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt solver;
|
||||
boolbvt boolbv(solver);
|
||||
boolbv.equality_propagation=false;
|
||||
|
@ -860,7 +860,7 @@ int interpolationt::induction_step()
|
|||
{
|
||||
status("Induction Step");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(satcheck);
|
||||
|
||||
|
|
|
@ -126,7 +126,7 @@ int interpolationt_netlist::check_initial_state()
|
|||
{
|
||||
satcheckt satcheck;
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
boolbvt solver(ns,satcheck);
|
||||
// check if I AND !P is satisfiable
|
||||
|
||||
|
@ -198,7 +198,7 @@ int interpolationt_netlist::iteration()
|
|||
", bound="+i2string(bound));
|
||||
//see if induction succeeds
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
solver.equality_propagation=false;
|
||||
|
@ -324,7 +324,7 @@ bool interpolationt_netlist::reached_fixedpoint()
|
|||
}
|
||||
*/
|
||||
satcheckt solver;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
bmc_mapt netlist_bmc_map_check;
|
||||
netlist_bmc_map_check.map_timeframes(working_netlist, bound+1, solver);
|
||||
|
||||
|
@ -816,7 +816,7 @@ int interpolationt_netlist::induction_step()
|
|||
{
|
||||
status("Induction Step");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort satcheck;
|
||||
boolbvt solver(ns, satcheck);
|
||||
|
||||
|
@ -928,7 +928,7 @@ void interpolationt_netlist::get_strengthened_interpolant(
|
|||
|
||||
bool interpolationt_netlist::check_partition_one_implies_interpolant(const bit_interpolantt ¤t_inter)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
|
||||
|
@ -961,7 +961,7 @@ bool interpolationt_netlist::check_partition_one_implies_interpolant(const bit_i
|
|||
|
||||
bool interpolationt_netlist::check_partition_two_and_interpolant(const bit_interpolantt ¤t_inter)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
|
||||
|
@ -1029,7 +1029,7 @@ else {
|
|||
// build_property(solver, bmc_map);
|
||||
|
||||
propt::resultt dec_result = solver.prop_solve();
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
switch(dec_result)
|
||||
{
|
||||
|
|
|
@ -185,7 +185,7 @@ int interpolationt_netlist_vmcai::forward_iteration()
|
|||
status("Iteration "+i2string(forward_iteration_number)+
|
||||
", bound="+i2string(bound));
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(interpolator);
|
||||
solver.equality_propagation=false;
|
||||
|
@ -301,7 +301,7 @@ bool interpolationt_netlist_vmcai::reached_fixedpoint(
|
|||
}
|
||||
|
||||
satcheckt solver;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
netlist_bmc_mapt netlist_bmc_map_check;
|
||||
netlist_bmc_map_check.map_timeframes(netlist, bound+1, solver);
|
||||
|
||||
|
@ -549,7 +549,7 @@ void interpolationt_netlist_vmcai::build_forward_property(
|
|||
{
|
||||
status("interpolationt_netlist_vmcai::build_property");
|
||||
|
||||
// namespacet ns(context);
|
||||
// namespacet ns(symbol_table);
|
||||
unsigned no_timeframes=bound+1;
|
||||
|
||||
prop_bv.clear();
|
||||
|
@ -580,7 +580,7 @@ void interpolationt_netlist_vmcai::build_forward_property(
|
|||
bool interpolationt_netlist_vmcai::is_property()
|
||||
{
|
||||
satcheckt solver;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
boolbvt solverbv(solver);
|
||||
|
||||
netlist_bmc_mapt netlist_bmc_map_init;
|
||||
|
@ -653,7 +653,7 @@ int interpolationt_netlist_vmcai::check_forward_reachable_states()
|
|||
return 0;
|
||||
}
|
||||
std::cout << "checking forward reachable states\n";
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(satcheck);
|
||||
unsigned check_bound = 2;
|
||||
|
@ -717,7 +717,7 @@ int interpolationt_netlist_vmcai::Refine_Interpolant(
|
|||
bool forward)
|
||||
{
|
||||
std::vector<unsigned > *fault_locations = forward ? &forward_fault_locations : &backward_fault_locations;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
status("SAT::Refine Interpolant");
|
||||
if(forward)
|
||||
forward_refinement = true;
|
||||
|
@ -900,7 +900,7 @@ int interpolationt_netlist_vmcai::backward_iteration()
|
|||
status("Iteration "+i2string(backward_iteration_number)+
|
||||
", bound="+i2string(bound));
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(interpolator);
|
||||
solver.equality_propagation=false;
|
||||
|
@ -975,7 +975,7 @@ int interpolationt_netlist_vmcai::backward_iteration()
|
|||
|
||||
int interpolationt_netlist_vmcai::check_backward_reachable_states()
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(satcheck);
|
||||
unsigned check_bound = 2;
|
||||
|
@ -1038,7 +1038,7 @@ void interpolationt_netlist_vmcai::build_backward_property(
|
|||
{
|
||||
status("build_property");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
prop_bv.clear();
|
||||
|
||||
bvt all_prop_bv;
|
||||
|
@ -1069,7 +1069,7 @@ void interpolationt_netlist_vmcai::build_backward_partition1(interpolatort &solv
|
|||
::unwind(netlist, netlist_bmc_map, *this, solver, false, bound);
|
||||
::unwind(netlist, netlist_bmc_map, *this, solver, false, bound-1);
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
bvt all_prop_bv;
|
||||
for(unsigned p_no=0; p_no<netlist.properties.size(); p_no++)
|
||||
{
|
||||
|
@ -1125,7 +1125,7 @@ void interpolationt_netlist_vmcai::check_if_interpolant_reach_intersect(
|
|||
aig_formulat &new_interpolant = interpolants->back();
|
||||
|
||||
satcheckt solver;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
netlist_bmc_mapt netlist_bmc_map_check;
|
||||
netlist_bmc_map_check.map_timeframes(netlist, bound+1, solver);
|
||||
|
||||
|
|
|
@ -177,7 +177,7 @@ int interpolationt_word::check_initial_state()
|
|||
{
|
||||
status("Checking initial state");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(ns, satcheck);
|
||||
|
||||
|
@ -305,7 +305,7 @@ void interpolationt_word::build_variable_map(
|
|||
it!=symbols.end();
|
||||
it++)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
exprt e0(*it);
|
||||
exprt e1(*it);
|
||||
|
@ -394,7 +394,7 @@ int interpolationt_word::iteration()
|
|||
return 1;
|
||||
}
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
interpolatort interpolator;
|
||||
boolbvt solver(ns, interpolator);
|
||||
solver.equality_propagation=false;
|
||||
|
@ -540,7 +540,7 @@ bool interpolationt_word::reached_fixedpoint()
|
|||
if(new_interpolant.is_false()) return true;
|
||||
|
||||
satcheckt solver;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
boolbvt prop_conv(ns, solver);
|
||||
build_variable_map(prop_conv);
|
||||
// "old" set of states
|
||||
|
@ -661,7 +661,7 @@ void interpolationt_word::get_interpolant(
|
|||
// interpolant = do_word_interpolation.get_interpolant(1);
|
||||
}
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
simplify(interpolant, ns);
|
||||
/* {
|
||||
|
||||
|
@ -716,7 +716,7 @@ void interpolationt_word::build_partition1(
|
|||
prop_convt &solver)
|
||||
{
|
||||
status("build_partition1");
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
if(interpolants.empty())
|
||||
{
|
||||
|
@ -761,7 +761,7 @@ void interpolationt_word::build_partition2(
|
|||
prop_convt &solver)
|
||||
{
|
||||
status("build_partition2");
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
unsigned no_timeframes=bound+1;
|
||||
|
||||
const exprt &op_invar=trans_expr->invar();
|
||||
|
@ -798,7 +798,7 @@ void interpolationt_word::build_property(
|
|||
|
||||
status("build_property");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
unsigned no_timeframes=bound+1;
|
||||
unsigned start;
|
||||
|
||||
|
@ -889,7 +889,7 @@ int interpolationt_word::induction_step()
|
|||
{
|
||||
status("Induction Step");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(ns, satcheck);
|
||||
|
||||
|
@ -1032,7 +1032,7 @@ void interpolationt_word::instantiate_with_if_lifting(prop_convt &solver,
|
|||
{
|
||||
exprt tmp(expr);
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
// std::cout << "tmp is " << tmp.pretty() << std::endl;
|
||||
rewrite_ift rewrite_if(tmp);
|
||||
rewrite_if();
|
||||
|
@ -1048,7 +1048,7 @@ literalt interpolationt_word::instantiate_convert_with_if_lifting(prop_convt &so
|
|||
{
|
||||
exprt tmp(expr);
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
rewrite_ift rewrite_if(tmp);
|
||||
rewrite_if();
|
||||
|
@ -1063,7 +1063,7 @@ bool interpolationt_word::check_partition_one_implies_interpolant(const exprt &t
|
|||
|
||||
if(t.is_false()) return false;
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt solver;
|
||||
boolbvt boolbv(ns, solver);
|
||||
// boolbv.equality_propagation=false;
|
||||
|
@ -1131,7 +1131,7 @@ bool interpolationt_word::check_partition_two_and_interpolant(const exprt &t)
|
|||
|
||||
if(t.is_false()) return false;
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt solver;
|
||||
boolbvt boolbv(ns, solver);
|
||||
boolbv.equality_propagation=false;
|
||||
|
|
|
@ -106,7 +106,7 @@ int k_inductiont::induction_base()
|
|||
status("Induction Base");
|
||||
|
||||
satcheckt satcheck;
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
boolbvt solver(ns, satcheck);
|
||||
|
||||
unwind(solver, bound+1, true);
|
||||
|
@ -129,7 +129,7 @@ int k_inductiont::induction_base()
|
|||
{
|
||||
result("SAT: bug found");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
trans_tracet trans_trace;
|
||||
|
||||
compute_trans_trace(
|
||||
|
@ -186,7 +186,7 @@ int k_inductiont::induction_step()
|
|||
{
|
||||
status("Induction Step");
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
satcheckt satcheck;
|
||||
boolbvt solver(ns, satcheck);
|
||||
|
||||
|
|
|
@ -328,7 +328,7 @@ void output_verilog_rtlt::assign_symbol(
|
|||
throw 0;
|
||||
}
|
||||
|
||||
const symbolt &symbol=namespacet(context).lookup(symbol_expr);
|
||||
const symbolt &symbol=namespacet(symbol_table).lookup(symbol_expr);
|
||||
|
||||
if(symbol.is_state_var)
|
||||
{
|
||||
|
@ -378,7 +378,7 @@ void output_verilog_rtlt::convert_expr(const exprt &expr)
|
|||
expr2verilogt expr2verilog;
|
||||
|
||||
// simplify first
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
exprt tmp(expr);
|
||||
simplify(tmp,ns);
|
||||
|
||||
|
@ -459,10 +459,10 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr)
|
|||
else if(expr.id()==ID_symbol)
|
||||
{
|
||||
const irep_idt &identifier=expr.get(ID_identifier);
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
err_location(expr);
|
||||
str << "symbol " << identifier << " not found"
|
||||
|
@ -481,10 +481,10 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr)
|
|||
else if(expr.id()==ID_next_symbol)
|
||||
{
|
||||
const irep_idt &identifier=expr.get(ID_identifier);
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
err_location(expr);
|
||||
str << "symbol " << identifier << " not found"
|
||||
|
@ -654,14 +654,14 @@ void output_verilog_netlistt::latches(const irep_idt &module)
|
|||
{
|
||||
bool found=false;
|
||||
|
||||
forall_symbol_module_map(m_it, context.symbol_module_map, module)
|
||||
forall_symbol_module_map(m_it, symbol_table.symbol_module_map, module)
|
||||
{
|
||||
const irep_idt &identifier=m_it->second;
|
||||
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "failed to find symbol " << identifier
|
||||
<< std::endl;
|
||||
|
@ -705,14 +705,14 @@ void output_verilog_rtlt::latches(const irep_idt &module)
|
|||
{
|
||||
bool found=false;
|
||||
|
||||
forall_symbol_module_map(m_it, context.symbol_module_map, module)
|
||||
forall_symbol_module_map(m_it, symbol_table.symbol_module_map, module)
|
||||
{
|
||||
const irep_idt &identifier=m_it->second;
|
||||
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "failed to find symbol " << identifier
|
||||
<< std::endl;
|
||||
|
@ -753,14 +753,14 @@ void output_verilog_baset::wires(const irep_idt &module)
|
|||
{
|
||||
bool found=false;
|
||||
|
||||
forall_symbol_module_map(m_it, context.symbol_module_map, module)
|
||||
forall_symbol_module_map(m_it, symbol_table.symbol_module_map, module)
|
||||
{
|
||||
const irep_idt &identifier=m_it->second;
|
||||
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "failed to find symbol " << identifier
|
||||
<< std::endl;
|
||||
|
|
|
@ -16,11 +16,11 @@ class output_verilog_baset:public message_streamt
|
|||
{
|
||||
public:
|
||||
output_verilog_baset(
|
||||
const contextt &_context,
|
||||
const symbol_tablet &_symbol_table,
|
||||
std::ostream &_out,
|
||||
message_handlert &_message_handler):
|
||||
message_streamt(_message_handler),
|
||||
context(_context), out(_out)
|
||||
symbol_table(_symbol_table), out(_out)
|
||||
{
|
||||
}
|
||||
|
||||
|
@ -29,7 +29,7 @@ public:
|
|||
protected:
|
||||
// common
|
||||
|
||||
const contextt &context;
|
||||
const symbol_tablet &symbol_table;
|
||||
std::ostream &out;
|
||||
unsigned count;
|
||||
|
||||
|
@ -62,10 +62,10 @@ class output_verilog_netlistt:public output_verilog_baset
|
|||
{
|
||||
public:
|
||||
output_verilog_netlistt(
|
||||
const contextt &_context,
|
||||
const symbol_tablet &_symbol_table,
|
||||
std::ostream &_out,
|
||||
message_handlert &_message_handler):
|
||||
output_verilog_baset(_context, _out, _message_handler)
|
||||
output_verilog_baset(_symbol_table, _out, _message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
|
@ -90,10 +90,10 @@ class output_verilog_rtlt:public output_verilog_baset
|
|||
{
|
||||
public:
|
||||
output_verilog_rtlt(
|
||||
const contextt &_context,
|
||||
const symbol_tablet &_symbol_table,
|
||||
std::ostream &_out,
|
||||
message_handlert &_message_handler):
|
||||
output_verilog_baset(_context, _out, _message_handler)
|
||||
output_verilog_baset(_symbol_table, _out, _message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
|
@ -64,8 +64,8 @@ int ebmc_parseoptionst::doit()
|
|||
if(cmdline.isset("cegar"))
|
||||
{
|
||||
#if 0
|
||||
namespacet ns(context);
|
||||
var_mapt var_map(context, main_symbol->name);
|
||||
namespacet ns(symbol_table);
|
||||
var_mapt var_map(symbol_table, main_symbol->name);
|
||||
|
||||
bmc_cegart bmc_cegar(
|
||||
var_map,
|
||||
|
|
|
@ -90,7 +90,7 @@ Function: show_transt::show_trans_verilog_netlist
|
|||
int show_transt::show_trans_verilog_netlist(std::ostream &out)
|
||||
{
|
||||
output_verilog_netlistt output_verilog(
|
||||
context, out, get_message_handler());
|
||||
symbol_table, out, get_message_handler());
|
||||
|
||||
try
|
||||
{
|
||||
|
@ -134,7 +134,7 @@ Function: show_transt::show_trans_verilog_rtl
|
|||
int show_transt::show_trans_verilog_rtl(std::ostream &out)
|
||||
{
|
||||
output_verilog_rtlt output_verilog(
|
||||
context, out, get_message_handler());
|
||||
symbol_table, out, get_message_handler());
|
||||
|
||||
try
|
||||
{
|
||||
|
|
|
@ -19,15 +19,15 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
class gen_interfacet
|
||||
{
|
||||
public:
|
||||
gen_interfacet(contextt &_context,
|
||||
gen_interfacet(symbol_tablet &_symbol_table,
|
||||
std::ostream &_out,
|
||||
std::ostream &_err):
|
||||
context(_context), out(_out), err(_err) { }
|
||||
symbol_table(_symbol_table), out(_out), err(_err) { }
|
||||
|
||||
void gen_interface(const symbolt &module, bool have_bound);
|
||||
|
||||
protected:
|
||||
contextt &context;
|
||||
symbol_tablet &symbol_table;
|
||||
std::ostream &out, &err;
|
||||
|
||||
std::set<irep_idt> modules_done;
|
||||
|
@ -58,10 +58,10 @@ Function: gen_interfacet::lookup
|
|||
|
||||
symbolt &gen_interfacet::lookup(const irep_idt &identifier)
|
||||
{
|
||||
contextt::symbolst::iterator it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
{
|
||||
err << "failed to find identifier " << identifier << std::endl;
|
||||
throw 0;
|
||||
|
@ -215,7 +215,7 @@ void gen_interfacet::gen_module(
|
|||
std::set<irep_idt>::iterator
|
||||
in_progress_it=modules_in_progress.insert(module.name).first;
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, module.name)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, module.name)
|
||||
{
|
||||
const symbolt &symbol=lookup(it->second);
|
||||
|
||||
|
@ -233,7 +233,7 @@ void gen_interfacet::gen_module(
|
|||
|
||||
os << "struct module_" << module.base_name << " {" << std::endl;
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, module.name)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, module.name)
|
||||
{
|
||||
const symbolt &symbol=lookup(it->second);
|
||||
|
||||
|
@ -327,12 +327,12 @@ Function: gen_interfacet::gen_interface
|
|||
\*******************************************************************/
|
||||
|
||||
void gen_interface(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const symbolt &module,
|
||||
bool have_bound,
|
||||
std::ostream &out,
|
||||
std::ostream &err)
|
||||
{
|
||||
gen_interfacet gen_interface(context, out, err);
|
||||
gen_interfacet gen_interface(symbol_table, out, err);
|
||||
gen_interface.gen_interface(module, have_bound);
|
||||
}
|
||||
|
|
|
@ -11,10 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <iostream>
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
|
||||
void gen_interface(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const symbolt &module,
|
||||
bool have_bound,
|
||||
std::ostream &out,
|
||||
|
|
|
@ -16,9 +16,9 @@ class hw_bmct:public bmct
|
|||
public:
|
||||
hw_bmct(
|
||||
const optionst &_options,
|
||||
const contextt &_context,
|
||||
const symbol_tablet &_symbol_table,
|
||||
message_handlert &_message_handler):
|
||||
bmct(_options, _context, _message_handler)
|
||||
bmct(_options, _symbol_table, _message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
|
@ -60,17 +60,17 @@ void instantiate_symbol(exprt &expr, unsigned timeframe)
|
|||
class map_varst:public message_streamt
|
||||
{
|
||||
public:
|
||||
map_varst(contextt &_context, expr_listt &_constraints,
|
||||
map_varst(symbol_tablet &_symbol_table, expr_listt &_constraints,
|
||||
message_handlert &_message, unsigned _no_timeframes):
|
||||
message_streamt(_message),
|
||||
context(_context), constraints(_constraints),
|
||||
symbol_table(_symbol_table), constraints(_constraints),
|
||||
no_timeframes(_no_timeframes)
|
||||
{ }
|
||||
|
||||
void map_vars(const irep_idt &module);
|
||||
|
||||
protected:
|
||||
contextt &context;
|
||||
symbol_tablet &symbol_table;
|
||||
expr_listt &constraints;
|
||||
unsigned no_timeframes;
|
||||
std::set<irep_idt> top_level_inputs;
|
||||
|
@ -115,7 +115,7 @@ protected:
|
|||
mp_integer s;
|
||||
if(to_integer(size_expr, s))
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
str << "failed to convert array size `"
|
||||
<< from_expr(ns, "", size_expr) << "'";
|
||||
error();
|
||||
|
@ -140,10 +140,10 @@ Function: map_varst::lookup
|
|||
|
||||
symbolt &map_varst::lookup(const irep_idt &identifier)
|
||||
{
|
||||
contextt::symbolst::iterator it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "failed to find identifier `" << identifier
|
||||
<< "'";
|
||||
|
@ -239,7 +239,7 @@ bool map_varst::array_types_eq(
|
|||
return true;
|
||||
}
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
const typet &s1=ns.follow(type1.subtype());
|
||||
const typet &s2=ns.follow(type2.subtype());
|
||||
|
@ -275,7 +275,7 @@ bool map_varst::check_types_rec(
|
|||
const typet &type2,
|
||||
std::string &error_msg)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
if(type1.id()==ID_symbol)
|
||||
return check_types_rec(ns.follow(type1), type2, error_msg);
|
||||
|
@ -353,7 +353,7 @@ void map_varst::add_constraint_rec(
|
|||
const exprt &program_symbol,
|
||||
const exprt &module_symbol)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
|
||||
const typet &t1=ns.follow(program_symbol.type());
|
||||
const typet &t2=ns.follow(module_symbol.type());
|
||||
|
@ -402,7 +402,7 @@ void map_varst::map_var(
|
|||
// rhs: symbol
|
||||
exprt e2=symbol_exprt(module_symbol.name, module_symbol.type);
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
ns.follow_macros(e2);
|
||||
instantiate_symbol(e2, transition);
|
||||
|
||||
|
@ -423,7 +423,7 @@ Function: map_varst::add_array
|
|||
|
||||
const symbolt &map_varst::add_array(symbolt &symbol)
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
const typet &full_type=ns.follow(symbol.type);
|
||||
|
||||
|
@ -449,8 +449,8 @@ const symbolt &map_varst::add_array(symbolt &symbol)
|
|||
new_symbol.base_name=id2string(new_symbol.base_name)+"_array";
|
||||
|
||||
symbolt *p;
|
||||
if(context.move(new_symbol, p))
|
||||
throw "context.move() failed";
|
||||
if(symbol_table.move(new_symbol, p))
|
||||
throw "symbol_table.move() failed";
|
||||
|
||||
// change initialization
|
||||
exprt symbol_expr(ID_symbol, p->type);
|
||||
|
@ -520,7 +520,7 @@ void map_varst::map_var_rec(
|
|||
const exprt &expr,
|
||||
const symbolt::hierarchyt &hierarchy)
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
const typet &expr_type=ns.follow(expr.type());
|
||||
const struct_typet &struct_type=to_struct_type(expr_type);
|
||||
const struct_typet::componentst &components=struct_type.components();
|
||||
|
@ -546,7 +546,7 @@ void map_varst::map_var_rec(
|
|||
|
||||
std::list<const symbolt *> symbols;
|
||||
|
||||
forall_symbol_module_map(s_it, context.symbol_module_map, main_module)
|
||||
forall_symbol_module_map(s_it, symbol_table.symbol_module_map, main_module)
|
||||
{
|
||||
const symbolt &s=lookup(s_it->second);
|
||||
if(s.type.id()==ID_module) continue;
|
||||
|
@ -617,7 +617,7 @@ void map_varst::map_var(
|
|||
|
||||
// check types
|
||||
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
|
||||
const typet &type1=ns.follow(program_symbol.type());
|
||||
const typet &type2=ns.follow(module_symbol.type);
|
||||
|
@ -670,7 +670,7 @@ Function: map_varst::map_vars
|
|||
|
||||
Outputs:
|
||||
|
||||
Purpose: Looks through context for external ANSI-C symbols
|
||||
Purpose: Looks through symbol_table for external ANSI-C symbols
|
||||
Calls map_var to find mapping to HDL
|
||||
|
||||
\*******************************************************************/
|
||||
|
@ -688,14 +688,14 @@ void map_varst::map_vars(const irep_idt &module)
|
|||
timeframe_symbol.is_lvalue=true;
|
||||
timeframe_symbol.value=gen_zero(index_type());
|
||||
|
||||
context.move(timeframe_symbol);
|
||||
symbol_table.move(timeframe_symbol);
|
||||
}
|
||||
|
||||
const symbolt &module_symbol=lookup(module);
|
||||
|
||||
irep_idt struct_symbol;
|
||||
|
||||
Forall_symbols(it, context.symbols)
|
||||
Forall_symbols(it, symbol_table.symbols)
|
||||
{
|
||||
if(it->second.mode==ID_C ||
|
||||
it->second.mode==ID_cpp ||
|
||||
|
@ -739,7 +739,7 @@ void map_varst::map_vars(const irep_idt &module)
|
|||
|
||||
exprt timeframe_expr=from_integer(0, index_type());
|
||||
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
exprt expr(ID_index, ns.follow(symbol_expr.type()).subtype());
|
||||
expr.move_to_operands(symbol_expr, timeframe_expr);
|
||||
|
||||
|
@ -749,7 +749,7 @@ void map_varst::map_vars(const irep_idt &module)
|
|||
map_var_rec(module_symbol.name, expr, hierarchy);
|
||||
}
|
||||
|
||||
Forall_symbols(it, context.symbols)
|
||||
Forall_symbols(it, symbol_table.symbols)
|
||||
{
|
||||
if(it->second.mode==ID_C ||
|
||||
it->second.mode==ID_cpp ||
|
||||
|
@ -760,13 +760,13 @@ void map_varst::map_vars(const irep_idt &module)
|
|||
if(base_name=="next_timeframe" &&
|
||||
it->second.type.id()==ID_code)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
add_next_timeframe(it->second, struct_symbol, top_level_inputs, ns);
|
||||
}
|
||||
else if(base_name=="set_inputs" &&
|
||||
it->second.type.id()==ID_code)
|
||||
{
|
||||
namespacet ns(context);
|
||||
namespacet ns(symbol_table);
|
||||
add_set_inputs(it->second, struct_symbol, top_level_inputs, ns);
|
||||
}
|
||||
}
|
||||
|
@ -786,12 +786,12 @@ Function: map_vars
|
|||
\*******************************************************************/
|
||||
|
||||
void map_vars(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
expr_listt &constraints,
|
||||
message_handlert &message,
|
||||
unsigned no_timeframes)
|
||||
{
|
||||
map_varst map_vars(context, constraints, message, no_timeframes);
|
||||
map_varst map_vars(symbol_table, constraints, message, no_timeframes);
|
||||
map_vars.map_vars(module);
|
||||
}
|
||||
|
|
|
@ -11,11 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <iostream>
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <message.h>
|
||||
|
||||
void map_vars(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
expr_listt &constraints,
|
||||
message_handlert &message,
|
||||
|
|
|
@ -66,7 +66,7 @@ int hw_cbmc_parseoptionst::doit()
|
|||
if(cmdline.isset("vcd"))
|
||||
options.set_option("vcd", cmdline.getval("vcd"));
|
||||
|
||||
hw_bmct bmc(options, context, ui_message_handler);
|
||||
hw_bmct bmc(options, symbol_table, ui_message_handler);
|
||||
set_verbosity(bmc);
|
||||
set_verbosity(*this);
|
||||
|
||||
|
@ -85,7 +85,7 @@ int hw_cbmc_parseoptionst::doit()
|
|||
|
||||
if(cmdline.isset("show-claims"))
|
||||
{
|
||||
const namespacet ns(context);
|
||||
const namespacet ns(symbol_table);
|
||||
show_claims(ns, get_ui(), goto_functions);
|
||||
return 0;
|
||||
}
|
||||
|
@ -123,11 +123,11 @@ bool hw_cbmc_parseoptionst::get_modules(bmct &bmc)
|
|||
try
|
||||
{
|
||||
const symbolt &symbol=
|
||||
get_module(context, module, get_message_handler());
|
||||
get_module(symbol_table, module, get_message_handler());
|
||||
|
||||
if(cmdline.isset("gen-interface"))
|
||||
{
|
||||
gen_interface(context, symbol, true, std::cout, std::cerr);
|
||||
gen_interface(symbol_table, symbol, true, std::cout, std::cerr);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -147,7 +147,7 @@ bool hw_cbmc_parseoptionst::get_modules(bmct &bmc)
|
|||
status("Mapping variables");
|
||||
|
||||
map_vars(
|
||||
context,
|
||||
symbol_table,
|
||||
symbol.name,
|
||||
hw_bmc.bmc_constraints,
|
||||
ui_message_handler,
|
||||
|
@ -163,7 +163,7 @@ bool hw_cbmc_parseoptionst::get_modules(bmct &bmc)
|
|||
}
|
||||
else if(cmdline.isset("show-modules"))
|
||||
{
|
||||
show_modules(context, get_ui());
|
||||
show_modules(symbol_table, get_ui());
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
@ -116,11 +116,11 @@ Function: smv_languaget::typecheck
|
|||
\*******************************************************************/
|
||||
|
||||
bool smv_languaget::typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
return smv_typecheck(smv_parse_tree, context, module, message_handler);
|
||||
return smv_typecheck(smv_parse_tree, symbol_table, module, message_handler);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
|
|
@ -34,7 +34,7 @@ public:
|
|||
std::set<std::string> &module_set);
|
||||
|
||||
virtual bool typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler);
|
||||
|
||||
|
|
|
@ -26,13 +26,13 @@ class smv_typecheckt:public typecheckt
|
|||
public:
|
||||
smv_typecheckt(
|
||||
smv_parse_treet &_smv_parse_tree,
|
||||
contextt &_context,
|
||||
symbol_tablet &_symbol_table,
|
||||
const std::string &_module,
|
||||
bool _do_spec,
|
||||
message_handlert &_message_handler):
|
||||
typecheckt(_message_handler),
|
||||
smv_parse_tree(_smv_parse_tree),
|
||||
context(_context),
|
||||
symbol_table(_symbol_table),
|
||||
module(_module),
|
||||
do_spec(_do_spec)
|
||||
{
|
||||
|
@ -65,7 +65,7 @@ public:
|
|||
|
||||
protected:
|
||||
smv_parse_treet &smv_parse_tree;
|
||||
contextt &context;
|
||||
symbol_tablet &symbol_table;
|
||||
const std::string &module;
|
||||
bool do_spec;
|
||||
|
||||
|
@ -246,10 +246,10 @@ void smv_typecheckt::instantiate(
|
|||
const exprt::operandst &operands,
|
||||
const irept &location)
|
||||
{
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
err_location(location);
|
||||
str << "submodule `"
|
||||
|
@ -295,12 +295,12 @@ void smv_typecheckt::instantiate(
|
|||
|
||||
std::set<irep_idt> var_identifiers;
|
||||
|
||||
forall_symbol_module_map(v_it, context.symbol_module_map, identifier)
|
||||
forall_symbol_module_map(v_it, symbol_table.symbol_module_map, identifier)
|
||||
{
|
||||
contextt::symbolst::const_iterator s_it2=
|
||||
context.symbols.find(v_it->second);
|
||||
symbol_tablet::symbolst::const_iterator s_it2=
|
||||
symbol_table.symbols.find(v_it->second);
|
||||
|
||||
if(s_it2==context.symbols.end())
|
||||
if(s_it2==symbol_table.symbols.end())
|
||||
{
|
||||
str << "symbol `" << v_it->second << "' not found";
|
||||
throw 0;
|
||||
|
@ -325,7 +325,7 @@ void smv_typecheckt::instantiate(
|
|||
|
||||
var_identifiers.insert(symbol.name);
|
||||
|
||||
context.move(symbol);
|
||||
symbol_table.move(symbol);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -336,10 +336,10 @@ void smv_typecheckt::instantiate(
|
|||
v_it!=var_identifiers.end();
|
||||
v_it++)
|
||||
{
|
||||
contextt::symbolst::iterator s_it2=
|
||||
context.symbols.find(*v_it);
|
||||
symbol_tablet::symbolst::iterator s_it2=
|
||||
symbol_table.symbols.find(*v_it);
|
||||
|
||||
if(s_it2==context.symbols.end())
|
||||
if(s_it2==symbol_table.symbols.end())
|
||||
{
|
||||
str << "symbol `" << *v_it << "' not found";
|
||||
throw 0;
|
||||
|
@ -584,9 +584,9 @@ void smv_typecheckt::typecheck(
|
|||
if(define_map.find(identifier)!=define_map.end())
|
||||
convert_define(identifier);
|
||||
|
||||
contextt::symbolst::iterator s_it=context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator s_it=symbol_table.symbols.find(identifier);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
{
|
||||
err_location(expr);
|
||||
str << "variable `" << identifier << "' not found";
|
||||
|
@ -1173,7 +1173,7 @@ void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars)
|
|||
symbol.is_state_var=false;
|
||||
symbol.type=var.type;
|
||||
|
||||
context.add(symbol);
|
||||
symbol_table.add(symbol);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1202,9 +1202,9 @@ void smv_typecheckt::collect_define(const exprt &expr)
|
|||
|
||||
const irep_idt &identifier=op0.get(ID_identifier);
|
||||
|
||||
contextt::symbolst::iterator it=context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "collect_define failed to find symbol `"
|
||||
<< identifier << "'";
|
||||
|
@ -1253,9 +1253,9 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)
|
|||
throw 0;
|
||||
}
|
||||
|
||||
contextt::symbolst::iterator it=context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "convert_define failed to find symbol `"
|
||||
<< identifier << "'";
|
||||
|
@ -1372,7 +1372,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
|
|||
Forall_operands(it, trans)
|
||||
gen_and(*it);
|
||||
|
||||
context.move(module_symbol);
|
||||
symbol_table.move(module_symbol);
|
||||
|
||||
// spec
|
||||
|
||||
|
@ -1394,7 +1394,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
|
|||
spec_symbol.value=it->expr;
|
||||
spec_symbol.location=it->location;
|
||||
|
||||
context.move(spec_symbol);
|
||||
symbol_table.move(spec_symbol);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -1438,13 +1438,13 @@ Function: smv_typecheck
|
|||
|
||||
bool smv_typecheck(
|
||||
smv_parse_treet &smv_parse_tree,
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler,
|
||||
bool do_spec)
|
||||
{
|
||||
smv_typecheckt smv_typecheck(
|
||||
smv_parse_tree, context, module, do_spec, message_handler);
|
||||
smv_parse_tree, symbol_table, module, do_spec, message_handler);
|
||||
return smv_typecheck.typecheck_main();
|
||||
}
|
||||
|
||||
|
|
|
@ -9,14 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#ifndef CPROVER_SMV_TYPECHECK_H
|
||||
#define CPROVER_SMV_TYPECHECK_H
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <message.h>
|
||||
|
||||
#include "smv_parse_tree.h"
|
||||
|
||||
bool smv_typecheck(
|
||||
smv_parse_treet &smv_parse_tree,
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler,
|
||||
bool do_spec=true);
|
||||
|
|
|
@ -113,9 +113,9 @@ void show_state(
|
|||
std::cout << "Transition system state " << timeframe << "\n";
|
||||
std::cout << "----------------------------------------------------\n";
|
||||
|
||||
const contextt &context=ns.get_context();
|
||||
const symbol_tablet &symbol_table=ns.get_symbol_table();
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, module)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, module)
|
||||
{
|
||||
const symbolt &symbol=ns.lookup(it->second);
|
||||
|
||||
|
|
|
@ -31,11 +31,11 @@ class convert_trans_to_netlistt
|
|||
{
|
||||
public:
|
||||
convert_trans_to_netlistt(
|
||||
contextt &_context,
|
||||
symbol_tablet &_symbol_table,
|
||||
netlistt &_dest,
|
||||
messaget &_message):
|
||||
context(_context),
|
||||
ns(_context),
|
||||
symbol_table(_symbol_table),
|
||||
ns(_symbol_table),
|
||||
dest(_dest),
|
||||
message(_message)
|
||||
{
|
||||
|
@ -46,7 +46,7 @@ public:
|
|||
const std::list<exprt> &properties);
|
||||
|
||||
protected:
|
||||
contextt &context;
|
||||
symbol_tablet &symbol_table;
|
||||
const namespacet ns;
|
||||
netlistt &dest;
|
||||
messaget &message;
|
||||
|
@ -153,14 +153,14 @@ literalt convert_trans_to_netlistt::new_input()
|
|||
{
|
||||
irep_idt id="convert::input";
|
||||
|
||||
if(context.symbols.find(id)==context.symbols.end())
|
||||
if(symbol_table.symbols.find(id)==symbol_table.symbols.end())
|
||||
{
|
||||
symbolt symbol;
|
||||
symbol.name=id;
|
||||
symbol.type=bool_typet();
|
||||
symbol.is_input=true;
|
||||
symbol.base_name="input";
|
||||
context.move(symbol);
|
||||
symbol_table.move(symbol);
|
||||
}
|
||||
|
||||
var_mapt::vart &var=dest.var_map.map[id];
|
||||
|
@ -191,13 +191,13 @@ void convert_trans_to_netlistt::map_vars(
|
|||
{
|
||||
boolbv_widtht boolbv_width(ns);
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map,
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map,
|
||||
module)
|
||||
{
|
||||
contextt::symbolst::const_iterator s_it=
|
||||
context.symbols.find(it->second);
|
||||
symbol_tablet::symbolst::const_iterator s_it=
|
||||
symbol_table.symbols.find(it->second);
|
||||
|
||||
if(s_it==context.symbols.end())
|
||||
if(s_it==symbol_table.symbols.end())
|
||||
continue;
|
||||
|
||||
const symbolt &symbol=s_it->second;
|
||||
|
@ -285,7 +285,7 @@ void convert_trans_to_netlistt::operator()(
|
|||
}
|
||||
}
|
||||
|
||||
const symbolt &module_symbol=namespacet(context).lookup(module);
|
||||
const symbolt &module_symbol=namespacet(symbol_table).lookup(module);
|
||||
const transt &trans=to_trans_expr(module_symbol.value);
|
||||
|
||||
// build the net-list
|
||||
|
@ -744,13 +744,13 @@ Function: convert_trans_to_netlist
|
|||
\*******************************************************************/
|
||||
|
||||
void convert_trans_to_netlist(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
const std::list<exprt> &properties,
|
||||
netlistt &dest,
|
||||
messaget &message)
|
||||
{
|
||||
convert_trans_to_netlistt c(context, dest, message);
|
||||
convert_trans_to_netlistt c(symbol_table, dest, message);
|
||||
|
||||
c(module, properties);
|
||||
}
|
||||
|
|
|
@ -11,11 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <namespace.h>
|
||||
#include <message.h>
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <std_expr.h>
|
||||
|
||||
void convert_trans_to_netlist(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
const std::list<exprt> &properties,
|
||||
class netlistt &dest,
|
||||
|
|
|
@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#ifndef CPROVER_TRANS_PROPERTY_H
|
||||
#define CPROVER_TRANS_PROPERTY_H
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <message.h>
|
||||
#include <namespace.h>
|
||||
|
||||
|
|
|
@ -28,12 +28,12 @@ Function: show_modules
|
|||
\*******************************************************************/
|
||||
|
||||
void show_modules(
|
||||
const contextt &context,
|
||||
const symbol_tablet &symbol_table,
|
||||
ui_message_handlert::uit ui)
|
||||
{
|
||||
unsigned count=0;
|
||||
|
||||
forall_symbols(it, context.symbols)
|
||||
forall_symbols(it, symbol_table.symbols)
|
||||
{
|
||||
const symbolt &symbol=it->second;
|
||||
|
||||
|
|
|
@ -10,10 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#define CPROVER_TRANS_SHOW_MODULES_H
|
||||
|
||||
#include <ui_message.h>
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
|
||||
void show_modules(
|
||||
const contextt &context,
|
||||
const symbol_tablet &symbol_table,
|
||||
ui_message_handlert::uit ui);
|
||||
|
||||
#endif
|
||||
|
|
|
@ -117,12 +117,12 @@ void compute_trans_trace(
|
|||
|
||||
for(unsigned t=0; t<no_timeframes; t++)
|
||||
{
|
||||
const contextt &context=ns.get_context();
|
||||
const symbol_tablet &symbol_table=ns.get_symbol_table();
|
||||
|
||||
assert(t<dest.states.size());
|
||||
trans_tracet::statet &state=dest.states[t];
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, module)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, module)
|
||||
{
|
||||
const symbolt &symbol=ns.lookup(it->second);
|
||||
|
||||
|
|
|
@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <vector>
|
||||
#include <string>
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <solvers/prop/prop.h>
|
||||
|
||||
#include "bv_varid.h"
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
#include "verilog2expr.h"
|
||||
|
||||
bool verilog2expr(const string &code, exprt &expr,
|
||||
const contextt &context,
|
||||
const symbol_tablet &symbol_table,
|
||||
const sequentt &sequent,
|
||||
string &msg)
|
||||
{
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
#include "sequent.h"
|
||||
|
||||
bool verilog2expr(const string &code, exprt &expr,
|
||||
const contextt &context,
|
||||
const symbol_tablet &symbol_table,
|
||||
const sequentt &sequent,
|
||||
string &msg);
|
||||
|
||||
|
|
|
@ -6,11 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "verilog_context.h"
|
||||
#include "verilog_symbol_table.h"
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: verilog_contextt::context_lookup
|
||||
Function: verilog_symbol_tablet::symbol_table_lookup
|
||||
|
||||
Inputs:
|
||||
|
||||
|
@ -20,11 +20,11 @@ Function: verilog_contextt::context_lookup
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
symbolt &verilog_contextt::context_lookup(const irep_idt &identifier)
|
||||
symbolt &verilog_symbol_tablet::symbol_table_lookup(const irep_idt &identifier)
|
||||
{
|
||||
contextt::symbolst::iterator it=context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator it=symbol_table.symbols.find(identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
throw "symbol "+id2string(identifier)+" not found";
|
||||
|
||||
return it->second;
|
||||
|
|
|
@ -244,12 +244,12 @@ void verilog_flatteningt::flatten_inst(verilog_instt &inst)
|
|||
{
|
||||
const irep_idt &identifier=inst.get("module");
|
||||
|
||||
// must be in context
|
||||
// must be in symbol_table
|
||||
const symbolt &symbol=lookup(identifier);
|
||||
|
||||
// make sure it's flat already
|
||||
verilog_flattening(
|
||||
context, identifier, get_message_handler(), options);
|
||||
symbol_table, identifier, get_message_handler(), options);
|
||||
|
||||
assert(symbol.value.id()=="flat_verilog_module");
|
||||
|
||||
|
@ -283,7 +283,7 @@ void verilog_flatteningt::flatten_inst(
|
|||
std::list<irep_idt> new_symbols;
|
||||
replace_mapt replace_map;
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, symbol.module)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, symbol.module)
|
||||
{
|
||||
const symbolt &symbol=lookup(it->second);
|
||||
|
||||
|
@ -313,7 +313,7 @@ void verilog_flatteningt::flatten_inst(
|
|||
|
||||
new_symbol.name=full_identifier;
|
||||
|
||||
if(context.add(new_symbol))
|
||||
if(symbol_table.add(new_symbol))
|
||||
{
|
||||
str << "name collision during module instantiation: "
|
||||
<< new_symbol.name;
|
||||
|
@ -341,7 +341,7 @@ void verilog_flatteningt::flatten_inst(
|
|||
it!=new_symbols.end();
|
||||
it++)
|
||||
{
|
||||
symbolt &symbol=context_lookup(*it);
|
||||
symbolt &symbol=symbol_table_lookup(*it);
|
||||
replace_symbols(replace_map, symbol.value);
|
||||
}
|
||||
|
||||
|
@ -433,7 +433,7 @@ Function: verilog_flatteningt::typecheck
|
|||
|
||||
void verilog_flatteningt::typecheck()
|
||||
{
|
||||
symbolt &symbol=context_lookup(module);
|
||||
symbolt &symbol=symbol_table_lookup(module);
|
||||
// done already?
|
||||
if(symbol.value.id()=="flat_verilog_module") return;
|
||||
flatten_module(symbol);
|
||||
|
@ -452,12 +452,12 @@ Function: verilog_flattening
|
|||
\*******************************************************************/
|
||||
|
||||
bool verilog_flattening(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
message_handlert &message_handler,
|
||||
const optionst &options)
|
||||
{
|
||||
verilog_flatteningt verilog_flattening(
|
||||
context, module, options, message_handler);
|
||||
symbol_table, module, options, message_handler);
|
||||
return verilog_flattening.typecheck_main();
|
||||
}
|
||||
|
|
|
@ -22,10 +22,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <options.h>
|
||||
|
||||
#include "verilog_typecheck_base.h"
|
||||
#include "verilog_context.h"
|
||||
#include "verilog_symbol_table.h"
|
||||
|
||||
bool verilog_flattening(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
message_handlert &message_handler,
|
||||
const optionst &options);
|
||||
|
@ -44,17 +44,17 @@ bool verilog_flattening(
|
|||
|
||||
class verilog_flatteningt:
|
||||
public verilog_typecheck_baset,
|
||||
public verilog_contextt
|
||||
public verilog_symbol_tablet
|
||||
{
|
||||
public:
|
||||
verilog_flatteningt(
|
||||
contextt &_context,
|
||||
symbol_tablet &_symbol_table,
|
||||
const irep_idt &_module,
|
||||
const optionst &_options,
|
||||
message_handlert &_message_handler):
|
||||
verilog_typecheck_baset(ns, _message_handler),
|
||||
verilog_contextt(_context),
|
||||
ns(_context),
|
||||
verilog_symbol_tablet(_symbol_table),
|
||||
ns(_symbol_table),
|
||||
options(_options),
|
||||
module(_module)
|
||||
{
|
||||
|
|
|
@ -138,7 +138,7 @@ void verilog_typecheckt::interface_ports(irept::subt &ports)
|
|||
|
||||
symbolt *s;
|
||||
|
||||
if(context.move(new_symbol, s))
|
||||
if(symbol_table.move(new_symbol, s))
|
||||
{
|
||||
err_location(decl.op0());
|
||||
str << "port `" << name << "' is also declared";
|
||||
|
@ -211,7 +211,7 @@ void verilog_typecheckt::interface_function_or_task(
|
|||
id2string(symbol.module)+"."+
|
||||
id2string(symbol.base_name);
|
||||
|
||||
if(context.move(symbol, new_symbol))
|
||||
if(symbol_table.move(symbol, new_symbol))
|
||||
{
|
||||
err_location(decl);
|
||||
str << "symbol `" << symbol.base_name
|
||||
|
@ -239,7 +239,7 @@ void verilog_typecheckt::interface_function_or_task(
|
|||
id2string(new_symbol->name)+"."+
|
||||
id2string(new_symbol->base_name);
|
||||
|
||||
context.move(return_symbol);
|
||||
symbol_table.move(return_symbol);
|
||||
}
|
||||
|
||||
// do the declarations within the task/function
|
||||
|
@ -377,9 +377,9 @@ void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &de
|
|||
|
||||
if(input || output)
|
||||
{
|
||||
contextt::symbolst::iterator s_it=
|
||||
context.symbols.find(function_or_task_name);
|
||||
assert(s_it!=context.symbols.end());
|
||||
symbol_tablet::symbolst::iterator s_it=
|
||||
symbol_table.symbols.find(function_or_task_name);
|
||||
assert(s_it!=symbol_table.symbols.end());
|
||||
symbolt &function_or_task_symbol=s_it->second;
|
||||
code_typet::argumentst &arguments=
|
||||
to_code_type(function_or_task_symbol.type).arguments();
|
||||
|
@ -392,10 +392,10 @@ void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &de
|
|||
argument.set(ID_input, input);
|
||||
}
|
||||
|
||||
contextt::symbolst::iterator result=
|
||||
context.symbols.find(symbol.name);
|
||||
symbol_tablet::symbolst::iterator result=
|
||||
symbol_table.symbols.find(symbol.name);
|
||||
|
||||
if(result!=context.symbols.end())
|
||||
if(result!=symbol_table.symbols.end())
|
||||
{
|
||||
err_location(decl);
|
||||
str << "symbol `" << symbol.base_name
|
||||
|
@ -403,7 +403,7 @@ void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &de
|
|||
throw 0;
|
||||
}
|
||||
|
||||
context.add(symbol);
|
||||
symbol_table.add(symbol);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -527,11 +527,11 @@ void verilog_typecheckt::interface_module_decl(const verilog_declt &decl)
|
|||
id2string(symbol.module)+"."+
|
||||
id2string(symbol.base_name);
|
||||
|
||||
contextt::symbolst::iterator result=
|
||||
context.symbols.find(symbol.name);
|
||||
symbol_tablet::symbolst::iterator result=
|
||||
symbol_table.symbols.find(symbol.name);
|
||||
|
||||
if(result==context.symbols.end())
|
||||
context.add(symbol);
|
||||
if(result==symbol_table.symbols.end())
|
||||
symbol_table.add(symbol);
|
||||
else
|
||||
{
|
||||
symbolt &osymbol=result->second;
|
||||
|
@ -604,7 +604,7 @@ void verilog_typecheckt::interface_parameter(const exprt &expr)
|
|||
|
||||
symbolt *new_symbol;
|
||||
|
||||
if(context.move(symbol, new_symbol))
|
||||
if(symbol_table.move(symbol, new_symbol))
|
||||
{
|
||||
err_location(expr);
|
||||
str << "conflicting definition of symbol `"
|
||||
|
@ -691,7 +691,7 @@ void verilog_typecheckt::interface_inst(
|
|||
id2string(symbol.base_name);
|
||||
symbol.value.set(ID_module, identifier);
|
||||
|
||||
if(context.add(symbol))
|
||||
if(symbol_table.add(symbol))
|
||||
{
|
||||
err_location(op);
|
||||
str << "duplicate definition of identifier `"
|
||||
|
|
|
@ -156,18 +156,18 @@ Function: verilog_languaget::typecheck
|
|||
\*******************************************************************/
|
||||
|
||||
bool verilog_languaget::typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
if(module=="") return false;
|
||||
|
||||
if(verilog_typecheck(parse_tree, context, module, message_handler))
|
||||
if(verilog_typecheck(parse_tree, symbol_table, module, message_handler))
|
||||
return true;
|
||||
|
||||
message_handler.print(9, "Synthesis");
|
||||
|
||||
if(verilog_synthesis(context, module, message_handler, options))
|
||||
if(verilog_synthesis(symbol_table, module, message_handler, options))
|
||||
return true;
|
||||
|
||||
return false;
|
||||
|
@ -186,7 +186,7 @@ Function: verilog_languaget::interfaces
|
|||
\*******************************************************************/
|
||||
|
||||
bool verilog_languaget::interfaces(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
return false;
|
||||
|
|
|
@ -36,11 +36,11 @@ public:
|
|||
std::set<std::string> &module_set);
|
||||
|
||||
virtual bool interfaces(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
message_handlert &message_handler);
|
||||
|
||||
virtual bool typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler);
|
||||
|
||||
|
|
|
@ -131,10 +131,10 @@ void verilog_typecheckt::module_instance(
|
|||
|
||||
// find base symbol
|
||||
|
||||
contextt::symbolst::const_iterator it=
|
||||
context.symbols.find(module_identifier);
|
||||
symbol_tablet::symbolst::const_iterator it=
|
||||
symbol_table.symbols.find(module_identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
{
|
||||
err_location(location);
|
||||
str << "module not found" << std::endl;
|
||||
|
@ -175,8 +175,8 @@ void verilog_typecheckt::module_instance(
|
|||
|
||||
module_identifier+=suffix;
|
||||
|
||||
if(context.symbols.find(module_identifier)!=
|
||||
context.symbols.end())
|
||||
if(symbol_table.symbols.find(module_identifier)!=
|
||||
symbol_table.symbols.end())
|
||||
return; // done already
|
||||
|
||||
// create symbol
|
||||
|
@ -194,11 +194,11 @@ void verilog_typecheckt::module_instance(
|
|||
// throw away old stuff
|
||||
symbol.value.clear();
|
||||
|
||||
// put symbol in context
|
||||
// put symbol in symbol_table
|
||||
|
||||
symbolt *new_symbol;
|
||||
|
||||
if(context.move(symbol, new_symbol))
|
||||
if(symbol_table.move(symbol, new_symbol))
|
||||
{
|
||||
err_location(location);
|
||||
str << "duplicate definition of module "
|
||||
|
@ -208,7 +208,7 @@ void verilog_typecheckt::module_instance(
|
|||
|
||||
// recursive call
|
||||
|
||||
verilog_typecheckt verilog_typecheck(*new_symbol, context, get_message_handler());
|
||||
verilog_typecheckt verilog_typecheck(*new_symbol, symbol_table, get_message_handler());
|
||||
|
||||
if(verilog_typecheck.typecheck_main())
|
||||
throw 0;
|
||||
|
|
|
@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#ifndef CPROVER_VERILOG_CONTEXT_H
|
||||
#define CPROVER_VERILOG_CONTEXT_H
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Class: verilog_contextt
|
||||
Class: verilog_symbol_tablet
|
||||
|
||||
Inputs:
|
||||
|
||||
|
@ -23,16 +23,16 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
\*******************************************************************/
|
||||
|
||||
class verilog_contextt
|
||||
class verilog_symbol_tablet
|
||||
{
|
||||
public:
|
||||
verilog_contextt(contextt &_context):context(_context)
|
||||
verilog_symbol_tablet(symbol_tablet &_symbol_table):symbol_table(_symbol_table)
|
||||
{
|
||||
}
|
||||
|
||||
protected:
|
||||
contextt &context;
|
||||
symbolt &context_lookup(const irep_idt &identifier);
|
||||
symbol_tablet &symbol_table;
|
||||
symbolt &symbol_table_lookup(const irep_idt &identifier);
|
||||
};
|
||||
|
||||
#endif
|
|
@ -557,7 +557,7 @@ void verilog_synthesist::replace_by_wire(
|
|||
new_symbol.name=id2string(base.name)+"_"+i2string(c);
|
||||
new_symbol.base_name=id2string(base.base_name)+"_"+i2string(c);
|
||||
}
|
||||
while(context.symbols.find(new_symbol.name)!=context.symbols.end());
|
||||
while(symbol_table.symbols.find(new_symbol.name)!=symbol_table.symbols.end());
|
||||
|
||||
new_symbol.type=what.type();
|
||||
new_symbol.module=base.module;
|
||||
|
@ -571,7 +571,7 @@ void verilog_synthesist::replace_by_wire(
|
|||
assignment.next.value=what;
|
||||
new_wires.insert(new_symbol.name);
|
||||
|
||||
if(context.move(new_symbol))
|
||||
if(symbol_table.move(new_symbol))
|
||||
throw "failed to add replace_by_wire symbol";
|
||||
|
||||
what=symbol_expr;
|
||||
|
@ -774,10 +774,10 @@ symbolt &verilog_synthesist::assignment_symbol(const exprt &lhs)
|
|||
|
||||
const irep_idt &identifier=e->get(ID_identifier);
|
||||
|
||||
contextt::symbolst::iterator it=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator it=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(it==context.symbols.end())
|
||||
if(it==symbol_table.symbols.end())
|
||||
{
|
||||
str << "assignment failed to find symbol `"
|
||||
<< identifier
|
||||
|
@ -981,12 +981,12 @@ void verilog_synthesist::synth_inst(
|
|||
{
|
||||
const irep_idt &identifier=statement.get(ID_module);
|
||||
|
||||
// must be in context
|
||||
// must be in symbol_table
|
||||
const symbolt &symbol=lookup(identifier);
|
||||
|
||||
// make sure it's synthesized already
|
||||
verilog_synthesis(
|
||||
context, identifier, get_message_handler(), options);
|
||||
symbol_table, identifier, get_message_handler(), options);
|
||||
|
||||
forall_operands(it, statement)
|
||||
expand_inst(symbol, *it, trans);
|
||||
|
@ -1191,7 +1191,7 @@ void verilog_synthesist::expand_inst(
|
|||
|
||||
std::list<irep_idt> new_symbols;
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, symbol.module)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, symbol.module)
|
||||
{
|
||||
const symbolt &symbol=lookup(it->second);
|
||||
|
||||
|
@ -1219,7 +1219,7 @@ void verilog_synthesist::expand_inst(
|
|||
|
||||
new_symbol.name=full_identifier;
|
||||
|
||||
if(context.add(new_symbol))
|
||||
if(symbol_table.add(new_symbol))
|
||||
{
|
||||
str << "name collision during module instantiation: "
|
||||
<< new_symbol.name << std::endl;
|
||||
|
@ -1244,7 +1244,7 @@ void verilog_synthesist::expand_inst(
|
|||
it!=new_symbols.end();
|
||||
it++)
|
||||
{
|
||||
symbolt &symbol=context_lookup(*it);
|
||||
symbolt &symbol=symbol_table_lookup(*it);
|
||||
replace_symbols(replace_map, symbol.value);
|
||||
}
|
||||
|
||||
|
@ -1652,7 +1652,7 @@ void verilog_synthesist::synth_assert(
|
|||
}
|
||||
|
||||
const irep_idt &identifier=statement.get(ID_identifier);
|
||||
symbolt &symbol=context_lookup(identifier);
|
||||
symbolt &symbol=symbol_table_lookup(identifier);
|
||||
|
||||
synth_expr(symbol.value, S_CURRENT);
|
||||
}
|
||||
|
@ -1679,7 +1679,7 @@ void verilog_synthesist::synth_assert_module_item(
|
|||
}
|
||||
|
||||
const irep_idt &identifier=module_item.get(ID_identifier);
|
||||
symbolt &symbol=context_lookup(identifier);
|
||||
symbolt &symbol=symbol_table_lookup(identifier);
|
||||
|
||||
construct=C_OTHER;
|
||||
|
||||
|
@ -2098,9 +2098,9 @@ void verilog_synthesist::synth_event_guard(
|
|||
|
||||
irep_idt identifier="conf::clock_enable_mode";
|
||||
|
||||
// check context for clock guard
|
||||
// check symbol_table for clock guard
|
||||
|
||||
if(context.symbols.find(identifier)!=context.symbols.end())
|
||||
if(symbol_table.symbols.find(identifier)!=symbol_table.symbols.end())
|
||||
{
|
||||
// found! we make it a guard
|
||||
|
||||
|
@ -2616,7 +2616,7 @@ void verilog_synthesist::synth_assignments(transt &trans)
|
|||
it!=local_symbols.end();
|
||||
it++)
|
||||
{
|
||||
symbolt &symbol=context_lookup(*it);
|
||||
symbolt &symbol=symbol_table_lookup(*it);
|
||||
|
||||
if(symbol.is_state_var && !symbol.is_macro)
|
||||
{
|
||||
|
@ -2656,7 +2656,7 @@ void verilog_synthesist::synth_assignments(transt &trans)
|
|||
it!=new_wires.end();
|
||||
it++)
|
||||
{
|
||||
symbolt &symbol=context_lookup(*it);
|
||||
symbolt &symbol=symbol_table_lookup(*it);
|
||||
assignmentt &assignment=assignments[symbol.name];
|
||||
|
||||
synth_assignments(symbol, CURRENT,
|
||||
|
@ -2853,7 +2853,7 @@ void verilog_synthesist::convert_module_items(symbolt &symbol)
|
|||
|
||||
// find out about symbols of this module
|
||||
|
||||
forall_symbol_module_map(it, context.symbol_module_map, module)
|
||||
forall_symbol_module_map(it, symbol_table.symbol_module_map, module)
|
||||
local_symbols.insert(it->second);
|
||||
|
||||
// do the module items
|
||||
|
@ -2912,7 +2912,7 @@ Function: verilog_synthesist::typecheck
|
|||
|
||||
void verilog_synthesist::typecheck()
|
||||
{
|
||||
symbolt &symbol=context_lookup(module);
|
||||
symbolt &symbol=symbol_table_lookup(module);
|
||||
if(symbol.value.id()==ID_trans) return; // done already
|
||||
convert_module_items(symbol);
|
||||
}
|
||||
|
@ -2930,12 +2930,12 @@ Function: verilog_synthesis
|
|||
\*******************************************************************/
|
||||
|
||||
bool verilog_synthesis(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
message_handlert &message_handler,
|
||||
const optionst &options)
|
||||
{
|
||||
verilog_synthesist verilog_synthesis(
|
||||
context, module, options, message_handler);
|
||||
symbol_table, module, options, message_handler);
|
||||
return verilog_synthesis.typecheck_main();
|
||||
}
|
||||
|
|
|
@ -21,10 +21,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <std_expr.h>
|
||||
|
||||
#include "verilog_typecheck_base.h"
|
||||
#include "verilog_context.h"
|
||||
#include "verilog_symbol_table.h"
|
||||
|
||||
bool verilog_synthesis(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const irep_idt &module,
|
||||
message_handlert &message_handler,
|
||||
const optionst &options);
|
||||
|
@ -43,17 +43,17 @@ bool verilog_synthesis(
|
|||
|
||||
class verilog_synthesist:
|
||||
public verilog_typecheck_baset,
|
||||
public verilog_contextt
|
||||
public verilog_symbol_tablet
|
||||
{
|
||||
public:
|
||||
verilog_synthesist(
|
||||
contextt &_context,
|
||||
symbol_tablet &_symbol_table,
|
||||
const irep_idt &_module,
|
||||
const optionst &_options,
|
||||
message_handlert &_message_handler):
|
||||
verilog_typecheck_baset(ns, _message_handler),
|
||||
verilog_contextt(_context),
|
||||
ns(_context),
|
||||
verilog_symbol_tablet(_symbol_table),
|
||||
ns(_symbol_table),
|
||||
options(_options),
|
||||
value_map(NULL),
|
||||
module(_module),
|
||||
|
|
|
@ -284,14 +284,14 @@ void verilog_typecheckt::convert_function_or_task(verilog_declt &decl)
|
|||
id2string(module_identifier)+"."+
|
||||
id2string(decl.get_identifier());
|
||||
|
||||
contextt::symbolst::iterator result=
|
||||
context.symbols.find(identifier);
|
||||
symbol_tablet::symbolst::iterator result=
|
||||
symbol_table.symbols.find(identifier);
|
||||
|
||||
if(result==context.symbols.end())
|
||||
if(result==symbol_table.symbols.end())
|
||||
{
|
||||
err_location(decl);
|
||||
str << "expected to find " << decl_class << " symbol `"
|
||||
<< identifier << "' in context";
|
||||
<< identifier << "' in symbol_table";
|
||||
throw 0;
|
||||
}
|
||||
|
||||
|
@ -369,7 +369,7 @@ void verilog_typecheckt::convert_decl(verilog_declt &decl)
|
|||
|
||||
lhs.set(ID_identifier, identifier);
|
||||
|
||||
symbolt &symbol=context_lookup(identifier);
|
||||
symbolt &symbol=symbol_table_lookup(identifier);
|
||||
convert_expr(rhs);
|
||||
propagate_type(rhs, symbol.type);
|
||||
lhs.type()=symbol.type;
|
||||
|
@ -861,8 +861,8 @@ void verilog_typecheckt::convert_assert(exprt &statement)
|
|||
id2string(module_identifier)+
|
||||
".property."+id2string(base_name);
|
||||
|
||||
if(context.symbols.find(full_identifier)!=
|
||||
context.symbols.end())
|
||||
if(symbol_table.symbols.find(full_identifier)!=
|
||||
symbol_table.symbols.end())
|
||||
{
|
||||
err_location(statement);
|
||||
str << "property identifier `" << base_name << "' already used";
|
||||
|
@ -884,7 +884,7 @@ void verilog_typecheckt::convert_assert(exprt &statement)
|
|||
symbol.location=statement.find_location();
|
||||
|
||||
symbolt *new_symbol;
|
||||
context.move(symbol, new_symbol);
|
||||
symbol_table.move(symbol, new_symbol);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
@ -1398,7 +1398,7 @@ bool verilog_typecheckt::implicit_wire(
|
|||
symbol.type=typet(ID_bool); // TODO: other types?
|
||||
|
||||
symbolt *new_symbol;
|
||||
context.move(symbol, new_symbol);
|
||||
symbol_table.move(symbol, new_symbol);
|
||||
symbol_ptr=new_symbol;
|
||||
|
||||
return false;
|
||||
|
@ -1436,7 +1436,7 @@ Function: verilog_typecheck
|
|||
|
||||
bool verilog_typecheck(
|
||||
const verilog_parse_treet &parse_tree,
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
|
@ -1452,7 +1452,7 @@ bool verilog_typecheck(
|
|||
return true;
|
||||
}
|
||||
|
||||
return verilog_typecheck(context, it->second->verilog_module, message_handler);
|
||||
return verilog_typecheck(symbol_table, it->second->verilog_module, message_handler);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
@ -1468,7 +1468,7 @@ Function: verilog_typecheck
|
|||
\*******************************************************************/
|
||||
|
||||
bool verilog_typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const verilog_modulet &verilog_module,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
|
@ -1487,11 +1487,11 @@ bool verilog_typecheck(
|
|||
|
||||
symbol.type.add(ID_module_source)=verilog_module.to_irep();
|
||||
|
||||
// put symbol in context
|
||||
// put symbol in symbol_table
|
||||
|
||||
symbolt *new_symbol;
|
||||
|
||||
if(context.move(symbol, new_symbol))
|
||||
if(symbol_table.move(symbol, new_symbol))
|
||||
{
|
||||
message_streamt message_stream(message_handler);
|
||||
message_stream.str << "duplicate definition of module "
|
||||
|
@ -1500,6 +1500,6 @@ bool verilog_typecheck(
|
|||
throw 0;
|
||||
}
|
||||
|
||||
verilog_typecheckt verilog_typecheck(*new_symbol, context, message_handler);
|
||||
verilog_typecheckt verilog_typecheck(*new_symbol, symbol_table, message_handler);
|
||||
return verilog_typecheck.typecheck_main();
|
||||
}
|
||||
|
|
|
@ -10,28 +10,28 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#define CPROVER_VERILOG_TYPECHECK_H
|
||||
|
||||
#include <hash_cont.h>
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <typecheck.h>
|
||||
#include <mp_arith.h>
|
||||
#include <replace_expr.h>
|
||||
|
||||
#include "verilog_typecheck_expr.h"
|
||||
#include "verilog_parse_tree.h"
|
||||
#include "verilog_context.h"
|
||||
#include "verilog_symbol_table.h"
|
||||
|
||||
bool verilog_typecheck(
|
||||
const verilog_parse_treet &parse_tree,
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler);
|
||||
|
||||
bool verilog_typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const verilog_modulet &verilog_module,
|
||||
message_handlert &message_handler);
|
||||
|
||||
bool verilog_typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module_identifier,
|
||||
const exprt::operandst ¶meters,
|
||||
message_handlert &message_handler);
|
||||
|
@ -50,16 +50,16 @@ bool verilog_typecheck(
|
|||
|
||||
class verilog_typecheckt:
|
||||
public verilog_typecheck_exprt,
|
||||
public verilog_contextt
|
||||
public verilog_symbol_tablet
|
||||
{
|
||||
public:
|
||||
verilog_typecheckt(
|
||||
symbolt &_module_symbol,
|
||||
contextt &_context,
|
||||
symbol_tablet &_symbol_table,
|
||||
message_handlert &_message_handler):
|
||||
verilog_typecheck_exprt(ns, _message_handler),
|
||||
verilog_contextt(_context),
|
||||
ns(_context),
|
||||
verilog_symbol_tablet(_symbol_table),
|
||||
ns(_symbol_table),
|
||||
module_symbol(_module_symbol),
|
||||
assertion_counter(0)
|
||||
{}
|
||||
|
|
|
@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#ifndef CPROVER_VERILOG_TYPECHEK_BASE_H
|
||||
#define CPROVER_VERILOG_TYPECHEK_BASE_H
|
||||
|
||||
#include <context.h>
|
||||
#include <symbol_table.h>
|
||||
#include <typecheck.h>
|
||||
#include <mp_arith.h>
|
||||
#include <namespace_utils.h>
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
#include "vhdl2expr.h"
|
||||
|
||||
bool vhdl2expr(const string &code, exprt &expr,
|
||||
const contextt &context,
|
||||
const symbol_tablet &symbol_table,
|
||||
const sequentt &sequent,
|
||||
string &msg)
|
||||
{
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
#include "sequent.h"
|
||||
|
||||
bool vhdl2expr(const string &code, exprt &expr,
|
||||
const contextt &context,
|
||||
const symbol_tablet &symbol_table,
|
||||
const sequentt &sequent,
|
||||
string &msg);
|
||||
|
||||
|
|
|
@ -148,19 +148,19 @@ Function: vhdl_languaget::typecheck
|
|||
\*******************************************************************/
|
||||
|
||||
bool vhdl_languaget::typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
if(module=="") return false;
|
||||
|
||||
#if 0
|
||||
if(vhdl_typecheck(parse_tree, context, module, message_handler))
|
||||
if(vhdl_typecheck(parse_tree, symbol_table, module, message_handler))
|
||||
return true;
|
||||
|
||||
message_handler.print(9, "Synthesis");
|
||||
|
||||
if(vhdl_synthesis(context, module, message_handler, options))
|
||||
if(vhdl_synthesis(symbol_table, module, message_handler, options))
|
||||
return true;
|
||||
#endif
|
||||
|
||||
|
@ -180,7 +180,7 @@ Function: vhdl_languaget::interfaces
|
|||
\*******************************************************************/
|
||||
|
||||
bool vhdl_languaget::interfaces(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
message_handlert &message_handler)
|
||||
{
|
||||
return false;
|
||||
|
|
|
@ -36,11 +36,11 @@ public:
|
|||
std::set<std::string> &module_set);
|
||||
|
||||
virtual bool interfaces(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
message_handlert &message_handler);
|
||||
|
||||
virtual bool typecheck(
|
||||
contextt &context,
|
||||
symbol_tablet &symbol_table,
|
||||
const std::string &module,
|
||||
message_handlert &message_handler);
|
||||
|
||||
|
|
|
@ -9,9 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#ifndef CPROVER_VHDL_TYPECHECK_H
|
||||
#define CPROVER_VHDL_TYPECHECK_H
|
||||
|
||||
#include "context.h"
|
||||
#include "symbol_table.h"
|
||||
|
||||
bool convert_vhdl(void *root, contextt &context, std::string &error);
|
||||
bool convert_vhdl(void *root, symbol_tablet &symbol_table, std::string &error);
|
||||
|
||||
#endif
|
||||
|
||||
|
|
Loading…
Reference in New Issue