Skip to content

Commit d2c3752

Browse files
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.
1 parent b0de0e3 commit d2c3752

File tree

3 files changed

+0
-5
lines changed

3 files changed

+0
-5
lines changed

src/cbmc/cbmc_solvers.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,6 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
180180
info.string_max_length=options.get_signed_int_option("string-max-length");
181181
info.string_non_empty=options.get_bool_option("string-non-empty");
182182
info.trace=options.get_bool_option("trace");
183-
info.string_printable=options.get_bool_option("string-printable");
184183
if(options.get_bool_option("max-node-refinement"))
185184
info.max_node_refinement=
186185
options.get_unsigned_int_option("max-node-refinement");

src/solvers/refinement/string_constraint_generator.h

-3
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,6 @@ class string_constraint_generatort final
4242
{
4343
/// Max length of non-deterministic strings
4444
size_t string_max_length=std::numeric_limits<size_t>::max();
45-
/// Prefer printable characters in non-deterministic strings
46-
bool string_printable=false;
4745
};
4846

4947
string_constraint_generatort(const infot& info, const namespacet& ns);
@@ -347,7 +345,6 @@ class string_constraint_generatort final
347345
std::set<array_string_exprt> created_strings;
348346
unsigned symbol_count=0;
349347
const messaget message;
350-
const bool force_printable_characters;
351348

352349
std::vector<exprt> axioms;
353350
std::vector<symbol_exprt> boolean_symbols;

src/solvers/refinement/string_constraint_generator_main.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,6 @@ string_constraint_generatort::string_constraint_generatort(
3131
const string_constraint_generatort::infot &info,
3232
const namespacet &ns)
3333
: max_string_length(info.string_max_length),
34-
force_printable_characters(info.string_printable),
3534
ns(ns)
3635
{
3736
}

0 commit comments

Comments
 (0)