Skip to content

Commit

Permalink
smv_typecheckt: use errort()
Browse files Browse the repository at this point in the history 
This replaces instances of "throw 0;" by "throw errort()".
  • Loading branch information
@kroening
kroening committed Dec 24, 2024
1 parent d5bb9c8 commit 401bbf4
Showing 1 changed file with 64 additions and 96 deletions.
160 changes: 64 additions & 96 deletions src/smvlang/smv_typecheck.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -221,20 +221,14 @@ void smv_typecheckt::instantiate(

if(s_it==symbol_table.symbols.end())
{
error().source_location=location;
error() << "submodule `"
<< identifier
<< "' not found" << eom;
throw 0;
throw errort().with_location(location)
<< "submodule `" << identifier << "' not found";
}

if(s_it->second.type.id()!=ID_module)
{
error().source_location=location;
error() << "submodule `"
<< identifier
<< "' not a module" << eom;
throw 0;
throw errort().with_location(location)
<< "submodule `" << identifier << "' not a module";
}

const irept::subt &ports=s_it->second.type.find(ID_ports).get_sub();
Expand All @@ -243,10 +237,8 @@ void smv_typecheckt::instantiate(

if(ports.size()!=operands.size())
{
error().source_location=location;
error() << "submodule `" << identifier
<< "' has wrong number of arguments" << eom;
throw 0;
throw errort().with_location(location)
<< "submodule `" << identifier << "' has wrong number of arguments";
}

std::set<irep_idt> port_identifiers;
Expand Down Expand Up @@ -275,12 +267,14 @@ void smv_typecheckt::instantiate(

if(s_it2==symbol_table.symbols.end())
{
error() << "symbol `" << v_it->second << "' not found" << eom;
throw 0;
throw errort() << "symbol `" << v_it->second << "' not found";
}

if (port_identifiers.find(s_it2->first) != port_identifiers.end()) {
} else if (s_it2->second.type.id() == ID_module) {
if(port_identifiers.find(s_it2->first) != port_identifiers.end())
{
}
else if(s_it2->second.type.id() == ID_module)
{
}
else
{
Expand Down Expand Up @@ -316,8 +310,7 @@ void smv_typecheckt::instantiate(

if(s_it2==nullptr)
{
error() << "symbol `" << v_id << "' not found" << eom;
throw 0;
throw errort() << "symbol `" << v_id << "' not found";
}

symbolt &symbol=*s_it2;
Expand Down Expand Up @@ -400,10 +393,9 @@ void smv_typecheckt::instantiate_rename(
}
else
{
error().source_location=expr.find_source_location();
error() << "expected symbol expression here, but got "
<< to_string(it->second) << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "expected symbol expression here, but got "
<< to_string(it->second);
}
}
else
Expand Down Expand Up @@ -431,10 +423,8 @@ void smv_typecheckt::typecheck_op(
{
if(expr.operands().size()==0)
{
error().source_location=expr.find_source_location();
error() << "Expected operands for " << expr.id()
<< " operator" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected operands for " << expr.id() << " operator";
}

for(auto &op : expr.operands())
Expand Down Expand Up @@ -497,9 +487,8 @@ smv_ranget smv_typecheckt::convert_type(const typet &src)
}
else
{
error().source_location=src.source_location();
error() << "Unexpected type: `" << to_string(src) << "'" << eom;
throw 0;
throw errort().with_location(src.source_location())
<< "Unexpected type: `" << to_string(src) << "'";
}

return dest;
Expand Down Expand Up @@ -589,9 +578,8 @@ void smv_typecheckt::typecheck(

if(s_it==nullptr)
{
error().source_location=expr.find_source_location();
error() << "variable `" << identifier << "' not found" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "variable `" << identifier << "' not found";
}

symbolt &symbol=*s_it;
Expand Down Expand Up @@ -647,9 +635,8 @@ void smv_typecheckt::typecheck(
{
if(expr.operands().size()!=2)
{
error().source_location=expr.find_source_location();
error() << "Expected two operands for -> operator" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected two operands for -> operator";
}

typecheck_op(expr, bool_typet(), mode);
Expand All @@ -663,9 +650,8 @@ void smv_typecheckt::typecheck(

if(expr.operands().size()!=2)
{
error().source_location=expr.find_source_location();
error() << "Expected two operands for " << expr.id() << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected two operands for " << expr.id();
}

expr.type()=bool_typet();
Expand All @@ -684,9 +670,8 @@ void smv_typecheckt::typecheck(
{
if(op0.type().id()!=ID_range)
{
error().source_location=expr.find_source_location();
error() << "Expected number type for " << to_string(expr) << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected number type for " << to_string(expr);
}
}
}
Expand All @@ -708,9 +693,8 @@ void smv_typecheckt::typecheck(

if(expr.operands().size()!=2)
{
error().source_location=expr.find_source_location();
error() << "Expected two operands for " << expr.id() << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected two operands for " << expr.id();
}

if(type.is_nil())
Expand Down Expand Up @@ -742,9 +726,8 @@ void smv_typecheckt::typecheck(
}
else if(type.id()!=ID_range)
{
error().source_location=expr.find_source_location();
error() << "Expected number type for " << to_string(expr) << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected number type for " << to_string(expr);
}
}
else if(expr.id()==ID_constant)
Expand Down Expand Up @@ -772,9 +755,8 @@ void smv_typecheckt::typecheck(
expr=true_exprt();
else
{
error().source_location=expr.find_source_location();
error() << "expected 0 or 1 here, but got " << value << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "expected 0 or 1 here, but got " << value;
}
}
else if(type.id()==ID_range)
Expand All @@ -783,17 +765,15 @@ void smv_typecheckt::typecheck(

if(int_value<smv_range.from || int_value>smv_range.to)
{
error().source_location=expr.find_source_location();
error() << "expected " << smv_range.from << ".." << smv_range.to
<< " here, but got " << value << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "expected " << smv_range.from << ".." << smv_range.to
<< " here, but got " << value;
}
}
else
{
error().source_location=expr.find_source_location();
error() << "Unexpected constant: " << value << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Unexpected constant: " << value;
}
}
}
Expand Down Expand Up @@ -936,9 +916,8 @@ void smv_typecheckt::typecheck(
}
else
{
error().source_location=expr.find_source_location();
error() << "No type checking for " << expr.id() << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "No type checking for " << expr.id();
}

if(!type.is_nil() && expr.type()!=type)
Expand Down Expand Up @@ -969,12 +948,10 @@ void smv_typecheckt::typecheck(
return;
}

error().source_location=expr.find_source_location();
error() << "Expected expression of type `" << to_string(type)
<< "', but got expression `" << to_string(expr)
<< "', which is of type `" << to_string(expr.type())
<< "'" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected expression of type `" << to_string(type)
<< "', but got expression `" << to_string(expr) << "', which is of type `"
<< to_string(expr.type()) << "'";
}
}

Expand All @@ -996,9 +973,8 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
{
if(expr_mode!=NORMAL)
{
error().source_location=expr.find_source_location();
error() << "next(next(...)) encountered" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "next(next(...)) encountered";
}

assert(expr.operands().size()==1);
Expand Down Expand Up @@ -1044,9 +1020,8 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
{
if(expr.operands().size()==0)
{
error().source_location=expr.find_source_location();
error() << "expected operand here" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "expected operand here";
}

std::string identifier=
Expand All @@ -1061,10 +1036,8 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
{
if(expr.operands().size()<1)
{
error().source_location=expr.find_source_location();
error() << "Expected at least one operand for " << expr.id()
<< " expression" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "Expected at least one operand for " << expr.id() << " expression";
}

exprt tmp;
Expand All @@ -1075,8 +1048,8 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
{
if(op.operands().size() != 2)
{
error().source_location = op.find_source_location();
throw "case expected to have two operands";
throw errort().with_location(op.find_source_location())
<< "case expected to have two operands";
}

exprt &condition = to_binary_expr(op).op0();
Expand Down Expand Up @@ -1254,23 +1227,22 @@ Function: smv_typecheckt::collect_define
void smv_typecheckt::collect_define(const exprt &expr)
{
if(expr.id()!=ID_equal || expr.operands().size()!=2)
throw "collect_define expects equality";
throw errort() << "collect_define expects equality";

const exprt &op0 = to_equal_expr(expr).op0();
const exprt &op1 = to_equal_expr(expr).op1();

if(op0.id()!=ID_symbol)
throw "collect_define expects symbol on left hand side";
throw errort() << "collect_define expects symbol on left hand side";

const irep_idt &identifier=op0.get(ID_identifier);
const irep_idt &identifier = to_symbol_expr(op0).get_identifier();

auto it=symbol_table.get_writeable(identifier);

if(it==nullptr)
{
error() << "collect_define failed to find symbol `"
<< identifier << "'" << eom;
throw 0;
throw errort() << "collect_define failed to find symbol `" << identifier
<< "'";
}

symbolt &symbol=*it;
Expand All @@ -1285,9 +1257,8 @@ void smv_typecheckt::collect_define(const exprt &expr)

if(!result.second)
{
error().source_location=expr.find_source_location();
error() << "symbol `" << identifier << "' defined twice" << eom;
throw 0;
throw errort().with_location(expr.find_source_location())
<< "symbol `" << identifier << "' defined twice";
}
}

Expand All @@ -1311,17 +1282,15 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)

if(d.in_progress)
{
error() << "definition of `" << identifier << "' is cyclic" << eom;
throw 0;
throw errort() << "definition of `" << identifier << "' is cyclic";
}

auto it=symbol_table.get_writeable(identifier);

if(it==nullptr)
{
error() << "convert_define failed to find symbol `"
<< identifier << "'" << eom;
throw 0;
throw errort() << "convert_define failed to find symbol `" << identifier
<< "'";
}

symbolt &symbol=*it;
Expand Down Expand Up @@ -1491,8 +1460,7 @@ void smv_typecheckt::typecheck()

if(it==smv_parse_tree.modules.end())
{
error() << "failed to find module " << module << eom;
throw 0;
throw errort() << "failed to find module " << module;
}

convert(it->second);
Expand Down

0 comments on commit 401bbf4

Please sign in to comment.