Replace asserts and throws under goto-symex #6

NlightNFotis · 2018-07-19T09:29:25Z

No description provided.

NlightNFotis

Just left some comments about the rationale regarding some of the changes to make it easier for other people to review.

NlightNFotis · 2018-07-19T13:59:02Z

src/goto-symex/slice_by_trace.cpp

@@ -94,7 +101,7 @@ void symex_slice_by_tracet::slice_by_trace(
    }
    else if(!(g_copy.id()==ID_constant))
    {
-      throw "guards should only be and, symbol, constant, or `not'";
+      UNHANDLED_CASE;


Some rationale for the changes: This is just for documentation purposes, the INVARIANT above should have crashed it anyway if it's something different.

NlightNFotis · 2018-07-19T14:04:08Z

src/goto-symex/symex_builtin_functions.cpp

@@ -313,8 +307,7 @@ void goto_symext::symex_printf(
  statet &state,
  const exprt &rhs)
 {
-  if(rhs.operands().empty())
-    throw "printf expected to have at least one operand";


I have made the judgement call to drop what I consider to be redundant error messages, in the cases where the PRECONDITION assertion itself (within the context) seems self evident.

NlightNFotis · 2018-07-19T14:05:24Z

src/goto-symex/symex_builtin_functions.cpp

-    #endif
-  }
-  else
-    throw "unknown macro: "+id2string(identifier);


Here, I consider the whole

if (something) { ...some computation... } else { throw exception }

to just have the general form:

assert (something) ... do the useful computation ...

so I have rearranged it appropriately.

That's assuming that (something) is error checked elsewhere, and that its not being provided from user code....

NlightNFotis · 2018-07-19T14:07:23Z

src/goto-symex/symex_dead.cpp

-    throw "dead expects symbol as first operand";
-
+  PRECONDITION(code.operands().size()!=1);
+	PRECONDITION(code.op0().id()!=ID_symbol);


I don't know why there's this preceding space, and also the preconditions are wrong.

Something that is of the form

if (not something) throw exception

should have the form

assert (something);

NlightNFotis · 2018-07-19T14:08:54Z

src/goto-symex/symex_function_call.cpp

-                       assignment.rhs().type(), ns))
-        throw
-          "goto_symext::return_assignment type mismatch at "+
-          instruction.source_location.as_string()+":\n"+


Here I made the judgement call that the error message, especially within the context, was too chatty. I replaced it with an INVARIANT which keeps part of the message, but drops the extraneous information (at least for the usual case)

or to put in in another way, I have a severe dislike for an error message in an invariant that prints two expressions.pretty()

a) - Are we sure this is not a user level error?
b) Imagine you made a modification to CBMC and hit this new INVARIANT - how would you go about debugging it? What types mismatch?

NlightNFotis · 2018-07-19T14:10:27Z

src/goto-symex/symex_function_call.cpp

  }
+
+  POSTCONDITION(!frame.return_value.is_not_nil());


Replaced the throw "return with unexpected value" with just a POSTCONDITION. I think it's cleaner this way, and more self evident what it does, while not altering the semantics of the code.

NlightNFotis · 2018-07-19T14:11:01Z

src/goto-symex/symex_goto.cpp

-  if(instruction.targets.size()!=1)
-    throw "no support for non-deterministic gotos";
+  DATA_INVARIANT(
+  	instruction.targets.size()!=1, "no support for non-deterministic gotos");


Again, this hasn't been inverted properly, should be instruction.targets.size() == 1

hannes-steffenhagen-diffblue

There are quite a few things in here that need additional discussion, and a couple things that definitely need to be changed.

hannes-steffenhagen-diffblue · 2018-07-19T13:07:59Z

src/goto-symex/build_goto_trace.cpp

@@ -222,7 +222,7 @@ void build_goto_trace(
      else if(it->is_atomic_end() && current_time<0)
        current_time*=-1;

-      assert(current_time>=0);
+      PRECONDITION(current_time>=0);


This isn't a precondition, this is an invariant that's supposed to be maintained by the current code block.

(Again, difference - Precondition failure is meant to indicate that the function was used incorrectly, whereas most other invariant failures are meant to indicate that the function itself is broken).

hannes-steffenhagen-diffblue · 2018-07-19T13:10:32Z

src/goto-symex/goto_symex_state.cpp

@@ -51,8 +51,7 @@ void goto_symex_statet::level0t::operator()(

  const symbolt *s;
  const bool found_l0 = !ns.lookup(obj_identifier, s);
-  DATA_INVARIANT(
-    found_l0, "level0: failed to find " + id2string(obj_identifier));
+  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));


