-
Notifications
You must be signed in to change notification settings - Fork 274
Refactor string refinement constructors #1300
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
romainbrenguier
merged 32 commits into
diffblue:develop
from
LAJW:refactor/string-refinement-constructors
Aug 31, 2017
Merged
Changes from 1 commit
Commits
Show all changes
32 commits
Select commit
Hold shift + click to select a range
22b4885
Remove usage of static in the header file
848f2a5
Constraint gen cosmetics
3217fe3
constraint_generator message is a member
c51e35e
Use C++11 initialization for constraint generator members
cf950ab
Use vector instead of list for constraint_generator data
8043a0d
Hide index_symbols and boolean_symbols in constraint generator
16a0a34
constraint generator const namespace
51d897a
Better string_refinement constructor Act 1
9146575
Better string_refinement constructor Act II
a00b2db
String refinement - remove unused public methods, fix comments
30fe11b
Better string_constraint_generator constructor
99c815e
Make string_constraint_generatort::fresh_symbol non-static
abe4046
Better bv_refinement constructor
792a70d
Hide bv_refinement members, add override specifier
07f6b39
Remove unnecessary typedef
50173d6
Make some string_constraint_generator methods static
aa85392
Make more generator methods private
5368c8c
Private get_created_strings
a440da7
Group generator's member variables
01c6767
Rename axioms to m_axioms
e5c45a5
Prefix all generator member variables with "m_"
1282d03
Update unit tests with new constructors
4087187
Don't pass language_uit::uit as a pointer
83a29dc
Fix linter errors
107704a
Fix is_in_conflict with conflict override
fd59d47
Preprocess constexpr
acaad4f
Remove dead bv_refinementt::set_to
04fae6d
Correct comment
7fd2bfa
Use_counter_example assignable via constructor
22d699c
Move constexpr ifdef into a util header
8da7c30
Constraint generator doxygen
0838f61
Fix function declaration slicing
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -26,14 +26,14 @@ Author: Romain Brenguier, [email protected] | |
#include <util/refined_string_type.h> | ||
#include <solvers/refinement/string_constraint.h> | ||
|
||
class string_constraint_generatort: messaget | ||
class string_constraint_generatort final: messaget | ||
{ | ||
public: | ||
// This module keeps a list of axioms. It has methods which generate | ||
// string constraints for different string functions and add them | ||
// to the axiom list. | ||
|
||
string_constraint_generatort(namespacet _ns): | ||
explicit string_constraint_generatort(namespacet _ns): | ||
max_string_length(std::numeric_limits<size_t>::max()), | ||
force_printable_characters(false), | ||
ns(_ns) | ||
|
@@ -91,21 +91,19 @@ class string_constraint_generatort: messaget | |
exprt add_axioms_for_function_application( | ||
const function_application_exprt &expr); | ||
|
||
static constant_exprt constant_char(int i, const typet &char_type); | ||
|
||
|
||
// Used by format function | ||
class format_specifiert; | ||
|
||
private: | ||
static constant_exprt constant_char(int i, const typet &char_type); | ||
// The integer with the longest string is Integer.MIN_VALUE which is -2^31, | ||
// that is -2147483648 so takes 11 characters to write. | ||
// The long with the longest string is Long.MIN_VALUE which is -2^63, | ||
// approximately -9.223372037*10^18 so takes 20 characters to write. | ||
const std::size_t MAX_INTEGER_LENGTH=11; | ||
const std::size_t MAX_LONG_LENGTH=20; | ||
const std::size_t MAX_FLOAT_LENGTH=15; | ||
const std::size_t MAX_DOUBLE_LENGTH=30; | ||
constexpr static const std::size_t MAX_INTEGER_LENGTH=11; | ||
constexpr static const std::size_t MAX_LONG_LENGTH=20; | ||
constexpr static const std::size_t MAX_FLOAT_LENGTH=15; | ||
constexpr static const std::size_t MAX_DOUBLE_LENGTH=30; | ||
|
||
std::map<function_application_exprt, exprt> function_application_cache; | ||
namespacet ns; | ||
|
@@ -346,7 +344,6 @@ class string_constraint_generatort: messaget | |
return args; | ||
} | ||
|
||
private: | ||
// Helper functions | ||
exprt int_of_hex_char(const exprt &chr) const; | ||
exprt is_high_surrogate(const exprt &chr) const; | ||
|
@@ -363,13 +360,16 @@ exprt is_digit_with_radix( | |
const bool strict_formatting, | ||
const exprt &radix_as_char, | ||
const unsigned long radix_ul); | ||
|
||
exprt get_numeric_value_from_character( | ||
const exprt &chr, | ||
const typet &char_type, | ||
const typet &type, | ||
const bool strict_formatting, | ||
unsigned long radix_ul); | ||
|
||
size_t max_printed_string_length(const typet &type, unsigned long ul_radix); | ||
|
||
std::string utf16_constant_array_to_java( | ||
const array_exprt &arr, unsigned length); | ||
|
||
|
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
constexpr
redundant withconst
?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
auto val = WITH_CONST_VAL
is of typeconst size_t
andauto val = WITHOUT_CONST_VAL
is of typesize_t
. VS 2013 doesn't support constexpr so static const is the next best thing after macro.