Skip to content

Conversation

danpoe
Copy link
Contributor

@danpoe danpoe commented Aug 20, 2018

No description provided.

@kroening
Copy link
Collaborator

A key problem of throwing exceptions is that they can't be used for warnings.

Thus, I'd recommend retaining the message handlers in places where warnings might be needed.

@danpoe danpoe force-pushed the refactor/error-handling-util branch 2 times, most recently from e69d31c to 700b28e Compare September 5, 2018 14:07
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR failed Diffblue compatibility checks (cbmc commit: 700b28e).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

if(expr.operands().size()!=2)
throw "index takes two operands";
DATA_INVARIANT(
expr.operands().size() == 2, "index expression has two operands");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use to_index_expr and let it do all the error checking and reporting.

{
assert(expr.operands().size()==1);
DATA_INVARIANT(
expr.operands().size() == 1, "member expression has one operand");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

to_member_expr

@danpoe danpoe force-pushed the refactor/error-handling-util branch from 700b28e to 23e9de7 Compare September 6, 2018 13:06
@danpoe danpoe force-pushed the refactor/error-handling-util branch from 23e9de7 to b0bab14 Compare September 6, 2018 13:08
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR failed Diffblue compatibility checks (cbmc commit: 23e9de7).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR failed Diffblue compatibility checks (cbmc commit: b0bab14).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84005870
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: b0bab14).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84005870

std::string reason;

public:
system_exceptiont(const std::string &reason) : reason(reason)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be marked as explicit, should take reason as plain string rather than reference and should move reason.

public:
system_exceptiont(const std::string &reason) : reason(reason)
{
}

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should go into exception_utils.cpp

res += "System Exception\n";
res += "Reason: " + reason + "\n";
return res;
}

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should go into exception_utils.cpp

std::cerr << e.what() << "\n";
return CPROVER_EXIT_USAGE_ERROR;
}
catch(system_exceptiont &e)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should probably add a base class like cprover_exceptiont so we don't have to do this for every single kind of exception we introduce.

@danpoe danpoe force-pushed the refactor/error-handling-util branch from b0bab14 to e0715f3 Compare September 20, 2018 16:44
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR failed Diffblue compatibility checks (cbmc commit: e0715f3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85464121
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

src/util/graph.h Outdated
while(true)
{
assert(!t.scc_stack.empty());
INVARIANT(!t.scc_stack.empty(), "");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing error message

src/util/graph.h Outdated
for(std::size_t i = 0; i < nodes.size(); i++)
{
INVARIANT(
reachable_idx >= reachable.size() || i <= reachable[reachable_idx], "");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing message

@danpoe danpoe force-pushed the refactor/error-handling-util branch from e0715f3 to ffc52fb Compare September 21, 2018 16:50
@danpoe danpoe force-pushed the refactor/error-handling-util branch from ffc52fb to 73a215c Compare September 24, 2018 12:35
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 73a215c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85731119

rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
assert(rhs.is_not_nil());
}
catch(...)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Needs another rebase and several nit-picks, plus an actual concern about static_lifetime_init.


if(ns.lookup(id, symbol))
throw "failed to find "+id2string(id);
bool not_found = ns.lookup(id, symbol);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit pick: const


if(ns.lookup(id, symbol))
throw "failed to find "+id2string(id);
bool not_found = ns.lookup(id, symbol);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit pick: const

if(to_integer(to_constant_expr(tmp), int_value))
throw
"failed to convert symbol table configuration entry `"+id2string(id)+"'";
bool error = to_integer(to_constant_expr(tmp), int_value);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit pick: const

{
return true;
}
namespacet ns(symbol_table);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

const


if(static_lifetime_init(symbol_table, symbol.location, message_handler))
return true;
static_lifetime_init(symbol_table, symbol.location, message_handler);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This procedure still has a non-void return type, should that change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, changed it to void. The remaining check in static_lifetime_init is a precondition now.

@danpoe danpoe force-pushed the refactor/error-handling-util branch from 73a215c to 756c0b9 Compare September 25, 2018 10:58
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 756c0b9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85854252

@tautschnig tautschnig merged commit 5b5ba13 into diffblue:develop Sep 25, 2018
@danpoe danpoe deleted the refactor/error-handling-util branch June 2, 2020 17:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants