- Member eval_format_specifier (const format_specifiert &fs, const std::vector< mp_integer > &arg)
- Conversion of hexadecimal float is not implemented.
- Member string_constraint_generatort::add_axioms_for_substring (const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
- Should return code different from 0 if ‘start’ != start
or
end' != end`
- Member string_constraint_generatort::add_axioms_for_delete (const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
- Should use add_axioms_for_concat_substr instead of add_axioms_for_concat
- Member string_constraint_generatort::add_axioms_for_parse_int (const function_application_exprt &f)
- We should throw an exception when constraints added in add_axioms_for_correct_number_format do not hold.
- Member add_node (string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, symbol_generatort &fresh_symbol)
- there should be a class with just the three functions we require here
- Member add_axioms_for_format_specifier (string_constraint_generatort &generator, const format_specifiert &fs, const array_string_exprt &string_arg, const typet &index_type, const typet &char_type, const messaget &message)
Conversion of octal is not implemented.
Conversion for format specifier general is not implemented.
Conversion of hexadecimal float is not implemented.
Conversion of date-time is not implemented
- Member eval_format_specifier (const format_specifiert &fs, const std::vector< mp_integer > &arg)
Conversion of octal is not implemented.
Conversion for format specifier general is not implemented.
- Member string_constraint_generatort::add_axioms_for_substring (const function_application_exprt &f)
- Should return a integer different from zero when the string is shorter tan the end index.
- Member eval_format_specifier (const format_specifiert &fs, const std::vector< mp_integer > &arg)
- Conversion of date-time is not implemented
- Member length_for_format_specifier (const format_specifiert &fs, const array_string_exprt &arg, const typet &index_type, array_poolt &array_pool)
Conversion of octal is not implemented.
Conversion for format specifier general is not implemented.
Conversion of hexadecimal float is not implemented.
Conversion of date-time is not implemented
- Member is_linear_arithmetic_expr
- Add unit tests
- Member initialize_nondet_string_fields (struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable, allocate_objectst &allocate_objects)
- Refactor with make_nondet_string_expr
- Member get_tag (const typet &type)
- Use follow instead of assuming tag to symbol relationship.
- Member java_string_library_preprocesst::make_nondet_string_expr (const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
- refactor with initialize_nonddet_string_struct
- Member get_exponent (const exprt &src, const ieee_float_spect &spec)
- Refactor with float_bv.cpp float_utils.h
- Class string_constraintt
- The fact that we follow this grammar is not enforced at the moment.
- Member string_constraint_generatort::add_axioms_for_string_of_float (const function_application_exprt &f)
- The specifications of these functions is only partial.
- Member string_constraint_generatort::add_axioms_from_double (const function_application_exprt &f)
- The specifications is only partial.
- Member string_constraint_generatort::add_axioms_for_substring (const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
- The specification may not be correct for the case where the string is shorter than end.
- Member string_constraint_generatort::add_axioms_for_code_point_count (const function_application_exprt &f)
- This function is underspecified, we do not compute the exact value but over approximate it.
- Member string_constraint_generatort::add_axioms_for_offset_by_code_point (const function_application_exprt &f)
- This function is underspecified, it should return the index within this String that is offset from the given first argument by second argument code points and we approximate this by saying the result is between index + offset and index + 2 * offset.
- Member character_equals_ignore_case (const exprt &char1, const exprt &char2, const exprt &char_a, const exprt &char_A, const exprt &char_Z)
- The extra constant character arguments are not needed.
- Member string_constraint_generatort::add_axioms_for_constant (const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
- We should have a special treatment for java strings when the conversion function is available:
- Member string_constraint_generatort::add_axioms_from_literal (const function_application_exprt &f)
- The name of the function should be changed to reflect what it does.
- Class class_hierarchyt
- Implement missing functions from
class_hierarchyt
in class_hierarchy_grapht
so that class_hierarchyt
can be fully replaced.
- Member string_constraint_generatort::add_axioms_for_string_of_float (const array_string_exprt &res, const exprt &f)
- This specification is not correct for negative numbers and double precision.
- Member string_constraint_generatort::add_axioms_from_float_scientific_notation (const array_string_exprt &res, const exprt &f)
- For now we only consider single precision.
- Member string_constraint_generatort::add_axioms_for_index_of (const array_string_exprt &str, const exprt &c, const exprt &from_index)
- Make argument names match whose of add_axioms_for_index_of_string
- Member string_constraint_generatort::add_axioms_for_last_index_of (const array_string_exprt &str, const exprt &c, const exprt &from_index)
- Change argument names to match add_axioms_for_last_index_of_string
- Member string_constraint_generatort::associate_array_to_pointer (const exprt &return_code, const function_application_exprt &f)
- : we allow expression of the form of
arr[0]
instead of arr
as the array argument but this could go away.
- Member string_constraint_generatort::add_axioms_for_is_prefix (const function_application_exprt &f, bool swap_arguments)
The primitive should be renamed to starts_with
.
Get rid of the boolean flag.
- Member string_constraint_generatort::add_axioms_for_is_suffix (const function_application_exprt &f, bool swap_arguments)
- The primitive should be renamed
ends_with
.
- Member string_constraint_generatort::add_axioms_for_set_length (const function_application_exprt &f)
- We can reduce the number of constraints by merging 2 and 3.