Fixes and improvements to dynamic memory handling #982

tautschnig · 2017-06-01T12:40:09Z

This is a collection of patches prepared for SV-COMP, originally in #363. These improve soundness (avoiding allocation of too large objects, invalid_object reports), precision (offset computation), and efficiency (calloc and other forms of zero initialisation become constant-time, which could be leveraged in the Java front-end).

peterschrammel · 2017-06-25T20:09:28Z

src/goto-symex/symex_builtin_functions.cpp

+  state.rename(zero_init, ns); // to allow constant propagation
+  simplify(zero_init, ns);
+
+  if(zero_init.is_constant() && !zero_init.is_zero())


Shouldn't we throw an exception if zero_init.is_constant() does not hold instead of silently ignoring the violated precondition?

peterschrammel · 2017-06-25T20:11:34Z

src/solvers/flattening/bv_pointers.cpp

+    // compare object part to non-allocated dynamic objects
+    std::size_t number=0;
+
+    for(pointer_logict::objectst::const_iterator


Could use ranged for

tautschnig · 2017-06-28T16:48:46Z

@peterschrammel Comments addressed.

tautschnig · 2017-08-14T13:19:18Z

@smowton Maybe you could provide input on zero-initialisation of Java objects, where I've inserted a few TODOs in this PR.

smowton

A few style comments and some possible mistakes. Re: Java yes using calloc seems sensible. I won't give an approval since I don't understand the intent well enough, mostly due to unfamiliarity with the code being changed.

smowton · 2017-08-15T10:15:48Z

src/ansi-c/library/new.c

+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(malloc_size<(1ULL<<((sizeof(char*)-1)*8-1)));


What about @peterschrammel's recent change to parameterise the object-bits value?

Yes, that should be considered here (even though I'd prefer #1086 to eventually fix this properly), but needs some extra work to expose the configuration option to the C preprocessor. I should likely move this to a different PR.

Yeah I wouldn't want to commit a change that was actively false, and this will complain even if the user has set object-bits 16 or similar.

smowton · 2017-08-15T10:20:42Z

src/ansi-c/library/stdlib.c

+
+  // detect memory leaks
+  __CPROVER_bool record_may_leak;
+  __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak;


Using uninitialised?

Intentionally so, yes, to use non-determinism.

Do we have an explicit get-nondet-bool so this looks less like a mistake to the casual reader? Otherwise suggest commenting to this effect.

We could use __VERIFIER_nondet_bool(), which should work.

The fix is in #1243, for the entire C library.

smowton · 2017-08-15T10:22:16Z

src/ansi-c/library/stdlib.c

+  // flattening/pointer_logic.h; also avoid sign-extension issues
+  // for 32-bit systems that yields a maximum allocation of 2^23-1,
+  // i.e., just under 8MB
+  __CPROVER_assume(alloca_size<(1ULL<<((sizeof(char*)-1)*8-1)));


Worth macro-izing this repeated and somewhat tangly check?

Also true. Should be considered when in a new PR.

smowton · 2017-08-15T10:27:12Z

src/goto-symex/symex_builtin_functions.cpp

  address_of_exprt rhs;

+  symbol_exprt v=value_symbol.symbol_expr();
+  v.add("#dynamic_guard", state.guard);


-> irep_ids.def

smowton · 2017-08-15T10:27:40Z

src/goto-symex/symex_builtin_functions.cpp

  address_of_exprt rhs;

+  symbol_exprt v=value_symbol.symbol_expr();


Rename single-char variable

smowton · 2017-08-15T10:28:09Z

src/goto-symex/symex_builtin_functions.cpp

@@ -374,6 +408,9 @@ void goto_symext::symex_cpp_new(
  do_array=(code.get(ID_statement)==ID_cpp_new_array);

  dynamic_counter++;
+  // we can only encode 254 fresh objects + invalid + null in 8 bits
+  if(dynamic_counter>254)


Similar to above this is no longer true, this is now variable

Will drop as the check in flattening works these days.

smowton · 2017-08-15T10:50:47Z

src/solvers/flattening/bv_pointers.cpp

@@ -28,31 +30,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
    if(operands.size()==1 &&
       is_ptr(operands[0].type()))
    {
-      const bvt &bv=convert_bv(operands[0]);
+      // we postpone


Maybe comment a little more on why?

smowton · 2017-08-15T10:56:54Z

src/solvers/flattening/bv_pointers.cpp

+    // compare object part to non-allocated dynamic objects
+    std::size_t number=0;
+
+    for(const exprt &expr : objects)


How about an old-school for-loop--
for(auto iter=objects.begin(); iter!=objects.end(); iter++, number++)
instead of bumping number in three different places?

smowton · 2017-08-15T10:59:25Z

src/solvers/flattening/bv_pointers.cpp

+    disj.push_back(bv_utils.equal(saved_bv, invalid_bv));
+    disj.push_back(bv_utils.equal(saved_bv, null_bv));
+
+    // compare object part to non-allocated dynamic objects


Compare for equality, or...? Is the goal here to check that postponed.expr doesn't match any dynamic object id? I think you should document the intent of #dynamic_guard somewhere.

tautschnig · 2017-11-02T17:34:00Z

@marek-trtik Given all your work on the SV-COMP PR #1532, would you want to add/remove/change anything in this PR?

tautschnig · 2017-11-02T17:35:41Z

Otherwise this needs input/approval from 1) @thk123 to confirm that test-gen is not negatively impacted and 2) @kroening to confirm the code changes make sense.

marek-trtik · 2017-11-02T18:04:45Z

@tautschnig : I merged all commits of this PR into the PR #1532. The correctness can be easily checked as log messages of commits match (here and in #1532).

thk123 · 2017-11-02T18:08:51Z

@tautschnig Bump updated - waiting on CI - will try and post once it passes, though if anyone from DB see's that is has passed then it is fine to merge.

tautschnig · 2017-11-02T18:18:44Z

Thank you! We certainly need @kroening to weigh in on this one.

marek-trtik · 2017-11-03T10:01:59Z

I think clang-formater issues should also be handled before merge. (Which I already did in #1532).

thk123 · 2017-11-03T15:29:13Z

This is OK from a TG perspective 👍

peterschrammel · 2017-11-03T15:30:13Z

And a rebase...

tautschnig · 2017-11-06T12:23:47Z

@marek-trtik Do I have an easy way of cherry-picking the clang-format changes into this PR?

kroening · 2017-11-06T14:48:32Z

src/goto-programs/builtin_functions.cpp

  malloc_expr.copy_to_operands(object_size);
+  // could use true and git rid of the code below
+  malloc_expr.copy_to_operands(false_exprt());


kroening · 2017-11-06T14:51:44Z

src/pointer-analysis/value_set.cpp

-      if(object.offset_is_zero() && i_is_set)
-        object.offset=i;
+      if(object.offset_is_set && i_is_set)
+        object.offset+=i;
      else


Tempting, but there's a reason for what was there before.
The problem is that the above will do a concrete interpretation.
Image passing for(int i=0; i<BIG_NUM; i++) to this.

You would need to add some flag or counter to widen when this case is hit many (=heuristic) times.

I believe that the insert(dest, it->first, object); that follows this code actually takes care of this, unless I'm mistaken? That is, we seem to have taken care of this multiple times?

Ok -- there should really be a comment there, highlighting that this is where the widening happens.

kroening · 2017-11-06T14:53:54Z

Fine minus the problem with the missing widening on integer additions.

marek-trtik · 2017-11-06T16:12:39Z

@tautschnig There is no separate commit fixing the clang-formater for commits of this PR. I already fixed the issues in commits of #363. And so, I only merged updates made in this PR into those commits, with simultaneous fixing of clang-formater issues. The only way I see here is to cherry-pick the corresponding commits from #1532 and then squash them into a single commit fixing clang-formater issues.

tautschnig · 2017-11-06T16:16:49Z

@marek-trtik I'll try to take care of the cherry-picking the next hours or tomorrow morning.

marek-trtik · 2017-11-06T16:51:56Z

@tautschnig CORRECTION: I actually tried to move majority (if not all) clang-formater issues into a separate commit Fixing CPPLINTer/cnang-formater issues.
94aea2a

This attempt was for all commits of the PR #1532. However, I cannot give 100% guarantee that all fixes were moved to that commit.

Anyway, it might still be simpler/faster to cherry-pick only that commit, discard fixes made in files outside your PR, and then manually fix few remaining issues (which I might possibly forget to move to this commit).

See https://groups.google.com/d/msg/cprover-support/FQHJYskRRuI/mKo7EQq9BAAJ for discussion and the source of this regression test. The problem is addressed by the prior commits on this branch/pull request.

__CPROVER_allocate takes two arguments, where the second requests zero-initialization of the newly allocated object. Thus `calloc` can be implemented efficiently.

tautschnig · 2017-11-06T17:13:42Z

I've merged into the commits the changes as I deemed that fit for this PR. @marek-trtik I think a subsequent rebase on top of develop, once this PR is merged, should now be relatively painless.

marek-trtik · 2017-11-06T17:16:56Z

@tautschnig Yes, I should be easy.

tautschnig · 2017-11-07T11:13:10Z

@kroening Any opinions on my comments?

e8b3cb9 Merge remote-tracking branch 'upstream/develop' into smowton/merge/develop_20171116 dc4a293 Merge pull request diffblue#1594 from reuk/reuk/cmake-fixup 48fc3d4 Merge pull request diffblue#1592 from antlechner/antonia/char-escape 538eef6 Merge pull request diffblue#1577 from smowton/smowton/fix/dependence_graph_inconsistency d3d632d Use multi-argument form of FILE command 81e56cc Tidy up CMakeLists f7141c0 Merge pull request diffblue#1582 from romainbrenguier/refactor/numerical-cast 8ed1023 Use UTF-16 conversion function in expr2java a53f5bf Split UTF-16 conversion code into two cases e0ad069 Merge pull request diffblue#1558 from NathanJPhillips/feature/complete-journalling_symbol_table 69d1a52 Added usages of base class symbol table 3e42a8d Add comment on has_symbol a2b45e3 Update to journalling symbol table 7aa80ad Remove lookup_impl - it won't work for recording symbol table and adds complexity cdbac8c Sort output of symbol_tablet::show 2ef1c94 Fix bug where move from const symbol collections 8035397 Style improvements 6dae8e8 Merge pull request diffblue#1515 from smowton/smowton/admin/codeowners 5297646 another ranged for 3d66779 Merge branch 'develop' of github.com:diffblue/cbmc into develop 4b5467c another ranged for f5dbfd4 Merge pull request diffblue#1589 from reuk/reuk/fewer-exceptions 8e99272 use ranged for 95cf5c3 Add directories without code owners and adapt code owners 8da6a81 Replace try-catch with nullptr checks 9ff48e0 Add numeric_cast template for numeric conversion af31813 Merge pull request diffblue#1575 from svorenova/nested_generics_tg1301 21b4e7e Extend unit tests to test for nested generics cf47dcb Extending parsing of generics to parse nested generic types 1aefb09 Merge pull request diffblue#1547 from smowton/smowton/feature/remove_virtual_functions_single_call 2b4ed77 Merge pull request diffblue#1579 from smowton/smowton/fix/cmdline_destructor 7305506 Merge pull request diffblue#1580 from smowton/smowton/fix/cast_materialised_temporary 87b9de1 Remove pointless typecasts a59dea6 Add unit test checking dependence graph consistency 80e66ba Remove virtual functions: expose single-call entry-point ffe02e4 Remove useless cmdlinet::clear() call ae34e9b Merge pull request diffblue#1578 from thk123/bugfix/specalised-classes 779d0aa Merge pull request diffblue#1574 from diffblue/taint-memcpy-develop 28a4846 Merge pull request diffblue#1568 from smowton/smowton/fix/java_div_by_zero ffd089f Constructed class to mimic the original class in all but name of symbol 7f53f02 Merge pull request diffblue#1569 from thk123/bugfix/TG-1403/generic-field-arrays 1abc75e Dependence graph: ensure grapht representation is consistent with domain e03b0cb Abstract interpreter: add finalize hook fa7d62a Makefile for goto-analyzer-taint-ansi-c 758ebb3 transfer taint on memcpy and memmove d0a844b Assert denominator non-zero when Java runtime exceptions are disabled e5744b2 Reorder code owner definition according to change risk 0f98cb4 Removed redundant if statement ffa104c Enforce condition that generic references must refer to generic classes 6e06fbd Extending tests to deal with specialising with arrays when array fields a01a0f2 Extend the specialisation code to handle generic fields 1ccbf83 Correctly handle generic classes that have a array field f60d8c8 Unit utility for symbol types 21a33fa Renaming to_java_generic_class_type to remove spurious s 94ffce3 Merge pull request diffblue#1567 from mgudemann/mgudemann/feature/support_arrays_in_generic_parameters 5be97db Create new and adapt existing unit tests for generic array param ef6b4af Post-fix arrays as generic types with their element type 4db6fc6 Merge pull request diffblue#1553 from mgudemann/bugfix/initialize_pointer_width_in_unit_test b17ed58 Merge pull request diffblue#1555 from thk123/feature/remove-redundant-specalisation-code 9b34cdb Merge pull request diffblue#1564 from owen-jones-diffblue/bugfix/object-numbering-references 52d4326 Merge pull request diffblue#731 from tautschnig/more-rewriting 51133db Remove test checking don't specalise unspecalised generic types bf10b1b Manually call specalisation code bba9f76 Remove redundant regression test 3047678 Removed old method of specalising generics 2db8c45 Merge pull request diffblue#982 from tautschnig/pointer-handling fb532e8 Generalize ID_malloc to ID_allocate with optional zero-init 3c47ccb Use invariant annotations instead of asserts ebd5343 More unwinding should not yield additional assertion failures cc659c9 Use a known constant offset when dereferencing c507ccf Update all constant offsets, not just 0 0361c2a Merge pull request diffblue#1534 from svorenova/unit-test-cleanup f653f85 Merge pull request diffblue#263 from diffblue/owen/fix-memory-bug ede0e8c Fix bug that can cause segfault 51cbfc9 Deleting a utility function for generics 03438bb Disabling part of unit test due to a bug e3019f2 Extending test for derived generics f5ec45a Adding JIRA tickets cont. 1fa8e2f Adding unit test for generic fields 398c88a Applying new utility functions for generics cce7814 Refactoring unit test utility functions to make them easier to use c1e1ba2 Applying new function for accessing elements of arrays e908f0c Updating utility functions to check generic/non-generic java classes d9d9ea1 Cleaning includes, unifying scenario names, adding JIRA references 2883bb1 Extending test for generic arrays de97e23 Adding unit test for nested generics c9a3716 Adding unit test for functions with generics 9db9947 Extending test for generic class 89b99ce Extending test for generic functions 3e6cf35 Extending test for signature/descriptor mismatch 80be2fd Extending and cleaning test for generic class with generic inner classes 2e2e34b Renaming unit test for generic inner classes to bounded generic inner classes c5b06e6 Breaking the old parse_generic_class into two unit tests d3ff11c Adding a utility for checking java generic class 707ebf6 Cleaning existing unit tests af3efea Renaming java files 14c00dc Simplify all expressions generated by flatten_byte_operators 71e9642 Extensions to simplify_byte_extract 81943f2 Split ID_and/ID_or vs ID_xor simplification 77236cc Avoid nesting of ID_with/byte_update by rewriting byte_extract to use the root object ddd3d03 Extended simplify for byte_update, typing 7064483 simplify_typecast: simplify more pointer arithmetic 2b18e0c Merge pull request diffblue#1562 from NathanJPhillips/feature/extend-main_function_result 599a2f9 Merge pull request diffblue#264 from diffblue/smowton/fix/slice24_include de905e7 slice24 test: switch from malloc.h to stdlib.h 89a1132 Merge pull request diffblue#1559 from NathanJPhillips/bugfix/variable-scope 0aeb459 Tidied up get_main_symbol af2d3dd Merge pull request diffblue#1560 from NathanJPhillips/bugfix/catch-by-const-ref c8efb6f Fix bug that can cause segfault b7cc0ae Merge pull request diffblue#1561 from NathanJPhillips/bugfix/erroneous-replacement 7d66469 Typo in reachable 7de4858 Added copyright notice to fix linting error 476270b catch by const ref instead of by value or non-const ref 2f32aee Fixed scope of moved symbol 5057c57 Merge pull request diffblue#1557 from janmroczkowski/janmroczkowski/further-improvements-to-unified_difft 5e067bf Merge pull request diffblue#1481 from andreast271/do-c++-regression c9b6c42 Merge pull request diffblue#1513 from romainbrenguier/feature/input-string-printable c4486f1 Merge pull request diffblue#1552 from thk123/feature/goto-functions-utilities 2648cbb Make unified_difft::lcss return by value cd1258a Merge pull request diffblue#1425 from romainbrenguier/feature/java_new_array_data 6e3a0b0 Make more member function static 9efb65c Merge pull request diffblue#1556 from diffblue/revert-1554-janmroczkowski/more-static-member-functions-in-unified_difft 1c96ae5 Revert "Make more member function static in unified_difft" 9cb4569 Amend doxygen comments 4550676 Added missing utilities to the Makefile 7938bac Correcting linting errors 25d765b Use a for loop rather than chained algorithms e67d229 Renamed find declaration method fa14b47 Renamed utility file to require_goto_statements a657ec1 Moved functions into a namespace and documented them b96199f Moved and simplified the code for finding sub statements b9914a8 Add some java testing utilities. 2c175bd Update load_java_class to construct the entry point function 3453a89 Merge pull request diffblue#1554 from janmroczkowski/janmroczkowski/more-static-member-functions-in-unified_difft feaa85f Merge pull request diffblue#1455 from romainbrenguier/doc/string-solver-documentation c5ab866 Merge pull request diffblue#1430 from romainbrenguier/refactor/gather_indices fac9dea Rename "#lva_mode" to "lvsa_mode" 72c8533 Make two irep IDs 55b6ac5 Merge pull request diffblue#1502 from tautschnig/merge-failed-tests-printer dfa2ed2 Make more member function static d378980 Style: Disabling clang-format in get f5991ee Refactor universal_only_in_index to use expression iterators 9d1aa99 Correct constraints added for char_set e125e8a Refactor gather_indices to use for_each instead of visitor 4b0e2d4 Create goto-gcc symlink in cmake builds and enable goto-gcc tests 7736672 Style: use NOLINTNEXTLINE to avoid cpplint errors on long links 6016bef Improve readability of code imported from failed-tests-printer.pl dd6e431 test.pl: Use native perl instead of "cat" to print log file 3321735 Move implementation of failed-tests-printer.pl into test.pl ba16006 Do not use shell built-ins 96e169a Use single quotes for Windows compatibility d2c3752 Remove string_printable option from the solver b0de0e3 Test for string printable option on input strings 4b36fc6 Merge pull request diffblue#1533 from mgudemann/fix/support_class_bounds_generics 35096b8 Initialize architecture in `instantiate_not_contains` unit test b25630a Merge pull request diffblue#1550 from chrisr-diffblue/cleanup/java-generics-test-helpers 542a26d Stop adding printable constraints on all strings e65e340 Use command line option for string-printable param 8e92362 Propagate string-printable option in object_factory ae5f32e Add a printable option to string initialization 514e6a1 Add function to call constrain_character primitive 1d92c48 Add string primitive to constrain characters cb01526 Minor refactoring in add_default_axioms e1280cc Add utility function add_constraint_on_characters 6b88eb8 Add unit test for class / interface bound 2ed059a Support interface and class bound parsing in generics ccdd483 Merge pull request diffblue#1545 from chrisr-diffblue/TG-1158/unit-test-for-specialising-with-array-types 73808aa Merge pull request diffblue#1544 from smowton/smowton/feature/value_set_eq_operator 0507355 Refactored unit test helpers to be more general and extend their use-cases 93ebb84 Merge commit '356aed461b387a8ae815a9901a16d26f32f102be' into develop db758fb Add some unit test helper functions, useful for Java generics unit tests 98de899 Add a unit test for specialising Java generic types with array types b07fcdd Documentation improvements and readme for strings 1fa64a9 Avoid using is_valid_java_array in builin_functions 0dafac2 Add unit test for goto_trace_output in Makefile 435958f Unit test for goto_trace::output 5a0343f Doc: Summary for count_type_leaves fc363b3 Typo in goto_trace output 42c079d Use existing function for checking object is array 465e5dc Style: improve documentation in interpreter evaluate fe2efa7 Style: Replace assert by appropriate macros e36d7d8 Check if object is nil before writing trace 6b519ad Add identifier and rename statement to java_new_array_data d4f1b29 Add eq and neq operators to value_sett and related types b03ec16 Merge pull request diffblue#239 from diffblue/bugfix/value_sets_fi_and_reaching_defs_retrievals_of_dynamic_objects db79106 Added explanatory comment for the introduced condition. dfc6a20 Fixing C++ code-style issues. b0742cf Disable cbmc-cpp tests in appveyor, which runs regression on windows. All cbmc-cpp tests #include <assert.h> and cbmc cannot yet parse Microsoft C++ headers. d55a8da Add tests to cmake regression: cbmc-cover, cbmc-cpp, goto-analyzer-taint 3a4e48c Run cbmc c++ regression as part of default regression test Set is_parameter for c++ function parameter symbol 7989831 Added regression test for the fixed bug. 00b4af2 Bugfix: Explicit retrievals of DOs from value_set amd reaching_defs. git-subtree-dir: cbmc git-subtree-split: e8b3cb9

tautschnig force-pushed the pointer-handling branch 5 times, most recently from 475791e to 9a1bcbb Compare June 8, 2017 08:56

peterschrammel reviewed Jun 25, 2017

View reviewed changes

tautschnig force-pushed the pointer-handling branch from 9a1bcbb to a1070c8 Compare June 28, 2017 14:55

tautschnig force-pushed the pointer-handling branch 2 times, most recently from 88922e1 to 7e5eb9e Compare July 3, 2017 10:01

tautschnig mentioned this pull request Jul 4, 2017

Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

Closed

tautschnig force-pushed the pointer-handling branch from 7e5eb9e to 2c21e90 Compare July 10, 2017 19:43

tautschnig added the bugfix label Jul 10, 2017

tautschnig force-pushed the pointer-handling branch 3 times, most recently from 52d7bf4 to 66d250f Compare July 15, 2017 18:21

kroening self-assigned this Jul 17, 2017

tautschnig force-pushed the pointer-handling branch 2 times, most recently from cb082fa to cc95625 Compare July 19, 2017 09:17

tautschnig force-pushed the pointer-handling branch from cc95625 to e798e5a Compare August 7, 2017 12:15

tautschnig requested review from smowton and kroening August 14, 2017 13:18

smowton reviewed Aug 15, 2017

View reviewed changes

tautschnig force-pushed the pointer-handling branch 2 times, most recently from f71c1b5 to 4ec24f4 Compare August 16, 2017 07:27

tautschnig changed the base branch from master to develop August 22, 2017 12:23

tautschnig force-pushed the pointer-handling branch 3 times, most recently from ea2ebba to fd38768 Compare September 1, 2017 13:20

tautschnig assigned thk123 Nov 2, 2017

tautschnig force-pushed the pointer-handling branch from 7495a32 to ebff9ee Compare November 6, 2017 12:20

kroening reviewed Nov 6, 2017

View reviewed changes

tautschnig force-pushed the pointer-handling branch from ebff9ee to 37ee372 Compare November 6, 2017 15:05

tautschnig and others added 5 commits November 6, 2017 17:11

Update all constant offsets, not just 0

c507ccf

Use a known constant offset when dereferencing

cc659c9

Use invariant annotations instead of asserts

3c47ccb

Generalize ID_malloc to ID_allocate with optional zero-init

fb532e8

__CPROVER_allocate takes two arguments, where the second requests zero-initialization of the newly allocated object. Thus `calloc` can be implemented efficiently.

tautschnig force-pushed the pointer-handling branch from 37ee372 to fb532e8 Compare November 6, 2017 17:11

kroening merged commit 2db8c45 into diffblue:develop Nov 7, 2017

tautschnig deleted the pointer-handling branch November 8, 2017 10:43

		address_of_exprt rhs;

		symbol_exprt v=value_symbol.symbol_expr();

Fixes and improvements to dynamic memory handling #982

Fixes and improvements to dynamic memory handling #982

Conversation

tautschnig commented Jun 1, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Jun 28, 2017

tautschnig commented Aug 14, 2017

smowton 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

tautschnig commented Nov 2, 2017

tautschnig commented Nov 2, 2017

marek-trtik commented Nov 2, 2017

thk123 commented Nov 2, 2017

tautschnig commented Nov 2, 2017

marek-trtik commented Nov 3, 2017 • edited Loading

thk123 commented Nov 3, 2017

peterschrammel commented Nov 3, 2017

tautschnig commented Nov 6, 2017

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

kroening commented Nov 6, 2017

marek-trtik commented Nov 6, 2017 • edited Loading

tautschnig commented Nov 6, 2017

marek-trtik commented Nov 6, 2017 • edited Loading

tautschnig commented Nov 6, 2017

marek-trtik commented Nov 6, 2017

tautschnig commented Nov 7, 2017

marek-trtik commented Nov 3, 2017 •

edited

Loading

marek-trtik commented Nov 6, 2017 •

edited

Loading

marek-trtik commented Nov 6, 2017 •

edited

Loading