Fix --string-non-empty option #2909

romainbrenguier · 2018-09-06T12:18:04Z

This was broken and the option had no effect

tautschnig

Let's please stop doing any command-line option parsing in the language front-end. Undocumented command-line options are a no-go.

tautschnig · 2018-09-06T12:35:45Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -85,6 +85,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
    object_factory_parameters.max_nondet_string_length =
      safe_string2size_t(cmd.get_value("max-nondet-string-length"));
  }
+  if(cmd.isset("string-non-empty"))
+    object_factory_parameters.min_nondet_string_length = 1;


Can we please not have more command-line parsing in the language front-end? See
#2907 and #2908. Let alone doing so via an undocumented option?

While I remain unhappy it seems that #2908 is not currently progressing so I won't further block on this.

thk123 · 2018-09-10T16:36:02Z

jbmc/src/java_bytecode/object_factory_parameters.h

@@ -28,6 +28,9 @@ struct object_factory_parameterst final
  /// Maximum value for the non-deterministically-chosen length of a string.
  size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;

+  /// Maximum value for the non-deterministically-chosen length of a string.


🚫 ⛏️ Typo: Minimum

romainbrenguier · 2018-10-02T08:31:51Z

@thk123 @tautschnig this is ready for review

thk123

Test is missing one assertion status - please add. Also, any reason to have a binary flag rather than just a min-string-length option?

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc

tautschnig

Ok from my point of view, except the *.desc files as noted below. The where-to-parse-command-line-options is postponed.

tautschnig · 2018-10-02T09:18:15Z

jbmc/regression/jbmc-strings/string-non-empty-option/test.desc

+assertion.* line 13 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 17 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE
+


No blank lines here please, it confuses test runs on Windows. The same applies to the other *.desc files in this commit.

tautschnig · 2018-10-02T09:19:18Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -85,6 +85,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
    object_factory_parameters.max_nondet_string_length =
      safe_string2size_t(cmd.get_value("max-nondet-string-length"));
  }
+  if(cmd.isset("string-non-empty"))
+    object_factory_parameters.min_nondet_string_length = 1;


While I remain unhappy it seems that #2908 is not currently progressing so I won't further block on this.

romainbrenguier · 2018-10-02T09:23:50Z

@thk123

Also, any reason to have a binary flag rather than just a min-string-length option?

No particular reason, I'm just fixing the previously existing feature that was broken, but it could be replaced by a min-string-length option in the future.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 0e36b4d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86575976
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: 2d7e636).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86578648
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: 72350c2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86579860
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: cf123f0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86580449

romainbrenguier requested review from cesaro, cristina-david, mgudemann, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners September 6, 2018 12:18

romainbrenguier force-pushed the bugfix/string-non-empty branch 2 times, most recently from d7f2bf9 to aef2b66 Compare September 6, 2018 12:26

tautschnig requested changes Sep 6, 2018

View reviewed changes

thk123 reviewed Sep 10, 2018

View reviewed changes

tautschnig assigned romainbrenguier Sep 24, 2018

romainbrenguier force-pushed the bugfix/string-non-empty branch from aef2b66 to 5d57dcd Compare September 28, 2018 06:29

romainbrenguier requested a review from martin-cs as a code owner September 28, 2018 06:29

romainbrenguier requested a review from tautschnig September 28, 2018 06:29

romainbrenguier force-pushed the bugfix/string-non-empty branch 2 times, most recently from b25adc2 to 0e36b4d Compare October 2, 2018 08:28

romainbrenguier requested a review from thk123 October 2, 2018 08:29

Fix string non empty option

33a31a1

romainbrenguier force-pushed the bugfix/string-non-empty branch from 0e36b4d to 2d7e636 Compare October 2, 2018 08:31

thk123 reviewed Oct 2, 2018

View reviewed changes

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc Show resolved Hide resolved

tautschnig approved these changes Oct 2, 2018

View reviewed changes

romainbrenguier force-pushed the bugfix/string-non-empty branch from 2d7e636 to 72350c2 Compare October 2, 2018 09:20

Test for the string-non-empty option

cf123f0

romainbrenguier force-pushed the bugfix/string-non-empty branch from 72350c2 to cf123f0 Compare October 2, 2018 09:21

allredj reviewed Oct 2, 2018

View reviewed changes

thk123 approved these changes Oct 2, 2018

View reviewed changes

allredj reviewed Oct 2, 2018

View reviewed changes

peterschrammel approved these changes Oct 2, 2018

View reviewed changes

romainbrenguier merged commit 2c47e04 into diffblue:develop Oct 2, 2018

romainbrenguier deleted the bugfix/string-non-empty branch October 2, 2018 12:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix --string-non-empty option #2909

Fix --string-non-empty option #2909

romainbrenguier commented Sep 6, 2018

tautschnig left a comment

tautschnig Sep 6, 2018

tautschnig Oct 2, 2018

thk123 Sep 10, 2018

romainbrenguier commented Oct 2, 2018

thk123 left a comment

tautschnig left a comment

tautschnig Oct 2, 2018

tautschnig Oct 2, 2018

romainbrenguier commented Oct 2, 2018

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

Fix --string-non-empty option #2909

Fix --string-non-empty option #2909

Conversation

romainbrenguier commented Sep 6, 2018

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Sep 6, 2018

Choose a reason for hiding this comment

tautschnig Oct 2, 2018

Choose a reason for hiding this comment

thk123 Sep 10, 2018

Choose a reason for hiding this comment

romainbrenguier commented Oct 2, 2018

thk123 left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Oct 2, 2018

Choose a reason for hiding this comment

tautschnig Oct 2, 2018

Choose a reason for hiding this comment

romainbrenguier commented Oct 2, 2018

allredj left a 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

allredj left a comment

Choose a reason for hiding this comment