Pzucker/gdb #70
Pzucker/gdb #70
Conversation
wp/lib/bap_wp/src/postprocess.ml
Outdated
| @@ -0,0 +1,133 @@ | |||
| (***************************************************************************) | |||
There was a problem hiding this comment.
Not crazy about the name for this module. Maybe "output.ml"?
There was a problem hiding this comment.
Or even "output_gdb.ml", I'm not actually sure how good an idea it is to reuse this module for other things.
There was a problem hiding this comment.
I did also move the print_result function over into here. If I'm going to name it output_gdb.ml I should move that back. output.ml is perfectly acceptable
wp/lib/bap_wp/src/postprocess.ml
Outdated
| List.map ~f:strip_final_digits | ||
|
|
||
|
|
||
| (** [output_gdb] is similar to [print_result] except chews on the model and outputs a gdb script with a |
There was a problem hiding this comment.
This comment should probably be right before output_gdb.
wp/lib/bap_wp/src/postprocess.mli
Outdated
| val print_result : Z3.Solver.solver -> Z3.Solver.status -> Constr.t -> Z3.context -> unit | ||
|
|
||
|
|
||
| (** Prints to file a gdb script that will fill the appropriate registers with the countermodel *) |
There was a problem hiding this comment.
This should be more detailed! E.g. the BAP mlis have whole paragraphs explaining the input-output of their functions. We don't need to be quite as detailed, but still. Also: why have a Z3.context when there's one in the Env.t. Are they the same one? What is that first string argument?
wp/lib/bap_wp/src/postprocess.ml
Outdated
|
|
||
| type sign = Unsigned | Signed | ||
|
|
||
| let string_of_sign s = |
There was a problem hiding this comment.
Can you annotate the types for the inputs and output for the functions in this module?
There was a problem hiding this comment.
I should trash a lot of these anyway. They aren't used.
There was a problem hiding this comment.
My statement was false. They are used.
|
Oops, looks like this needs a rebase as well to fix merge conflicts. |
|
Why does it need a rebase? |
…cess module to output.ml
…cess module to output.ml
Added functionality and gdb-filename argument to output a gdb file that will breakpoint at the examined function and fill registers with the counter model.
Added documentation in wp-readme
No test as of yet. Not exactly sure how to unit test this.