Skip to content

Improvements in string preprocessing to facilitate constant propagation #984

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.

Sign up for GitHub

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

Closed
romainbrenguier wants to merge 18 commits into from
Closed

Improvements in string preprocessing to facilitate constant propagation #984

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
972ffda
Declaring auxiliary function for allocation of dynamic objects
romainbrenguier Apr 24, 2017
d7d12ee
Replacement of string preprocessing for Java
romainbrenguier Apr 24, 2017
353d7d0
Merging string and character preprocess as one argument of bytecode c…
romainbrenguier Apr 20, 2017
21d89b3
Removing and deactivating the old preprocessing
romainbrenguier Apr 21, 2017
b7b8a4d
Avoid copies of string preprocess objects
romainbrenguier May 31, 2017
b9e0491
Change the step at which we replace String methods code
romainbrenguier Jun 1, 2017
9ff5c77
Removing string conversion from method conversion
romainbrenguier Jun 1, 2017
dd4520a
Overwrite String type
May 24, 2017
0fd8afa
Specification for contains in the case of a constant argument diffblu…
romainbrenguier Apr 7, 2017
a85cfff
Make index_of precise diffblue/test-gen#77
romainbrenguier May 26, 2017
5cefca6
Making lastIndexOf precise diffblue/test-gen#77
romainbrenguier May 31, 2017
c8bdb11
Updating comments for index_of and last_index_of on characters
romainbrenguier May 31, 2017
02279c0
Optimize last_index_of for constant argument
romainbrenguier May 31, 2017
c297f03
[constraint-main] Adding existing string expr to created_strings so t…
romainbrenguier May 18, 2017
82e1c74
[preprocess] Improving constructor and copy of strings
romainbrenguier May 26, 2017
7682fe5
[preprocess] Adding CharSequence.length method
romainbrenguier May 30, 2017
4c624f7
[preprocess] More direct conversion of length methods
romainbrenguier May 30, 2017
4c425e0
[constraint-concat] Adding a add_axioms_for_concat_substr function
romainbrenguier May 30, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 0 additions & 9 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
#include <ansi-c/c_preprocess.h>

#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/string_refine_preprocess.h>
#include <goto-programs/remove_function_pointers.h>
#include <goto-programs/remove_virtual_functions.h>
#include <goto-programs/remove_instanceof.h>
Expand Down Expand Up @@ -905,14 +904,6 @@ bool cbmc_parse_optionst::process_goto_program(
status() << "Partial Inlining" << eom;
goto_partial_inline(goto_functions, ns, ui_message_handler);


if(cmdline.isset("refine-strings"))
{
status() << "Preprocessing for string refinement" << eom;
string_refine_preprocesst(
symbol_table, goto_functions, ui_message_handler);
}

// remove returns, gcc vectors, complex
remove_returns(symbol_table, goto_functions);
remove_vector(symbol_table, goto_functions);
Expand Down
1 change: 0 additions & 1 deletion src/goto-programs/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,6 @@ SRC = basic_blocks.cpp \
slice_global_inits.cpp \
string_abstraction.cpp \
string_instrumentation.cpp \
string_refine_preprocess.cpp \
system_library_symbols.cpp \
vcd_goto_trace.cpp \
wp.cpp \
Expand Down
Loading