Nice catch, this indeed doesn't seem to meet the definition of DATA_INVARIANT

hannes-steffenhagen-diffblue · 2018-07-19T14:37:36Z

src/goto-symex/goto_symex_state.cpp

-    DATA_INVARIANT(
-      expr.type().id() == ID_pointer,
-      "type of address_of should be ID_pointer");
+    PRECONDITION(expr.type().id() == ID_pointer);


This should probably be the first thing that's being checked in this block?

hannes-steffenhagen-diffblue · 2018-07-19T14:37:54Z

src/goto-symex/goto_symex_state.cpp

@@ -495,12 +493,9 @@ void goto_symex_statet::rename(
  }
  else if(expr.id()==ID_address_of)
  {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "address_of should have a single operand");
+    PRECONDITION(expr.operands().size() == 1);


No, this should be a DATA_INVARIANT.

hannes-steffenhagen-diffblue · 2018-07-19T14:40:34Z

src/goto-symex/postcondition.cpp

@@ -76,20 +76,19 @@ bool postconditiont::is_used_address_of(
  }
  else if(expr.id()==ID_index)
  {
-    assert(expr.operands().size()==2);
-
+    PRECONDITION(expr.operands().size() == 2);


DATA_INVARIANT

hannes-steffenhagen-diffblue · 2018-07-19T16:45:14Z

src/goto-symex/symex_main.cpp

-    PRECONDITION(expr.operands().size()==2);
-    PRECONDITION(expr.op0().id()==ID_symbol);
+    PRECONDITION(expr.operands().size() == 2);
+    PRECONDITION(expr.op0().id() == ID_symbol);


Also DATA_INVARIANT

hannes-steffenhagen-diffblue · 2018-07-19T16:45:44Z

src/goto-symex/symex_other.cpp

-    DATA_INVARIANT(
-      code.operands().size() == 2,
-      "array_copy/array_replace takes two operands");
+  	PRECONDITION(code.operands().size() == 2);


DATA_INVARIANT

hannes-steffenhagen-diffblue · 2018-07-19T16:45:57Z

src/goto-symex/symex_other.cpp

@@ -187,7 +185,7 @@ void goto_symext::symex_other(
    // process_array_expr)
    // 3. use the type of the resulting array to construct an array_of
    // expression
-    DATA_INVARIANT(code.operands().size() == 2, "array_set takes two operands");
+    PRECONDITION(code.operands().size() == 2);


DATA_INVARIANT

hannes-steffenhagen-diffblue · 2018-07-19T16:46:08Z

src/goto-symex/symex_other.cpp

-    DATA_INVARIANT(
-      code.operands().size() == 3,
-      "array_equal expected to take three arguments");
+    PRECONDITION(code.operands().size() == 3);


DATA_INVARIANT (probably)

hannes-steffenhagen-diffblue · 2018-07-19T16:46:56Z

src/goto-symex/symex_other.cpp

@@ -266,8 +262,7 @@ void goto_symext::symex_other(
  }
  else if(statement==ID_havoc_object)
  {
-    DATA_INVARIANT(code.operands().size()==1,
-                   "havoc_object must have one operand");
+    PRECONDITION(code.operands().size()==1);


DATA_INVARIANT

johnnonweiler · 2018-07-24T10:08:12Z

src/goto-symex/symex_builtin_functions.cpp

@@ -234,8 +229,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
  const exprt &lhs,
  const side_effect_exprt &code)
 {
-  if(code.operands().size()!=1)
-    throw "va_arg_next expected to have one operand";
+  PRECONDITION(code.operands().size() != 1);


Should this be "=="?

Yes, you are right, I don't know why this wasn't changed.

johnnonweiler

Two questions:

The whitespace doesn't appear to match the coding standards in some places. Have you run clang format?
What tests do we have to check that there aren't any "!=" where there should be "=="?

johnnonweiler · 2018-07-24T10:13:34Z

src/goto-symex/symex_decl.cpp

+  // two-operand decl not supported here
+  // we handle the decl with only one operand
+  PRECONDITION(code.operands().size()==1);
+  PRECONDITION(code.op0().id()!=ID_symbol);


code.op0().id == ID_symbol ?

Yeah, as John says - formatting for both PRECONDITIONS. Could consider these as DATA_INVARIANTS instead too?

I wasn't actually commenting on the formatting (although I do agree with Chris).
I was suggesting that I think it should be '==' instead of '!='.

Argh - yes, good catch John.

Yes, these were left in by mistake. This was part of a change I had done while I was quickly prototyping some changes during a discussion with Hannes, and forgot to properly go back and re-edit them.

It's the same thing as with the commented out code below.

johnnonweiler · 2018-07-24T10:24:05Z

src/goto-symex/slice_by_trace.cpp

+    	g_copy.id() == ID_not ||
+    	g_copy.id() == ID_and ||
+    	g_copy.id() == ID_constant,
+    	"guards should only be and, symbol, constant, or `not'");


Previously, this was throwing an exception for ID_and (but the comment suggested that guards can be and). Is this a deliberate change?

@johnnonweiler No it wasn't (https://github.com/diffblue/cbmc/blob/develop/src/goto-symex/slice_by_trace.cpp#L95). What that did is that it checked if the expression's type is ID_symbol or ID_not which was handled in the first if consequent statement, then it checked if the expression's type is ID_and, which was handled in the second consequent statement (else if (g_copy.id()==ID_and)...) and last it was throwing an exception if the expression's type was anything but a constant (else if (!(g_copy.id()==ID_constant)) - based on the idea that it had checked for the other meaningful types and handled them, and left the constant case unhandled but crashed on anything else).

This INVARIANT does the same thing, just earlier, while it also drops the unneeded exception now.

Sorry @NlightNFotis - I got confused by GitHub hiding a couple of lines in the diff!

johnnonweiler · 2018-07-24T10:24:57Z

src/goto-symex/symex_assign.cpp

@@ -55,8 +55,9 @@ void goto_symext::symex_assign(
      symex_allocate(state, lhs, side_effect_expr);
    else if(statement==ID_printf)
    {
-      if(lhs.is_not_nil())
-        throw "printf: unexpected assignment";
+    	PRECONDITION(!lhs.is_not_nil());


Could this be lhs.is_nil() (instead of the double negative)?

Agree with John here - don't like the double negative.

johnnonweiler · 2018-07-24T10:25:13Z

src/goto-symex/symex_assign.cpp

-        throw "printf: unexpected assignment";
+    	PRECONDITION(!lhs.is_not_nil());
+      // if(lhs.is_not_nil())
+        // throw "printf: unexpected assignment";


Why include this commented out code?

Yep, this code should be removed, not commented.

Yes, again, as stated before, this was part of some quick prototyping during a discussion with Hannes, that somehow manged to creep in.

chrisr-diffblue

There's a lot of work in here, and most of it is very good - but there's a few changes which I don't agree with, and a lot of white space indentation that needs cleaning up.

chrisr-diffblue · 2018-07-24T10:34:12Z

src/goto-symex/build_goto_trace.cpp

@@ -92,7 +92,7 @@ exprt build_full_lhs_rec(
          id==ID_byte_extract_big_endian)
  {
    exprt tmp=src_original;
-    assert(tmp.operands().size()==2);
+    PRECONDITION(tmp.operands().size() == 2);


Minor nit: Why not move the PRECONDITION to be the first line in the block?

Should this be a DATA_INVARIANT ?

chrisr-diffblue · 2018-07-24T10:41:56Z

src/goto-symex/build_goto_trace.cpp

@@ -222,7 +222,7 @@ void build_goto_trace(
      else if(it->is_atomic_end() && current_time<0)
        current_time*=-1;

-      assert(current_time>=0);
+      INVARIANT(current_time>=0, "time keeping inconsistency");


Again, isn't this a DATA_INVARIANT?

No. This is what the DATA_INVARIANT's documentation says:

// This condition should be used to document that assumptions that are
// made on goto_functions, goto_programs, exprts, etc. being well formed.
// "The data structure is corrupt or malformed"

To my understanding this is to assert properties of fundamental data structures representing the program under analysis. In this case current_time is a local variable that is only required to be consistent during the execution of the function.

Seems reasonable, thanks.

chrisr-diffblue · 2018-07-24T10:44:29Z

src/goto-symex/goto_symex_state.cpp

@@ -187,8 +186,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
  }
  else if(expr.id()==ID_member)
  {
-    if(expr.operands().size()!=1)
-      throw "member expects one operand";
+    PRECONDITION(expr.operands().size() == 1);


Surely DATA_INVARIANT?

By definition this falls between multiple categories of the invariant checks (it falls both under DATA_INVARIANT because it checks fundamental data structures like an exprt in this case, but it also falls under the PRECONDITION case, in that it's asserting whether an argument of the function is correct and the rest of the computation can be sound based on that assertion.

But I can certainly change it to the DATA_INVARIANT in case it makes things a little bit cleaner.

chrisr-diffblue · 2018-07-24T10:45:10Z

src/goto-symex/goto_symex_state.cpp

@@ -495,12 +493,10 @@ void goto_symex_statet::rename(
  }
  else if(expr.id()==ID_address_of)
  {
+    PRECONDITION(expr.type().id() == ID_pointer);


Isn't this DATA_INVARIANT?

Same thing as above really, but I can change it to make it clearer.

chrisr-diffblue · 2018-07-24T10:45:45Z

src/goto-symex/goto_symex_state.cpp

    DATA_INVARIANT(
-      expr.operands().size() == 1, "address_of should have a single operand");
+    	expr.operands().size() == 1, "address_of should have a single operand");


Unnecessary (and incorrect) indentation change.

chrisr-diffblue · 2018-07-24T14:36:36Z

src/goto-symex/symex_other.cpp

-    DATA_INVARIANT(code.operands().size()==1,
-                   "havoc_object must have one operand");
+    DATA_INVARIANT(
+  		code.operands().size() == 1,


Again, original message was better...

chrisr-diffblue · 2018-07-24T14:38:13Z

src/goto-symex/symex_start_thread.cpp

-  if(state.atomic_section_id!=0)
-    throw "start_thread in atomic section detected";
+  INVARIANT(state.atomic_section_id==0,
+    "start_thread in atomic section detected");


This could be a PRE_CONDITION, maybe?

The message might be better phrased as something like "start_thread not supported in atomic section" ?

While I agree with you, I find the message to be useful (in that it contains information that can't be transmitted through the condition checked easily), and making this a PRECONDITION would require the message to be killed. I don't believe this to be a good idea, this is why I kept it as an INVARIANT.

However, I can change this if there are strong feelings about it.

INVARIANT descriptions should describe what condition we expect to be holding, not what error condition they are detecting - I think the description should be updated.

chrisr-diffblue · 2018-07-24T14:43:53Z

src/util/exception_utils.h

@@ -10,6 +10,11 @@ Author: Fotis Koutoulakis, [email protected]
 #define CPROVER_UTIL_EXCEPTION_UTILS_H

 #include <string>
+#include <sstream>
+
+#include <goto-symex/symex_target_equation.h>


I think this is wrong. This means that 'src/util' now has a dependency on 'goto-symex' which I think is wrong. I also don't see why equation_conversion_exceptiont has been moved into this file, since it's so specific to symex....

chrisr-diffblue · 2018-07-24T14:44:42Z

src/goto-symex/equation_conversion_exceptions.h

@@ -1,47 +0,0 @@
-/*******************************************************************\


I don't see why this was removed! (see also my comments where this exception class was moved to....)

chrisr-diffblue · 2018-07-24T14:46:39Z

src/util/exception_utils.h

@@ -38,4 +43,31 @@ class invalid_user_input_exceptiont
  }
 };

+
+class equation_conversion_exceptiont : public std::runtime_error


If the intent of moving this exception class into this file was to make it part of the new exception class hierachy, then this class should be inheriting from something other than std::runtime_error...... I whole heartedly agree that this class should move into the new hierachy, but it shouldn't be in this util directory. It should stay in it's original file but just inherit from a suitable class in the new hierachy.

There's no hierarchy yet, and thinking about how to model one I think it's trickier than it looks to just design one on the spot. I will just revert this commit and note it down as one of the improvements I want to take a look at further down the line.

chrisr-diffblue · 2018-07-30T16:24:53Z

src/goto-symex/symex_decl.cpp

-  PRECONDITION(code.operands().size()==1);
-  PRECONDITION(code.op0().id()!=ID_symbol);
+  PRECONDITION(code.operands().size() == 1);
+  PRECONDITION(code.op0().id() == ID_symbol);


Why has this PRECONDITION changed from != to == ? I don't see why this patch hunk is here as apart from that operator changing, it's just whitespace formatting changing, which is not related to this pr.

The original code for this was:

if(code.op0().id()!=ID_symbol) throw "decl expects symbol as first operand";

When we turn these if conditions into PRECONDITIONs, we are changing from checking if something shouldn't happen, to checking that the opposite should always happen. I hadn't made the reversal of the condition properly in one of the previous commits, and this compensates for that.

chrisr-diffblue · 2018-07-30T16:33:34Z

src/goto-symex/symex_goto.cpp

-  PRECONDITION(state.atomic_section_id == goto_state.atomic_section_id);
+  INVARIANT(
+  	state.atomic_section_id == goto_state.atomic_section_id,
+  	"atomic sections differ across branches");


The description here is not quite right - the invariant is more a statement that "atomic section should be the same across branches". The description is a description of what invariant we are expecting to hold, not a description of what has gone wrong.

chrisr-diffblue · 2018-07-30T16:36:48Z

src/goto-symex/build_goto_trace.cpp

@@ -222,7 +222,7 @@ void build_goto_trace(
      else if(it->is_atomic_end() && current_time<0)
        current_time*=-1;

-      assert(current_time>=0);
+      INVARIANT(current_time>=0, "time keeping inconsistency");


Seems reasonable, thanks.

chrisr-diffblue · 2018-07-30T16:42:48Z

src/goto-symex/precondition.cpp

-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+    	dest.operands().size() == 1,
+    	"address_of expression expected to have one operand at this point");


"at this point" isn't needed - keep them tight.

chrisr-diffblue · 2018-07-30T16:43:01Z

src/goto-symex/precondition.cpp

-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+    	dest.operands().size() == 1,
+    	"dereference expression expected to have one operand at this point");



"at this point" isn't needed

chrisr-diffblue · 2018-07-30T16:44:25Z

src/goto-symex/slice_by_trace.cpp

+    DATA_INVARIANT(
+      g_copy.id() == ID_symbol || g_copy.id() == ID_not ||
+        g_copy.id() == ID_and || g_copy.id() == ID_constant,
+      "guards should only be and, symbol, constant, or `not'");


Either put quote marks around all the items, or none - at the moment you only put quote marks around 'not'

Ahh, I don't. It was like this, and because I've seen this pattern* in a couple of places around cbmc, I'm assuming it is by design. I can change it if you want though.

*: The pattern being something like this always:

``something'`

chrisr-diffblue · 2018-07-30T16:46:54Z

src/goto-symex/slice_by_trace.cpp

-      throw "trace uses symbol not in alphabet: "+event;
+    PRECONDITION(!alphabet.empty());
+    INVARIANT((alphabet.count(event) != 0) == alphabet_parity, 
+    	"trace uses symbol not in alphabet: " + event);


Description should describe what is being asserted.... "trace symbol must be in alphabet"

chrisr-diffblue · 2018-07-30T16:53:14Z

src/goto-symex/symex_dereference.cpp

@@ -155,6 +155,9 @@ exprt goto_symext::address_arithmetic(
  }
  else if(expr.id()==ID_dereference)
  {
+  	DATA_INVARIANT(
+  		expr.operands().size() == 1,
+  		"dereference expression expected to have one operand");


Indentation still...

chrisr-diffblue · 2018-07-30T16:54:09Z

src/goto-symex/symex_function_call.cpp

-    exprt value=code.op0();
+  PRECONDITION(
+  	code.operands().size() == 1 ||
+  	frame.return_value.is_nil());


Indentation still

NlightNFotis

@chrisr-diffblue The indentation errors were very weird this time around, because the last commit was explicitly passing git-clang-format on HEAD. It appeared that what you saw was new lines that had been indented with TAB rather than spaces, and git-clang-format was (and still is) okay with it. I have changed it manually to spaces to see if it makes it better.

NlightNFotis · 2018-07-31T08:59:49Z

src/goto-symex/slice_by_trace.cpp

+    DATA_INVARIANT(
+      g_copy.id() == ID_symbol || g_copy.id() == ID_not ||
+        g_copy.id() == ID_and || g_copy.id() == ID_constant,
+      "guards should only be and, symbol, constant, or `not'");


Ahh, I don't. It was like this, and because I've seen this pattern* in a couple of places around cbmc, I'm assuming it is by design. I can change it if you want though.

*: The pattern being something like this always:

``something'`

NlightNFotis · 2018-07-31T09:04:43Z

src/goto-symex/symex_decl.cpp

-  PRECONDITION(code.operands().size()==1);
-  PRECONDITION(code.op0().id()!=ID_symbol);
+  PRECONDITION(code.operands().size() == 1);
+  PRECONDITION(code.op0().id() == ID_symbol);


The original code for this was:

if(code.op0().id()!=ID_symbol) throw "decl expects symbol as first operand";

When we turn these if conditions into PRECONDITIONs, we are changing from checking if something shouldn't happen, to checking that the opposite should always happen. I hadn't made the reversal of the condition properly in one of the previous commits, and this compensates for that.

src/goto-symex/symex_dereference.cpp

src/goto-symex/symex_other.cpp

chrisr-diffblue · 2018-08-10T14:21:32Z

src/goto-symex/symex_start_thread.cpp

-  if(state.atomic_section_id!=0)
-    throw "start_thread in atomic section detected";
+  INVARIANT(state.atomic_section_id==0,
+    "start_thread in atomic section detected");


INVARIANT descriptions should describe what condition we expect to be holding, not what error condition they are detecting - I think the description should be updated.

John Nonweiler and others added 2 commits July 13, 2018 10:42

Replace asserts and throws with INVARIANT etc.

16d03d7

Translate asserts and throws to PRECONDITIONS and INVARIANTS

526945e

NlightNFotis commented Jul 19, 2018

View reviewed changes

hannes-steffenhagen-diffblue suggested changes Jul 19, 2018

View reviewed changes

johnnonweiler reviewed Jul 24, 2018

View reviewed changes

NlightNFotis added 2 commits July 24, 2018 11:11

Add changes suggested during code review.

112bd5b

Move equation conversion exception to exception utils

c7fb551

NlightNFotis force-pushed the custom_exception branch from a6bce43 to c7fb551 Compare July 24, 2018 10:11

johnnonweiler reviewed Jul 24, 2018

View reviewed changes

chrisr-diffblue requested changes Jul 24, 2018

View reviewed changes

Address the latest review comments.

b43902e

NlightNFotis force-pushed the custom_exception branch from c7fb551 to 09c7495 Compare July 27, 2018 09:21

chrisr-diffblue reviewed Jul 30, 2018

View reviewed changes

NlightNFotis commented Jul 31, 2018

View reviewed changes

chrisr-diffblue reviewed Aug 10, 2018

View reviewed changes

NlightNFotis added 4 commits August 30, 2018 11:52

Fixup into second

2d913c4

Add into the third one.

77b43ea

Some minor fixes

46aeea4

Some more changes.

f2a7a37

NlightNFotis force-pushed the custom_exception branch from aba3fe5 to f2a7a37 Compare September 5, 2018 14:13

NlightNFotis closed this Sep 5, 2018

NlightNFotis deleted the custom_exception branch September 5, 2018 14:14

		@@ -1,47 +0,0 @@
		/*******************************************************************\

Replace asserts and throws under goto-symex #6

Replace asserts and throws under goto-symex #6

Conversation

NlightNFotis commented Jul 19, 2018

NlightNFotis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johnnonweiler left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis Jul 24, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis left a comment

johnnonweiler left a comment •

edited

Loading

NlightNFotis Jul 24, 2018 •

edited

Loading