Fix-up to nondet-static option [TG-4365] #2643

majakusber · 2018-07-31T15:00:21Z

This PR makes nondet-static option behave in a bit cleaner way:

we only nondet-initialize custom static fields (before we would also nondet-initialize our variables such inflight_exception etc),
we replace the original line of CPROVER_init that set the value of a static variable with a line that nondet-initializes it (before we would add the new line after the original assignment).

majakusber · 2018-07-31T15:02:45Z

Test-gen pointer bump: https://github.com/diffblue/test-gen/pull/2112

tautschnig

Please review whether adding a flag (and in particular one that doesn't seem to be widely used) to symbolt is the right design choice. If yes, more changes are required as indicated below.

tautschnig · 2018-07-31T19:36:38Z

src/util/symbol.h

@@ -68,6 +68,10 @@ class symbolt
  bool is_lvalue, is_file_local, is_extern, is_volatile,
       is_parameter, is_auxiliary, is_weak;

+  // Can a static variable be nondet-initialized? User static variables can be
+  // but proprietary ones no (e.g., inflight_exception, clinit_already_run etc)
+  bool is_static_nondet_init = false;


This new field needs to be serialised and de-serialiased when writing/reading goto binaries. Also text output needs to be updated.

Why not just is_nondet_init (or some more grammatically correct name)? (The static information is already in is_static_lifetime if needed).

tautschnig · 2018-07-31T19:37:50Z

src/goto-instrument/nondet_static.cpp

@@ -31,7 +31,7 @@ void nondet_static(

  Forall_goto_program_instructions(i_it, init)
  {
-    const goto_programt::instructiont &instruction=*i_it;
+    const goto_programt::instructiont instruction=*i_it;


Why take a copy?

In case the instruction will be overriden, I need some info from the original instruction as it's being overriden (and without making a copy it gets into a loop). I could also make a copy of it only at point when I actually need it.

tautschnig · 2018-07-31T19:38:12Z

src/goto-instrument/nondet_static.cpp

@@ -54,7 +54,7 @@ void nondet_static(
      if(is_constant_or_has_constant_components(sym.type(), ns))
        continue;

-      i_it=init.insert_before(++i_it);
+      //i_it=init.insert_before(++i_it);


This line should just be removed?

Yes, it definitely should have been.

peterschrammel

PR seems incomplete at the moment.

peterschrammel · 2018-07-31T19:42:52Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -635,6 +635,7 @@ void java_bytecode_convert_classt::convert(
    symbolt new_symbol;

    new_symbol.is_static_lifetime=true;
+    new_symbol.is_static_nondet_init=true;


The commit message could be more informative (e.g. Add is_static_nondet_init to symbol)

peterschrammel · 2018-07-31T19:46:32Z

src/goto-instrument/nondet_static.cpp

@@ -46,6 +46,10 @@ void nondet_static(
      if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
        continue;

+      // static that can be nondet initialized?
+      if(!ns.lookup(sym.get_identifier()).is_static_nondet_init)


Could this replace the __CPROVER prefix check above? (These variables should all have static lifetime anyway?)

peterschrammel · 2018-07-31T19:49:52Z

src/util/symbol.h

@@ -68,6 +68,10 @@ class symbolt
  bool is_lvalue, is_file_local, is_extern, is_volatile,
       is_parameter, is_auxiliary, is_weak;

+  // Can a static variable be nondet-initialized? User static variables can be
+  // but proprietary ones no (e.g., inflight_exception, clinit_already_run etc)
+  bool is_static_nondet_init = false;


Why not just is_nondet_init (or some more grammatically correct name)? (The static information is already in is_static_lifetime if needed).

majakusber · 2018-08-01T09:14:10Z

From design point of view - we discussed this design with Peter, and it sounded like the cleanest solution. Although CI shows that this breaks how nondet-static works for C. So option (1) would be to keep the new field and correctly set it for fields in Java (this seems easy) and in C (this does not seem that easy as symbols are being created at many places and it's not obvious which ones are user/private). On the other hand, it seems that in C nondet-static was working correctly before the changes so option (2) would be to only fix how it works for Java by adding additional cases in nondet-static.cpp, namely if it's @inflight_exception or ..::clinit_already_run or java.String.Literal (all these are anyway used in Java only?) do not nondet-initialize it. The advantage of option (2) is that it won't break anything that is already working.

majakusber · 2018-08-01T10:07:18Z

@tautschnig @peterschrammel Here is my branch with option (2) implemented: develop...svorenova:fixup-nondet-static-2

peterschrammel · 2018-08-01T13:12:23Z

svorenova:fixup-nondet-static-2 is not an option.

peterschrammel · 2018-08-01T13:13:18Z

Looking at it again, I think using an ID_C comment is more appropriate. This is done similarly in comparable situations such as constant and initialization_required.

smowton

I'd say almost certainly rather than make a new symbol flag, either maintain the information you need (presumably a set of symbol IDs to reinit) elsewhere, or perhaps tag the symbol using a comment on its type, as e.g. already done to record a method's defining class, here: https://github.com/diffblue/cbmc/blob/develop/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp#L448)

That strategy isn't clean by any stretch of the imagination, but it does at least preserve the serialized (GBF) format and thus only impacts code that uses the new information.

smowton · 2018-08-01T14:02:27Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -635,6 +635,7 @@ void java_bytecode_convert_classt::convert(
    symbolt new_symbol;

    new_symbol.is_static_lifetime=true;
+    new_symbol.is_static_nondet_init=true;


I wouldn't, this will break GBF compatibility across this change, for example

smowton · 2018-08-01T14:07:16Z

(The long-term plan is for symbols to have an additional attributes irep for this sort of thing)

majakusber · 2018-08-01T15:37:40Z

I've re-implemented this using a new comment. Let me know what you think.

smowton · 2018-08-01T15:39:57Z

src/goto-instrument/nondet_static.cpp

+      // should not be nondet-initialized, e.g., proprietary variables?
+      if(
+        ns.lookup(sym.get_identifier())
+          .type.get_bool(ID_C_no_nondet_initialization_allowed))


Presumably also check for ID_C_constant?

Constants are checked below, using is_constant_or_has_constant_components

smowton · 2018-08-01T15:40:55Z

Better! I liked your suggestion of replacing clinit methods though rather than returning all this stuff to __CPROVER_initialize, did that plan not go anywhere?

majakusber · 2018-08-01T16:02:03Z

@smowton Yes, that change will follow in a separate PR. This PR only cleans up nondet-static a bit but we would still call static initializer. The following PR will make sure that even in the static initializer wrapper we only nondet initialize variables.

smowton

@peterschrammel @tautschnig maybe you can think of a better name for "this is internal state, nondet-static shouldn't trash it"?

smowton · 2018-08-01T16:37:01Z

src/goto-instrument/nondet_static.cpp

      // static lifetime?
      if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
        continue;

+      // should not be nondet-initialized, e.g., proprietary variables?
+      if(


Braces around multi-line if

smowton · 2018-08-01T16:38:37Z

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -24,6 +24,7 @@ void java_internal_additions(symbol_table_baset &dest)
    symbol.base_name="__CPROVER_rounding_mode";
    symbol.name=CPROVER_PREFIX "rounding_mode";
    symbol.type=signed_int_type();
+    symbol.type.set(ID_C_no_nondet_initialization_allowed, true);


Maybe ID_C_is_internal_state? Contrasting user static variables? No strong opinion though.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: ec4d5cd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80742567
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: f0dc854).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80752951

martin-cs

I don't want to say #751 BUT ... what is the correct way of marking that a variable is "internal only" and what should that mean for different transformations?

martin-cs · 2018-08-02T18:55:30Z

src/goto-instrument/nondet_static.cpp

@@ -38,10 +38,6 @@ void nondet_static(
      const symbol_exprt &sym=to_symbol_expr(
          to_code_assign(instruction.code).lhs());

-      // is it a __CPROVER_* variable?


If we are going to switch from marking internal / CPROVER generated variables by a CPROVER_PREFIX and instead use this new comment attribute, please could we do it across the whole code-base as I doubt that nondet-static is the only place that makes this distinction.

Also, "change how we mark internal variables" is a bigger change that should be in a PR marked "Fix-up nondet-static".

While I agree with what Martin said (that we should reconsider various __CPROVER_ prefixed symbols): 1) for several of them the main purpose of the prefix is disambiguation (avoid conflicts with user-provided symbols; 2) let's not ask for huge extra work going well beyond the purpose of the PR (this is happening in several PRs and often stalls progress) - create an issue so that it isn't forgotten instead.

OK; I'm just want to avoid a proliferation of undocumented, slightly disjoint conventions for what are "internal" variables.

martin-cs · 2018-08-02T18:57:53Z

src/goto-instrument/nondet_static.cpp

      // static lifetime?
      if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
        continue;

+      // should not be nondet-initialized, e.g., proprietary variables?


Terminological nit-picking but ... what is a proprietary variable in an open source system?

tautschnig

I like this approach. I think there are various details that can (and likely should) be improved as noted by the reviewers, but they should all be reasonably easy to address.

tautschnig · 2018-08-02T19:09:46Z

src/util/irep_ids.def

@@ -665,6 +665,7 @@ IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
+IREP_ID_TWO(C_no_nondet_initialization_allowed, #no_nondet_initialization_allowed)


A bit of nit-picking: "allowed" - who sets those rules? Do I get jailed if I do a nondet-init? :-) More seriously: The commit message, which is the only documentation here, provides examples, but doesn't really set out the rules. Effectively the commit message will need to set out the semantics.

Do I get jailed if I do a nondet-init?

You get punished with false alarms.

I'll leave out the allowed to make it clear - just no nondet-init, period, don't even try :) I will also amend the commit message in lines with my last message - marking internal variables that are not CPROVER variables, language specific internal variables.

tautschnig · 2018-08-02T19:14:57Z

src/goto-instrument/nondet_static.cpp

@@ -38,10 +38,6 @@ void nondet_static(
      const symbol_exprt &sym=to_symbol_expr(
          to_code_assign(instruction.code).lhs());

-      // is it a __CPROVER_* variable?


While I agree with what Martin said (that we should reconsider various __CPROVER_ prefixed symbols): 1) for several of them the main purpose of the prefix is disambiguation (avoid conflicts with user-provided symbols; 2) let's not ask for huge extra work going well beyond the purpose of the PR (this is happening in several PRs and often stalls progress) - create an issue so that it isn't forgotten instead.

peterschrammel · 2018-08-02T19:25:38Z

replacing clinit methods though rather than returning all this stuff to __CPROVER_initialize, did that plan not go anywhere?

@smowton, the second part of the static nondet fixes are in #2658.
The third part will then de-duplicate the static initialisations that Java does in two different places.

peterschrammel · 2018-08-02T19:27:58Z

better name for "this is internal state

The naming is more explicit on purpose because there might not only be 'internal' variables that must not be nondet-initialised. But I'm also fine with calling it differently.

(since when does Github post when you press Enter... grrrrr)

majakusber · 2018-08-03T07:28:35Z

As Peter mentioned the new comment is supposed to identify variables beyond _CPROVER variables that we do not want to nondet-initialize - for example @inflight_excpetion is not a CPROVER variable and it probably shouldn't be (it's only used in Java?). Now that I think about it, it makes sense to leave the check for CPROVER variables in nondet-static and really consider the new comment as a mean to mark things in the grey zone between core CPROVER variables and user defined variables such as language specific internal variables. Would you agree?

majakusber · 2018-08-03T08:02:26Z

I now pushed the changes along the lines of my previous comment. These should be reflecting all the comments.

I also changed how the last commit works as I learned about make_skip(), remove_skip(goto_programt) yesterday ;)

…ized This will be used by nondet-static option and will mark internal variables that are not CPROVER variables such as language specific internal variables - in Java, for example, @inflight_exception and clinit_already_run

This sets the flag to be true for java::@inflight_exception and static initializer internal variables (including clinit_already_run)

This will also make sure that nondet-static option does not nondet- initialize these

martin-cs · 2018-08-03T10:27:57Z

On Fri, 2018-08-03 at 00:28 -0700, svorenova wrote: As Peter mentioned the new comment is supposed to identify variables beyond _CPROVER variables that we do not want to nondet-initialize - for example ***@***.***_excpetion` is not a CPROVER variable and it probably shouldn't be (it's only used in Java?).

Rounding mode is already a language specific CPROVER variable. I don't know what the inflight exception does but if it's part of the model that CPROVER constructs of how the program works, then maybe it should be.

Now that I think about it, it makes sense to leave the check for CPROVER variables in nondet-static and really consider the new comment as a mean to mark things in the grey zone between core CPROVER variables and user defined variables such as language specific internal variables. Would you agree?

That's part of why I asked the question. I think the behaviour for CPROVER variables should stay unchanged. I can see a case for adding an extra if statement checking for an ID_C_block_nondet_static if you want additional options of blocking which global variables get non- det'd (although, is it better as an argument to nondet static?). This would be making clear that this is just a flag for that one piece of functionality and not about a general treatment of "internal" variables. Ofcourse, if you want something that marks a global variable as "internal" (apart from CPROVER prefixes) and affects multiple subsystems, then that is a different issue and should be addressed differently. But I don't think that is the case here?

martin-cs

Thanks for the changes; LGTM now.

Instead of keeping both the original line that sets the value of a variable and the new line that nondet initializes it, we only keep the new one

majakusber · 2018-08-03T10:44:18Z

I had to revert the last commit, make_skip, remove_skip was misbehaving. @martin-cs That's right, the comment should only affect nondet-static.

majakusber · 2018-08-03T10:48:05Z

@martin-cs By language specific variable I meant a variable that only exists for particular languages, not necessarily all that we support, such as inflight_exception which in Java determines whether there is an uncaught exception at any given time. I didn't mean that their value is dependent on the chosen language.

martin-cs · 2018-08-03T11:00:54Z

On Fri, 2018-08-03 at 03:48 -0700, svorenova wrote: @martin-cs By language specific variable I meant a variable that only exists for particular languages, not necessarily all that we support, such as inflight_exception which in Java determines whether there is an uncaught exception at any given time. I didn't mean that their value is dependent on the chosen language.

Yes; language specific variables can be and do have CPROVER prefixes.

allredj

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

5d3ea03 Merge pull request diffblue#2693 from zhixing-xu/fix_rw_range_upper 2b40338 Update test.desc c6d0427 Merge pull request diffblue#2674 from diffblue/msvc-link 318474f Merge pull request diffblue#2678 from romainbrenguier/feature/extend-builtin-functions-part3 c63030f Regression test for goto-link personality 64fedd0 Microsoft LINK personality d9f9dd9 Merge pull request diffblue#2688 from tautschnig/concat-dir-file 99946fc Merge pull request diffblue#2675 from diffblue/goto-cl-echo-file 252d857 Merge pull request diffblue#2687 from tautschnig/fo-directory 0d7ebd5 Fixed a problem where the rw_set range's upper bound not set correctly 29eab32 goto-cl: Fail invocation of trying to compile multiple files to non-directory 7f587c4 Fix concat_dir_file for Windows and unit-test it a44468b Document string_builtin_function::eval ecc0e43 Document eval_is_upper_case a345d30 Document eval_string 58307a0 Tests for String.toUpperCase 71de2e3 Tests for String.toLowerCase 579d00c Remove redundant function application ID check e2961b5 Add builtin class for string_to_upper_case fe9071b Make to_upper_case work for Latin-1 supplement 53ccd3f Refactor string_to_upper_case be477c9 Remove assumptions that input char are < 0x100 836cbad Extract an is_upper_case function 1137ffd Improve documentation of add_axioms_for_to_lower_case a71f2c0 Implement builtin string_to_lower_case function fae6a48 Merge pull request diffblue#2467 from tautschnig/vs-except 24de513 Merge pull request diffblue#2474 from tautschnig/vs-identifier e14f2f2 Merge pull request diffblue#2685 from diffblue/clcache-again 08698cc Merge pull request diffblue#2681 from diffblue/remove-aig d42020b remove --aig option cd4a163 AWS codebuild windows: set clcache base directory 1ba928c cleanup unnecessary path from configuration file 8c4801b Refactor add_axioms_for_to_lower_case 4291232 Merge pull request diffblue#2686 from diffblue/buildspec-apt-cache 3adb717 AWS codebuild: cache apt lists and packages 0efb169 remove AIGs 3a9c825 Merge pull request diffblue#2682 from diffblue/fix-clcache b9b5660 Merge pull request diffblue#2483 from tautschnig/vs-java-parameters a66ab1e CL prints the name of the file that's compiled onto stdout 0698a5f Merge pull request diffblue#2673 from diffblue/goto-cl-Fo 75855bf Java front-end: remove unused parameters 4df2187 debugging output to resolve seg fault 5bc7456 goto-cl: /Fo can set an output directory a43e4fa add is_directory to file_util.h 4ad91fb Codebuild for windows: set up cache path properly effb01b Merge pull request diffblue#2641 from diffblue/typedef-type 5ef2802 Merge pull request diffblue#2679 from tautschnig/version-string 2efea52 Refine test patterns to avoid spurious matches aa7ebbc Merge pull request diffblue#2672 from diffblue/goto-cc-multiple-source-files aaea781 Merge pull request diffblue#2671 from diffblue/fix_get_base_name 8b51faf fix get_base_name 694daaf gcc mode: error in case multiple files are given with -c and -o 09fdca3 Merge pull request diffblue#2643 from svorenova/fixup-nondet-static d42054a Merge pull request diffblue#2669 from diffblue/spurious-cover-test b391c9e introduce typedef_type in the C frontend 114030b Merge pull request diffblue#2664 from romainbrenguier/feature/extend-builtin-functions-part2 46f6231 cbmc test no longer uses --cover daff1d1 Make nondet-static replace lines in CPROVER_init 1bca129 Merge pull request diffblue#2665 from tautschnig/gcc-conditional-stmt 31366ad Tests for StringBuilder.setCharAt f4285e7 Add builtin support for string_set_char 2a8ea0f Better specify out-of-bounds case for set_char 9415a24 Refactor add_axioms_for_set_char 9762886 Refactor string_concat_char builtin function b62bf01 Make nondet-static check for ID_C_no_nondet_initialization a50562e Mark java.lang.String.Literals with ID_C_constant b3c08d3 Mark internal Java variables with ID_C_no_nondet_initialization f2dc978 Add a new comment to mark variables that should not be nondet initialized da7966c Merge pull request diffblue#2645 from mmuesly/feature_test_posix_memalign cb4a340 Merge pull request diffblue#2647 from diffblue/cleanout-jar-filet 2b27a2d Merge pull request diffblue#2622 from martin-cs/feature/context-sensitive-ait-merge-2 00b26a8 Adds a test for posix_memalign in stdlib.c 0f5a057 Merge pull request diffblue#2667 from tautschnig/slicer-cleanup 16e6462 Remove no-longer-used ifdef 96d345b Clean GCC conditional expressions in right-hand sides of declarations 086c266 Merge pull request diffblue#2651 from smowton/smowton/feature/unroll-enum-clone-loops f69b244 Merge pull request diffblue#2625 from smowton/smowton/feature/value-set-accuracy 730b3e2 Merge pull request diffblue#2655 from romainbrenguier/feature/extend-builtin-functions c4569dd remove java_class_loader_limitt from jar_filet e0f954d Merge pull request diffblue#2659 from smowton/smowton/fix/cmake-third-time-is-charm 7f547b1 Merge pull request diffblue#2656 from smowton/smowton/fix/testsuite-name 3a1593b Tests for String.valueOf(int) 7414d76 Add builtin support for string_of_int 0b44c89 Add version of make_string accepting iterators f81f082 Rename function to add_axioms_for_string_of_int 9a2a7c2 Switch version.cpp from a rule product to a byproduct 943d60c Value set: handle with, array and struct expressions more accurately 4f158a3 Mark regression tests as expecting failure for symex driven loading c9a53f9 Add regression tests for changes to JBMC enumeration support a985eae Interpreter: deal with member-of-constant-struct expressions 361469b Change source location of jump target in {table|lookup}switch 6270968 java-unwind-enum-static: also unwind clone loop in Enum.values() 714de0d Symex: expose call stack to unwinding decision making fb239ef Fix jbmc-generic-symex-driven-lazy-loading test name 28ba192 Strengthen the invariant on what are acceptable function calls. 773bc86 Convert various comments, asserts and throws into invariants. e65f027 Add comments to the abstract interpreter interface. 1fe0796 Convert various older domains to use the more recent ait API. afe32b7 Refactor the methods that access "the abstract domain at a location". aa743b3 Remove unused exception name from catch statement 5703504 Remove unused parameter identifier git-subtree-dir: cbmc git-subtree-split: 5d3ea03

majakusber self-assigned this Jul 31, 2018

majakusber requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, mgudemann, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners July 31, 2018 15:00

tautschnig requested changes Jul 31, 2018

View reviewed changes

peterschrammel reviewed Jul 31, 2018

View reviewed changes

smowton reviewed Aug 1, 2018

View reviewed changes

majakusber force-pushed the fixup-nondet-static branch 2 times, most recently from 1ea7e9e to bd46eee Compare August 1, 2018 15:36

smowton reviewed Aug 1, 2018

View reviewed changes

smowton approved these changes Aug 1, 2018

View reviewed changes

majakusber force-pushed the fixup-nondet-static branch from bd46eee to ec4d5cd Compare August 2, 2018 11:31

allredj reviewed Aug 2, 2018

View reviewed changes

martin-cs reviewed Aug 2, 2018

View reviewed changes

tautschnig approved these changes Aug 2, 2018

View reviewed changes

majakusber force-pushed the fixup-nondet-static branch from f0dc854 to 1ea8624 Compare August 3, 2018 08:01

majakusber force-pushed the fixup-nondet-static branch 3 times, most recently from 9d038ef to dd44837 Compare August 3, 2018 08:50

svorenova added 4 commits August 3, 2018 10:01

Mark internal Java variables with ID_C_no_nondet_initialization

b3c08d3

This sets the flag to be true for java::@inflight_exception and static initializer internal variables (including clinit_already_run)

Mark java.lang.String.Literals with ID_C_constant

a50562e

This will also make sure that nondet-static option does not nondet- initialize these

Make nondet-static check for ID_C_no_nondet_initialization

b62bf01

majakusber force-pushed the fixup-nondet-static branch 2 times, most recently from 49cd54d to 42e3acf Compare August 3, 2018 09:51

martin-cs approved these changes Aug 3, 2018

View reviewed changes

Make nondet-static replace lines in CPROVER_init

daff1d1

Instead of keeping both the original line that sets the value of a variable and the new line that nondet initializes it, we only keep the new one

majakusber force-pushed the fixup-nondet-static branch from 42e3acf to daff1d1 Compare August 3, 2018 10:40

majakusber changed the title ~~Fix-up to nondet-static option~~ Fix-up to nondet-static option [TG-4365] Aug 3, 2018

majakusber merged commit 09fdca3 into diffblue:develop Aug 3, 2018

majakusber deleted the fixup-nondet-static branch August 3, 2018 12:33

allredj reviewed Aug 3, 2018

View reviewed changes

Fix-up to nondet-static option [TG-4365] #2643

Fix-up to nondet-static option [TG-4365] #2643

Conversation

majakusber commented Jul 31, 2018

majakusber commented Jul 31, 2018

tautschnig 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

peterschrammel 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

majakusber commented Aug 1, 2018 • edited Loading

majakusber commented Aug 1, 2018

peterschrammel commented Aug 1, 2018

peterschrammel commented Aug 1, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Aug 1, 2018

majakusber commented Aug 1, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Aug 1, 2018

majakusber commented Aug 1, 2018

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

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

martin-cs 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

tautschnig 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

peterschrammel commented Aug 2, 2018

peterschrammel commented Aug 2, 2018 • edited Loading

majakusber commented Aug 3, 2018

majakusber commented Aug 3, 2018 • edited Loading

martin-cs commented Aug 3, 2018 via email

martin-cs left a comment

Choose a reason for hiding this comment

majakusber commented Aug 3, 2018

majakusber commented Aug 3, 2018

martin-cs commented Aug 3, 2018 via email

allredj left a comment

Choose a reason for hiding this comment

majakusber commented Aug 1, 2018 •

edited

Loading

peterschrammel commented Aug 2, 2018 •

edited

Loading

majakusber commented Aug 3, 2018 •

edited

Loading