Invariant cleanup, util directory, files j-r #2892

sonodtt · 2018-09-04T12:50:36Z

Cleanup of util directory, files j-r (json_irep.cpp withheld awaiting a review of cbmc exceptions)

Cleanup of asserts - replaced with invariants.
Removed all unstructured throw(...) statements, replacing with INVARIANT, PRECONDITION, where appropriate.

hannes-steffenhagen-diffblue

One invariant I'd change, also please run git-clang-format

hannes-steffenhagen-diffblue · 2018-09-04T12:56:32Z

src/util/mp_arith.cpp

  ullong_t shift=b.to_ulong();
-  if(shift>true_size)
-    throw "shift value out of range";
+  DATA_INVARIANT(shift<=true_size, "shift value must be in range");


PRECONDITION

sonodtt · 2018-09-04T13:16:12Z

@hannes-steffenhagen-diffblue (throws ashes on head ) - I did not push local changes. :(
Done.

hannes-steffenhagen-diffblue

OK, minor ⛏️ aside

hannes-steffenhagen-diffblue · 2018-09-04T13:29:05Z

src/util/mp_arith.cpp

  ullong_t shift=b.to_ulong();
-  if(shift>true_size)
-    throw "shift value out of range";
+  DATA_INVARIANT(shift <= true_size, "shift value must be in range");


This should still be a PRECONDITION

Yep. It is now that I pushed the local changes. (Doh!)

hannes-steffenhagen-diffblue · 2018-09-04T13:40:10Z

src/util/reference_counting.h

-  assert(old_d->ref_count!=0);
+  PRECONDITION(old_d->ref_count != 0);

-  #ifdef REFERENCE_COUNTING_DEBUG


This seems like an odd change, was this done by clang-format?

I have undone those indentations and it did not happen again upon a clang-format. (!?!)

tautschnig

Mostly looks good except as noted below.

tautschnig · 2018-09-04T14:10:21Z

src/util/namespace.h

+    INVARIANT(
+      !not_found,
+      "we are assuming that a name exists in the namespace "
+      "when this function is called");


Please include/keep id2string(name) in the error message.

tautschnig · 2018-09-04T14:10:49Z

src/util/rational.cpp

 /// Rational Numbers

 #include "rational.h"
+#include "invariant.h"


Maintain lexicographic ordering of includes: move one line up.

The first was the source file's own header. My lack of a spacing line did not make this clear.
Amended to:

#include "rational.h" #include <algorithm> #include <ostream> #include "invariant.h"

tautschnig · 2018-09-04T14:11:10Z

src/util/reference_counting.h

 #ifndef CPROVER_UTIL_REFERENCE_COUNTING_H
 #define CPROVER_UTIL_REFERENCE_COUNTING_H

 #include <cassert>


Should now be removed.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 3a915bf).
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).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 341f993).
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).

allredj

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

sonodtt requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 4, 2018 12:50

hannes-steffenhagen-diffblue suggested changes Sep 4, 2018

View reviewed changes

hannes-steffenhagen-diffblue self-assigned this Sep 4, 2018

sonodtt force-pushed the invariant-cleanup-util_dir-files_j-to-r branch from ebc8391 to 460ff53 Compare September 4, 2018 13:13

hannes-steffenhagen-diffblue approved these changes Sep 4, 2018

View reviewed changes

sonodtt force-pushed the invariant-cleanup-util_dir-files_j-to-r branch from 460ff53 to 3a915bf Compare September 4, 2018 14:00

tautschnig approved these changes Sep 4, 2018

View reviewed changes

sonodtt force-pushed the invariant-cleanup-util_dir-files_j-to-r branch from 3a915bf to 8f28c2f Compare September 4, 2018 15:14

allredj reviewed Sep 4, 2018

View reviewed changes

Invariant cleanup

341f993

sonodtt force-pushed the invariant-cleanup-util_dir-files_j-to-r branch from 8f28c2f to 341f993 Compare September 5, 2018 07:46

allredj reviewed Sep 5, 2018

View reviewed changes

allredj reviewed Sep 6, 2018

View reviewed changes

hannes-steffenhagen-diffblue merged commit 55a52a2 into diffblue:develop Sep 6, 2018

Invariant cleanup, util directory, files j-r #2892

Invariant cleanup, util directory, files j-r #2892

Uh oh!

Conversation

sonodtt commented Sep 4, 2018

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sonodtt commented Sep 4, 2018

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sonodtt Sep 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sonodtt Sep 5, 2018 •

edited

Loading