String solver cbmc pass option#278
String solver cbmc pass option#278romainbrenguier wants to merge 299 commits intodiffblue:masterfrom
Conversation
Cleanup: Name should precede literals in output
Use -DANSI_C_DEBUG to enable.
Moved context-free logic from scanner into the grammar and fixed bugs to permit 1) attributes on labels and 2) multiple attributes after pointer-type declarations.
Handle placement of symbols into specified sections by prefixing symbol names with <section-name>$$.
Full path are useful to track the exact location of the file when working with the output afterwards. Usage of file and directory concatenation is simplified.
…tion of the c tests accordingly
src/cbmc/cbmc_parse_options.cpp
Outdated
| " --yices use Yices\n" | ||
| " --z3 use Z3\n" | ||
| " --refine use refinement procedure (experimental)\n" | ||
| " --pass use pass procedure (experimental)\n" |
There was a problem hiding this comment.
So ... what is the pass procedure? Would be nice to be user-friendly in the --help output.
src/cbmc/cbmc_solvers.h
Outdated
| else if(options.get_bool_option("refine")) | ||
| solver = get_bv_refinement(); | ||
| else if(options.get_bool_option("pass")) { | ||
| std::cout << "PASS solver" << std::endl; |
There was a problem hiding this comment.
Use a proper message_streamt API
| virtual std::unique_ptr<solvert> get_solver() | ||
| { | ||
| solvert *solver; | ||
|
|
There was a problem hiding this comment.
Why remove whitespace?
|
|
||
| string_refinementt *string_refinement = new string_refinementt(ns, *prop); | ||
| string_refinement->set_ui(ui); | ||
| return new cbmc_solver_with_propt(string_refinement, prop); |
There was a problem hiding this comment.
That's two objects allocated on the heap and never freed?
There was a problem hiding this comment.
prop is deleted by ~cbmc_solver_with_propt and string_refinement by cbmc_solverst's destructor which cbmc_solver_with_propt inherits.
|
|
||
| if(cmdline.isset("pass")) | ||
| { | ||
| options.set_option("pass", true); |
There was a problem hiding this comment.
How about options.set_option("pass", cmdline.isset("pass")); ?
src/cbmc/cbmc_parse_options.cpp
Outdated
| goto_partial_inline(goto_functions, ns, ui_message_handler); | ||
|
|
||
|
|
||
| if(cmdline.isset("pass")) { |
There was a problem hiding this comment.
By the looks of it: is options.set_option("pass", ...) even required?
There was a problem hiding this comment.
It is used in cbmc_parse_options.h
|
this is made obsolete by the more recent pull request #341 |
…nchmark New end to end benchmark
…ert-revert-2490 Revert "REVERT PR diffblue#2490 switch-range commit"
Adding a PASS option for calling the string solver and changing the Makefile for this string solver