File tree 4 files changed +9
-19
lines changed 4 files changed +9
-19
lines changed Original file line number Diff line number Diff line change @@ -40,14 +40,14 @@ class string_constraint_generatort final
40
40
// / Arguments pack for the string_constraint_generator constructor
41
41
struct infot
42
42
{
43
- const namespacet *ns=nullptr ;
44
43
// / Max length of non-deterministic strings
45
44
size_t string_max_length=std::numeric_limits<size_t >::max();
46
45
// / Prefer printable characters in non-deterministic strings
47
46
bool string_printable=false ;
48
47
};
49
48
50
- explicit string_constraint_generatort (const infot& info);
49
+ explicit string_constraint_generatort (
50
+ const infot& info, const namespacet& ns);
51
51
52
52
// / Axioms are of three kinds: universally quantified string constraint,
53
53
// / not contains string constraints and simple formulas.
Original file line number Diff line number Diff line change 28
28
#include < util/ssa_expr.h>
29
29
30
30
string_constraint_generatort::string_constraint_generatort (
31
- const string_constraint_generatort::infot& info):
31
+ const string_constraint_generatort::infot& info, const namespacet& ns ):
32
32
max_string_length(info.string_max_length),
33
33
m_force_printable_characters(info.string_printable),
34
- m_ns(*info. ns) { }
34
+ m_ns(ns) { }
35
35
36
36
const std::vector<exprt> &string_constraint_generatort::get_axioms () const
37
37
{
Original file line number Diff line number Diff line change @@ -86,21 +86,11 @@ static bool validate(const string_refinementt::infot &info)
86
86
return true ;
87
87
}
88
88
89
- static string_constraint_generatort::infot
90
- generator_info (const string_refinementt::infot &in)
91
- {
92
- string_constraint_generatort::infot out;
93
- out.ns =in.ns ;
94
- out.string_max_length =in.string_max_length ;
95
- out.string_printable =in.string_printable ;
96
- return out;
97
- }
98
-
99
89
string_refinementt::string_refinementt (const infot &info, bool ):
100
90
supert(info),
101
91
config_(info),
102
92
loop_bound_(info.refinement_bound),
103
- generator(generator_info( info) ) { }
93
+ generator(info, *info.ns ) { }
104
94
105
95
string_refinementt::string_refinementt (const infot &info):
106
96
string_refinementt(info, validate(info)) { }
Original file line number Diff line number Diff line change @@ -34,18 +34,18 @@ class string_refinementt final: public bv_refinementt
34
34
private:
35
35
struct configt {
36
36
unsigned refinement_bound=0 ;
37
- size_t string_max_length=std::numeric_limits<size_t >::max();
38
37
// / Make non-deterministic character arrays have at least one character
39
38
bool string_non_empty=false ;
40
39
// / Concretize strings after solver is finished
41
40
bool trace=false ;
42
- // / Make non-deterministic characters printable
43
- bool string_printable=false ;
44
41
bool use_counter_example=false ;
45
42
};
46
43
public:
47
44
// / string_refinementt constructor arguments
48
- struct infot :public bv_refinementt ::infot, public configt { };
45
+ struct infot :
46
+ public bv_refinementt::infot,
47
+ public string_constraint_generatort::infot,
48
+ public configt { };
49
49
50
50
explicit string_refinementt (const infot &);
51
51
You can’t perform that action at this time.
0 commit comments