Skip to content

Commit a04dc21

Browse files
romainbrenguierJoel Allred
authored and
Joel Allred
committed
Many corrections in preprocessing of strings
Better signatures and string detection Better detection of string-like types and handling of char arrays Changing the way we deal with string initialisation from array Factorized part of type recognition and added StringBuilder and CharSequence to the list of java classes that should be considered as string. Changed the way we deal with StringBuilders: instead of having a map we add an assignment to the instructions. We also detect char arrays and handle them better. We now use substring and copy functions for initialisation from char array since the argument are always transformed into refined strings. For each string returned by a string function we also add into the java_string_to_cprover_string map a string_exprt. Corrected detection of typecast in make_cprover_string_assign Ensuring refined_string arguments of function applications are string_exprt Correct string_refine_preprocesst constructor. Order of initialisation is now the same as the order of declaration. This was picked up by g++ and clang. Added signatures for some StringBuilder functions. Removed map java_to_cprover_string and adapt signature for side effects. The usage of a map is not correct since strings can be modified by side effects. Signature is necessary for StringBuilders to be assigned in the right way with methods with side effects. Assign all string_exprt to refined string symbols in preprocessing. This makes it then easier to debug and to find witnesses for counter examples in the solver. Make signatures take priority over actual type and add signature for intern. Linting corrections Adding malloc for char arrays for String.toCharArray Fixing preprocessing of string function with side effect This fixes problems we were getting with some StringBuilder functions. The return value should contain a pointer to the original StringBuilder and the fields of the StringBuilder should be filled with the result of the function call. Corrected mistake in preprocessing of string functions with side effects char array assignements returns a string_exprt This is to be uniform with other preprocessing functions also returning string_exprt Preprocessing for StringBuilder.append on char array Corrected update of signature and commented out some unused code Corrected the initialization from char array We cannot use the substring function because the meaning of the third argument is different between `String.<init>([CII)` and `String.substring(SII)` Using new id for conversion between char pointer and array Cleaning of preprocessing for strings Removed useless functions and merged some maps Make a copy of the function call to be modified Removed redeclaration of location
1 parent c9ff379 commit a04dc21

File tree

2 files changed

+416
-452
lines changed

2 files changed

+416
-452
lines changed

0 commit comments

Comments
 (0)