From e1280cc1d05520b63074dc0385599c1d980835ae Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 10:25:25 +0100 Subject: [PATCH 01/10] Add utility function add_constraint_on_characters This generalizes what is done in add_default_axioms for making characters printable. --- .../refinement/string_constraint_generator.h | 5 +++ .../string_constraint_generator_main.cpp | 45 +++++++++++++++---- 2 files changed, 41 insertions(+), 9 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 8d1c9c75546..78286bafe4d 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -109,6 +109,11 @@ class string_constraint_generatort final void add_default_axioms(const array_string_exprt &s); exprt axiom_for_is_positive_index(const exprt &x); + void add_constraint_on_characters( + const array_string_exprt &s, + const exprt &start, + const exprt &end, + const std::string &char_set); // The following functions add axioms for the returned value // to be equal to the result of the function given as argument. diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index d7ff6d98c86..c1afcc30c64 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -324,16 +324,43 @@ void string_constraint_generatort::add_default_axioms( if(max_string_length!=std::numeric_limits::max()) axioms.push_back(s.axiom_for_length_le(max_string_length)); + const exprt index_zero = from_integer(0, s.length().type()); if(force_printable_characters) - { - symbol_exprt qvar=fresh_univ_index("printable", s.length().type()); - exprt chr=s[qvar]; - and_exprt printable( - binary_relation_exprt(chr, ID_ge, from_integer(' ', chr.type())), - binary_relation_exprt(chr, ID_le, from_integer('~', chr.type()))); - string_constraintt sc(qvar, s.length(), printable); - axioms.push_back(sc); - } + add_constraint_on_characters(s, index_zero, s.length(), " -~"); +} + +/// Add constraint on characters of a string. +/// +/// This constraint is +/// \f$ \forall i \in [start, end), low\_char \le s[i] \le high\_char \f$ +/// \param s: a string expression +/// \param start: index of the first character to constrain +/// \param end: index at which we stop adding constraints +/// \param char_set: a string of the form "-" where +/// `` and `` are two characters, which represents +/// the set of characters that are between `low_char` and `high_char`. +/// \return a string expression that is linked to the argument through axioms +/// that are added to the list +void string_constraint_generatort::add_constraint_on_characters( + const array_string_exprt &s, + const exprt &start, + const exprt &end, + const std::string &char_set) +{ + // Parse char_set + PRECONDITION(char_set.length() == 3); + PRECONDITION(char_set[1] == '-'); + const char &low_char = char_set[0]; + const char &high_char = char_set[2]; + + // Add constraint + const symbol_exprt qvar = fresh_univ_index("char_constr", s.length().type()); + const exprt chr = s[qvar]; + const and_exprt char_in_set( + binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())), + binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type()))); + const string_constraintt sc(qvar, start, end, true_exprt(), char_in_set); + axioms.push_back(sc); } /// Adds creates a new array if it does not already exists From cb0152680bf9fd1a2593466daaf07556b9b0a1a2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 10:27:31 +0100 Subject: [PATCH 02/10] Minor refactoring in add_default_axioms --- src/solvers/refinement/string_constraint_generator_main.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index c1afcc30c64..71594f87c0e 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -319,12 +319,12 @@ void string_constraint_generatort::add_default_axioms( if(!created_strings.insert(s).second) return; - axioms.push_back( - s.axiom_for_length_ge(from_integer(0, s.length().type()))); + const exprt index_zero = from_integer(0, s.length().type()); + axioms.push_back(s.axiom_for_length_ge(index_zero)); + if(max_string_length!=std::numeric_limits::max()) axioms.push_back(s.axiom_for_length_le(max_string_length)); - const exprt index_zero = from_integer(0, s.length().type()); if(force_printable_characters) add_constraint_on_characters(s, index_zero, s.length(), " -~"); } From 1d92c4860c8436568f8224b36991d79eb4a04d86 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 10:59:25 +0100 Subject: [PATCH 03/10] Add string primitive to constrain characters This add a constraint on all characters between given index bounds. --- .../refinement/string_constraint_generator.h | 3 ++ .../string_constraint_generator_main.cpp | 28 +++++++++++++++++++ src/util/irep_ids.def | 1 + 3 files changed, 32 insertions(+) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 78286bafe4d..eb4d5aee9a6 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -109,11 +109,14 @@ class string_constraint_generatort final void add_default_axioms(const array_string_exprt &s); exprt axiom_for_is_positive_index(const exprt &x); + void add_constraint_on_characters( const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set); + exprt + add_axioms_for_constrain_characters(const function_application_exprt &f); // The following functions add axioms for the returned value // to be equal to the result of the function given as argument. diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 71594f87c0e..cbc6545ff9b 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -363,6 +363,32 @@ void string_constraint_generatort::add_constraint_on_characters( axioms.push_back(sc); } +/// Add axioms to ensure all characters of a string belong to a given set. +/// +/// The axiom is: \f$\forall i \in [start, end).\ s[i] \in char_set \f$, where +/// `char_set` is given by the string `char_set_string` composed of three +/// characters `low_char`, `-` and `high_char`. Character `c` belongs to +/// `char_set` if \f$low_char \le c \le high_char\f$. +/// \param f: a function application with arguments: integer `|s|`, character +/// pointer `&s[0]`, string `char_set_string`, +/// optional integers `start` and `end` +/// \return integer expression whose value is zero +exprt string_constraint_generatort::add_axioms_for_constrain_characters( + const function_application_exprt &f) +{ + const auto &args = f.arguments(); + PRECONDITION(3 <= args.size() && args.size() <= 5); + PRECONDITION(args[2].type().id() == ID_string); + PRECONDITION(args[2].id() == ID_constant); + const array_string_exprt s = char_array_of_pointer(args[1], args[0]); + const irep_idt &char_set_string = to_constant_expr(args[2]).get_value(); + const exprt &start = + args.size() >= 4 ? args[3] : from_integer(0, s.length().type()); + const exprt &end = args.size() >= 5 ? args[4] : s.length(); + add_constraint_on_characters(s, start, end, char_set_string.c_str()); + return from_integer(0, get_return_code_type()); +} + /// Adds creates a new array if it does not already exists /// TODO: This should be replaced by associate_char_array_to_char_pointer array_string_exprt string_constraint_generatort::char_array_of_pointer( @@ -499,6 +525,8 @@ exprt string_constraint_generatort::add_axioms_for_function_application( res = associate_array_to_pointer(expr); else if(id == ID_cprover_associate_length_to_array_func) res = associate_length_to_array(expr); + else if(id == ID_cprover_string_constrain_characters_func) + res = add_axioms_for_constrain_characters(expr); else { std::string msg( diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ac1f75b7f60..4d4ea1838be 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -772,6 +772,7 @@ IREP_ID_ONE(cprover_string_concat_bool_func) IREP_ID_ONE(cprover_string_concat_double_func) IREP_ID_ONE(cprover_string_concat_float_func) IREP_ID_ONE(cprover_string_concat_code_point_func) +IREP_ID_ONE(cprover_string_constrain_characters_func) IREP_ID_ONE(cprover_string_contains_func) IREP_ID_ONE(cprover_string_copy_func) IREP_ID_ONE(cprover_string_delete_func) From 514e6a1149b0142883df9d79a597ef87eb980784 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 11:10:37 +0100 Subject: [PATCH 04/10] Add function to call constrain_character primitive This is to be used during bytecode conversion to add constraints on characters. --- .../java_string_library_preprocess.cpp | 32 +++++++++++++++++++ .../java_string_library_preprocess.h | 8 +++++ 2 files changed, 40 insertions(+) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index eaac8aaf6fc..9135480da20 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -704,6 +704,38 @@ void add_array_to_length_association( symbol_table)); } +/// Add a call to a primitive of the string solver which ensures all characters +/// belong to the character set. +/// \param pointer: a character pointer expression +/// \param length: length of the character sequence pointed by `pointer` +/// \param char_set: character set given by a range expression consisting of +/// two characters separated by an hyphen. +/// For instance "a-z" denotes all lower case ascii letters. +/// \param symbol_table: the symbol table +/// \param loc: source location +/// \param code [out] : code block to which declaration and calls get added +void add_character_set_constraint( + const exprt &pointer, + const exprt &length, + const irep_idt &char_set, + symbol_tablet &symbol_table, + const source_locationt &loc, + code_blockt &code) +{ + PRECONDITION(pointer.type().id() == ID_pointer); + symbolt &return_sym = get_fresh_aux_symbol( + java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table); + const exprt return_expr = return_sym.symbol_expr(); + code.add(code_declt(return_expr)); + const constant_exprt char_set_expr(char_set, string_typet()); + code.add( + code_assign_function_application( + return_expr, + ID_cprover_string_constrain_characters_func, + {length, pointer, char_set_expr}, + symbol_table)); +} + /// Create a refined_string_exprt `str` whose content and length are fresh /// symbols, calls the string primitive with name `function_name`. /// In the arguments of the primitive `str` takes the place of the result and diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index b02af6bfbcd..d9915655fd4 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -349,4 +349,12 @@ void add_array_to_length_association( const source_locationt &loc, code_blockt &code); +void add_character_set_constraint( + const exprt &pointer, + const exprt &length, + const irep_idt &char_set, + symbol_tablet &symbol_table, + const source_locationt &loc, + code_blockt &code); + #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H From ae5f32e7a58ba554561c4c3d8453915b32bdda4c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 11:13:32 +0100 Subject: [PATCH 05/10] Add a printable option to string initialization This will force characters to be printable when the string is initialized. This is set to false by default for now, but should then be activated when string-printable is given. --- src/java_bytecode/java_object_factory.cpp | 10 +++++++++- src/java_bytecode/java_object_factory.h | 3 ++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 330c5d19a3c..2d96ec23ece 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -542,7 +542,8 @@ codet initialize_nondet_string_struct( const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, - symbol_tablet &symbol_table) + symbol_tablet &symbol_table, + bool printable) { PRECONDITION( java_string_library_preprocesst::implements_java_char_sequence(obj.type())); @@ -605,6 +606,13 @@ codet initialize_nondet_string_struct( add_array_to_length_association( data_expr, length_expr, symbol_table, loc, code); + + // Printable ASCII characters are between ' ' and '~'. + if(printable) + { + add_character_set_constraint( + array_pointer, length_expr, " -~", symbol_table, loc, code); + } } // tmp_object = struct_expr; diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index e731c70998b..a64fcb78796 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -156,6 +156,7 @@ codet initialize_nondet_string_struct( const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, - symbol_tablet &symbol_table); + symbol_tablet &symbol_table, + bool printable = false); #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H From 8e9236271574b0b0de40534d78003189b00cda9e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 13:53:28 +0100 Subject: [PATCH 06/10] Propagate string-printable option in object_factory Note that for now this the default in the parameters is false and this is not affected yet by the command line options. --- src/java_bytecode/java_bytecode_language.h | 3 +++ src/java_bytecode/java_object_factory.cpp | 6 +++++- src/java_bytecode/java_object_factory.h | 2 +- .../java_object_factory/gen_nondet_string_init.cpp | 2 +- 4 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index eac76e3aa06..1cd59afeee1 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -75,6 +75,9 @@ struct object_factory_parameterst final /// dereference a pointer using a 'depth counter'. We set a pointer to null if /// such depth becomes >= than this maximum value. size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH; + + /// Force string content to be ASCII printable characters when set to true. + bool string_printable = false; }; typedef std::pair< diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 2d96ec23ece..60460ffcb21 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -624,6 +624,7 @@ codet initialize_nondet_string_struct( /// content and association of its address to the pointer `expr`. /// \param expr: pointer to be affected /// \param max_nondet_string_length: maximum length of strings to initialize +/// \param printable: Boolean, true to force content to be printable /// \param symbol_table: the symbol table /// \param loc: location in the source /// \param [out] code: code block in which initialization code is added @@ -633,6 +634,7 @@ codet initialize_nondet_string_struct( static bool add_nondet_string_pointer_initialization( const exprt &expr, const std::size_t &max_nondet_string_length, + bool printable, symbol_tablet &symbol_table, const source_locationt &loc, code_blockt &code) @@ -652,7 +654,8 @@ static bool add_nondet_string_pointer_initialization( dereference_exprt(expr, struct_type), max_nondet_string_length, loc, - symbol_table)); + symbol_table, + printable)); return false; } @@ -792,6 +795,7 @@ void java_object_factoryt::gen_nondet_pointer_init( add_nondet_string_pointer_initialization( expr, object_factory_parameters.max_nondet_string_length, + object_factory_parameters.string_printable, symbol_table, loc, assignments); diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index a64fcb78796..c6aeac7d3d3 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -157,6 +157,6 @@ codet initialize_nondet_string_struct( const std::size_t &max_nondet_string_length, const source_locationt &loc, symbol_tablet &symbol_table, - bool printable = false); + bool printable); #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 1225263b824..3d2dc659b3c 100644 --- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -49,7 +49,7 @@ SCENARIO( WHEN("Initialisation code for a string is generated") { const codet code = - initialize_nondet_string_struct(expr, 20, loc, symbol_table); + initialize_nondet_string_struct(expr, 20, loc, symbol_table, false); THEN("Code is produced") { From e65e340b8a8db07cfa640e8d3542f3d3063d493c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 14:32:40 +0100 Subject: [PATCH 07/10] Use command line option for string-printable param --- src/java_bytecode/java_bytecode_language.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index a4b15d8b963..e99f9fe0b73 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -51,6 +51,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) if(cmd.isset("string-max-input-length")) object_factory_parameters.max_nondet_string_length= std::stoi(cmd.get_value("string-max-input-length")); + object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); if(cmd.isset("lazy-methods-context-sensitive")) From 542a26dd60b8fe95d69f59b3b57c6340064976a4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 15:09:58 +0100 Subject: [PATCH 08/10] Stop adding printable constraints on all strings We no longer do that on all strings in the solver. This is now done during bytecode conversion for Java, and only for input strings. --- src/solvers/refinement/string_constraint_generator_main.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index cbc6545ff9b..17edf927a2f 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -324,9 +324,6 @@ void string_constraint_generatort::add_default_axioms( if(max_string_length!=std::numeric_limits::max()) axioms.push_back(s.axiom_for_length_le(max_string_length)); - - if(force_printable_characters) - add_constraint_on_characters(s, index_zero, s.length(), " -~"); } /// Add constraint on characters of a string. From b0de0e361a13673a76d4175df107d00bc86c2551 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 15:12:05 +0100 Subject: [PATCH 09/10] Test for string printable option on input strings This checks that the string-printable option only applies to input strings. This also adds a test to make sure no printable characters can be present when the option is activated. --- .../java_string_printable/Test.class | Bin 0 -> 921 bytes .../java_string_printable/Test.java | 21 ++++++++++++++++++ .../java_string_printable/test.desc | 8 +++++++ .../java_string_printable/test_char.desc | 7 ++++++ 4 files changed, 36 insertions(+) create mode 100644 regression/strings-smoke-tests/java_string_printable/Test.class create mode 100644 regression/strings-smoke-tests/java_string_printable/Test.java create mode 100644 regression/strings-smoke-tests/java_string_printable/test.desc create mode 100644 regression/strings-smoke-tests/java_string_printable/test_char.desc diff --git a/regression/strings-smoke-tests/java_string_printable/Test.class b/regression/strings-smoke-tests/java_string_printable/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..67670375b050345c8cc5c292229c80ef30cfc693 GIT binary patch literal 921 zcmZvaO-~b16o%j1PCM;%NKd%Y@1t-(K7A3hOO0_yw1S382l@SX*jD4 z-dz3>gH&$SIYXpknEYY;S&dtp;xL0x-{JZ$!(6V?&|YfAreJ+$x&cMZ=QNms;#!A^ZSNy5ZvUpvmnG(L=mHQ zvnK~9ACC6|(Mf8r;wlmf5^ivSi$CP|SXJY8gETu9O~g^Q=Uuc%BEEERsi=RGW>J5X*6|EJDJ0Q?l|dzXh=lDPYhI|Fhip)k}IJ<0-wK&B=fGZF5>iq mVSK=;= ' ' && c <= '~')); + assert(b); + return b; + } +} diff --git a/regression/strings-smoke-tests/java_string_printable/test.desc b/regression/strings-smoke-tests/java_string_printable/test.desc new file mode 100644 index 00000000000..9a91eb68f6e --- /dev/null +++ b/regression/strings-smoke-tests/java_string_printable/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --function Test.check --string-max-length 100 --string-printable --java-assume-inputs-non-null +^EXIT=10$ +^SIGNAL=0$ +assertion.* file Test.java line 6 .* SUCCESS +assertion.* file Test.java line 8 .* FAILURE +-- diff --git a/regression/strings-smoke-tests/java_string_printable/test_char.desc b/regression/strings-smoke-tests/java_string_printable/test_char.desc new file mode 100644 index 00000000000..af03ad6fbbe --- /dev/null +++ b/regression/strings-smoke-tests/java_string_printable/test_char.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --function Test.check_char --string-max-length 100 --string-printable +^EXIT=0$ +^SIGNAL=0$ +assertion.* file Test.java line 18 .* SUCCESS +-- From d2c375202f8563b67b7e592e78b213f85d30f2b4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 24 Oct 2017 15:15:54 +0100 Subject: [PATCH 10/10] Remove string_printable option from the solver This is now done by Java object factory on inputs and others nondet strings. To add the constraint in other cases, this can be done using the string_constrain_characters primitive. --- src/cbmc/cbmc_solvers.cpp | 1 - src/solvers/refinement/string_constraint_generator.h | 3 --- src/solvers/refinement/string_constraint_generator_main.cpp | 1 - 3 files changed, 5 deletions(-) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index d98b8b3dcca..d9c245b5b7a 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -180,7 +180,6 @@ std::unique_ptr cbmc_solverst::get_string_refinement() 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"); - info.string_printable=options.get_bool_option("string-printable"); if(options.get_bool_option("max-node-refinement")) info.max_node_refinement= options.get_unsigned_int_option("max-node-refinement"); diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index eb4d5aee9a6..41e97131662 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -42,8 +42,6 @@ class string_constraint_generatort final { /// Max length of non-deterministic strings size_t string_max_length=std::numeric_limits::max(); - /// Prefer printable characters in non-deterministic strings - bool string_printable=false; }; string_constraint_generatort(const infot& info, const namespacet& ns); @@ -347,7 +345,6 @@ class string_constraint_generatort final std::set created_strings; unsigned symbol_count=0; const messaget message; - const bool force_printable_characters; std::vector axioms; std::vector boolean_symbols; diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 17edf927a2f..730e0877a2b 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -31,7 +31,6 @@ string_constraint_generatort::string_constraint_generatort( const string_constraint_generatort::infot &info, const namespacet &ns) : max_string_length(info.string_max_length), - force_printable_characters(info.string_printable), ns(ns) { }