String solver cbmc pass option #278
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
| @@ -1175,6 +1187,7 @@ void cbmc_parse_optionst::help() | |||
| " --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.
| if(options.get_bool_option("dimacs")) | ||
| solver = get_dimacs(); | ||
| 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
| @@ -79,11 +79,14 @@ class cbmc_solverst:public messaget | |||
| 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.
| @@ -341,6 +342,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) | |||
| options.set_option("refine-arithmetic", true); | |||
| } | |||
|
|
|||
| 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")); ?
| @@ -911,6 +917,12 @@ bool cbmc_parse_optionst::process_goto_program( | |||
| status() << "Partial Inlining" << eom; | |||
| 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