From 9810f9286666ca7c6d8f07b9ccbdc438a0cc4e55 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Jan 2018 09:43:39 +0000 Subject: [PATCH 1/2] Drop string_non_empty field for string refinement --- src/cbmc/cbmc_solvers.cpp | 1 - src/solvers/refinement/string_refinement.h | 2 -- 2 files changed, 3 deletions(-) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index d9c245b5b7a..825f1b855de 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -178,7 +178,6 @@ std::unique_ptr cbmc_solverst::get_string_refinement() info.ui=ui; if(options.get_bool_option("string-max-length")) info.string_max_length=options.get_signed_int_option("string-max-length"); - info.string_non_empty=options.get_bool_option("string-non-empty"); info.trace=options.get_bool_option("trace"); if(options.get_bool_option("max-node-refinement")) info.max_node_refinement= diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 8e4a3432703..cab3aff3328 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -49,8 +49,6 @@ class string_refinementt final: public bv_refinementt struct configt { std::size_t refinement_bound=0; - /// Make non-deterministic character arrays have at least one character - bool string_non_empty=false; /// Concretize strings after solver is finished bool trace=false; bool use_counter_example=true; From 5a8eea5cdb062f454ec51ca27a2793225ce49543 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Jan 2018 09:46:45 +0000 Subject: [PATCH 2/2] Remove the string-non-empty option This had no effect on the solver, so should not be used. --- src/cbmc/cbmc_parse_options.cpp | 2 -- src/cbmc/cbmc_parse_options.h | 1 - src/jbmc/jbmc_parse_options.cpp | 2 -- src/jbmc/jbmc_parse_options.h | 1 - 4 files changed, 6 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 29493dd0dbb..156335ae95f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -271,7 +271,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("refine-strings")) { options.set_option("refine-strings", true); - options.set_option("string-non-empty", cmdline.isset("string-non-empty")); options.set_option("string-printable", cmdline.isset("string-printable")); if(cmdline.isset("string-max-length")) options.set_option( @@ -1009,7 +1008,6 @@ void cbmc_parse_optionst::help() " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" " --refine-strings use string refinement (experimental)\n" - " --string-non-empty add constraint that strings are non empty (experimental)\n" // NOLINT(*) " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) " --string-max-length add constraint on the length of strings\n" // NOLINT(*) " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 9c46c7ee2ab..beb1fbd631f 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -44,7 +44,6 @@ class optionst; "(no-pretty-names)(beautify)" \ "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ "(refine-strings)" \ - "(string-non-empty)" \ "(string-printable)" \ "(string-max-length):" \ "(string-max-input-length):" \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index d699212aa5a..2dc4dee67b0 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -246,7 +246,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("refine-strings")) { options.set_option("refine-strings", true); - options.set_option("string-non-empty", cmdline.isset("string-non-empty")); options.set_option("string-printable", cmdline.isset("string-printable")); if(cmdline.isset("string-max-length")) options.set_option( @@ -910,7 +909,6 @@ void jbmc_parse_optionst::help() " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" " --refine-strings use string refinement (experimental)\n" - " --string-non-empty add constraint that strings are non empty (experimental)\n" // NOLINT(*) " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) " --string-max-length add constraint on the length of strings\n" // NOLINT(*) " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index a80a8300f01..06e0b47144d 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -44,7 +44,6 @@ class optionst; "(no-pretty-names)(beautify)" \ "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ "(refine-strings)" \ - "(string-non-empty)" \ "(string-printable)" \ "(string-max-length):" \ "(string-max-input-length):" \