loop-to-recursion transformation #11
Conversation
There was a problem hiding this comment.
Good start!
Please add regression tests to test your implementation. Have a look in https://github.com/peterschrammel/cbmc/tree/master/regression/goto-instrument how to do that.
You can just push new commits to your branch. They'll automatically appear in this Pull Request.
| Forall_goto_program_instructions(it, goto_function_body) | ||
|
|
||
| { | ||
| if(!it->is_backwards_goto() && |
There was a problem hiding this comment.
Lines 41-43 seem unnecessary.
|
|
||
| //search for loop | ||
| Forall_goto_program_instructions(it, goto_function_body) | ||
|
|
There was a problem hiding this comment.
style: remove blank line (several occurrences)
| bool has_loop ( | ||
| goto_programt &goto_function_body) | ||
| { | ||
|
|
| #include <goto-programs/remove_skip.h> | ||
|
|
||
|
|
||
| #include "loop_to_recursion.h" |
|
|
||
| if(it->is_backwards_goto()) | ||
| found = true; | ||
| break; |
There was a problem hiding this comment.
Returning directly from here seems easier. Lines 49-54 (except 51) can go away...
| goto_functionst &goto_functions, | ||
| symbol_tablet &symbol_table, | ||
| messaget message) | ||
| { |
There was a problem hiding this comment.
Style: don't indent braces, but only block inside braces (multiple occurrences)
|
|
||
| //add REC_function symbol | ||
| symbolt recursive_function; | ||
| const irep_idt rec_f_name = "REC_function"; |
There was a problem hiding this comment.
When you have multiple loops, you'll need call them differently.
| goto_functions.function_map.find("REC_function"); | ||
|
|
||
| //not added? | ||
| if(rec_func_id==goto_functions.function_map.end()) |
There was a problem hiding this comment.
You'll need a different function for each loop.
| if(!goto_function.body_available()) | ||
| continue; | ||
|
|
||
| if(has_loop(goto_function.body)) |
There was a problem hiding this comment.
In the end you should replace all the loops in all the functions by its own corresponding recursive function.
|
|
||
| symbolt &rec_f = symbol_table.lookup("REC_function"); | ||
|
|
||
| /*before adding replacing loop by REC_function call, |
There was a problem hiding this comment.
Style: Use
// comments
// even if they are over
// multiple lines
…le. 3. Considering more than one loop in a function. 4. Adding a regression test.
Allows to detect errors related to synchronization on null references, for example.
Allows to detect errors related to synchronization on null references, for example. Fixes diffblue#1236.
Allows to detect errors related to synchronization on null references, for example. Fixes diffblue#1236.
Allows to detect errors related to synchronization on null references, for example. Fixes diffblue#1236.
Allows to detect errors related to synchronization on null references on Monitor enter. Partially fixes issue 1236.
Allows to detect errors related to synchronization on null references on Monitor enter. Partially fixes issue 1236.
Allows to detect errors related to synchronization on null references on Monitor enter. Partially fixes issue 1236.
…xceptions Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions)
Trying to add a new loop transformation option to eliminate loops in C programs by converting them into recursive function calls.