Skip to content

Cleanup expression/code cast validation #4176

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 12 commits into from
Mar 7, 2019
Merged

Cleanup expression/code cast validation #4176

Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
1de6c23
code_declt::check: for now accept more than one operand
tautschnig Feb 13, 2019
3c85341
code_deadt::check: to_symbol_expr requires a symbol_exprt
tautschnig Feb 13, 2019
92c140f
Replace misleading comments about validate_expr
tautschnig Feb 13, 2019
1d7789f
Re-use code_*t::check in validate_expr and to_code_*t
tautschnig Feb 13, 2019
8a21dea
Re-use validate_expr in to_code_*t
tautschnig Feb 13, 2019
10d61b2
mathematical_expr.h: move can_cast and validate_expr
tautschnig Feb 13, 2019
35262aa
Re-use validate_expr in mathematical_expr.h
tautschnig Feb 13, 2019
b61e3f1
std_expr.h: move can_cast and validate_expr
tautschnig Feb 13, 2019
0a73e03
std_expr.h: add/enable missing can_cast, validate_expr
tautschnig Feb 13, 2019
5e8af57
std_expr.h: remove commented-out validation steps
tautschnig Feb 13, 2019
4b5d356
Re-use validate_expr in to_*exprt
tautschnig Feb 13, 2019
d4dc77f
Re-use *_exprt::check in validate_expr and to_*exprt
tautschnig Feb 13, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Re-use code_*t::check in validate_expr and to_code_*t 
Prefer code re-use over duplicated (and possibly inconsistent)
implementations.
  • Loading branch information
@tautschnig
tautschnig committed Mar 6, 2019
commit 1d7789f0f23fc13136eb4b21a90e419550915905
39 changes: 13 additions & 26 deletions src/util/std_code.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -364,7 +364,7 @@ template<> inline bool can_cast_expr<code_assignt>(const exprt &base)

inline void validate_expr(const code_assignt & x)
{
validate_operands(x, 2, "assignment must have two operands");
code_assignt::check(x);
}

inline const code_assignt &to_code_assign(const codet &code)
Expand Down Expand Up @@ -432,29 +432,20 @@ template<> inline bool can_cast_expr<code_declt>(const exprt &base)

inline void validate_expr(const code_declt &x)
{
validate_operands(x, 1, "decls must have one or more operands", true);
code_declt::check(x);
}

inline const code_declt &to_code_decl(const codet &code)
{
PRECONDITION(code.get_statement() == ID_decl);

// will be size()==1 in the future
DATA_INVARIANT(
code.operands().size() >= 1, "decls must have one or more operands");
DATA_INVARIANT(
code.op0().id() == ID_symbol, "decls symbols must be a \"symbol\"");

code_declt::check(code);
return static_cast<const code_declt &>(code);
}

inline code_declt &to_code_decl(codet &code)
{
PRECONDITION(code.get_statement() == ID_decl);

// will be size()==1 in the future
DATA_INVARIANT(
code.operands().size() >= 1, "decls must have one or more operands");
code_declt::check(code);
return static_cast<code_declt &>(code);
}

Expand Down Expand Up @@ -510,28 +501,20 @@ template<> inline bool can_cast_expr<code_deadt>(const exprt &base)

inline void validate_expr(const code_deadt &x)
{
validate_operands(x, 1, "dead statement must have one operand");
code_deadt::check(x);
}

inline const code_deadt &to_code_dead(const codet &code)
{
PRECONDITION(code.get_statement() == ID_dead);
DATA_INVARIANT(
code.operands().size() == 1, "dead statement must have one operand");
DATA_INVARIANT(
to_unary_expr(code).op().id() == ID_symbol,
"dead statement must take symbol operand");
code_deadt::check(code);
return static_cast<const code_deadt &>(code);
}

inline code_deadt &to_code_dead(codet &code)
{
PRECONDITION(code.get_statement() == ID_dead);
DATA_INVARIANT(
code.operands().size() == 1, "dead statement must have one operand");
DATA_INVARIANT(
to_unary_expr(code).op().id() == ID_symbol,
"dead statement must take symbol operand");
code_deadt::check(code);
return static_cast<code_deadt &>(code);
}

Expand Down Expand Up @@ -1242,18 +1225,20 @@ template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)

inline void validate_expr(const code_function_callt &x)
{
validate_operands(x, 3, "function calls must have three operands");
code_function_callt::check(x);
}

inline const code_function_callt &to_code_function_call(const codet &code)
{
PRECONDITION(code.get_statement() == ID_function_call);
code_function_callt::check(code);
return static_cast<const code_function_callt &>(code);
}

inline code_function_callt &to_code_function_call(codet &code)
{
PRECONDITION(code.get_statement() == ID_function_call);
code_function_callt::check(code);
return static_cast<code_function_callt &>(code);
}

Expand Down Expand Up @@ -1305,18 +1290,20 @@ template<> inline bool can_cast_expr<code_returnt>(const exprt &base)

inline void validate_expr(const code_returnt &x)
{
validate_operands(x, 1, "return must have one operand");
code_returnt::check(x);
}

inline const code_returnt &to_code_return(const codet &code)
{
PRECONDITION(code.get_statement() == ID_return);
code_returnt::check(code);
return static_cast<const code_returnt &>(code);
}

inline code_returnt &to_code_return(codet &code)
{
PRECONDITION(code.get_statement() == ID_return);
code_returnt::check(code);
return static_cast<code_returnt &>(code);
}

Expand Down