Factor nondet choices in object factory #863
Conversation
This splits the nondet-if-then-else concept into a utility. It only has one user here, but downstream branches already have several users. This reduces the diff between branches for easier future merges.
| init_code.move_to_operands(set_null_label); | ||
| init_code.move_to_operands(init_done_label); | ||
| } | ||
| init_null_diamond.finish(); |
There was a problem hiding this comment.
I believe this is mis-indented.
There was a problem hiding this comment.
Looks it in the diff but isn't
|
|
||
| \*******************************************************************/ | ||
|
|
||
| inline exprt get_nondet_bool(const typet &type) |
There was a problem hiding this comment.
I'd suggest expr_util.{h,cpp} would be a good enough place to hold this one instead of creating a header-only module.
| #include <util/symbol_table.h> | ||
| #include <util/source_location.h> | ||
|
|
||
| // This will be unified with other similar fresh-symbol routines shortly |
There was a problem hiding this comment.
When is that point in time?
| Outputs: | ||
|
|
||
| Purpose: Emits instructions and defines labels for the beginning of | ||
| a nondeterministic if-else diamond. Code is emitted to the |
There was a problem hiding this comment.
It may be worth reading #767 front to back. Quoting the my key comment:
"It seems the code here really mixes up two concepts [...]: the code is being generated as if in the GOTO intermediate level, but it's being done using high-level language constructs. There does not seem to be any need for labels or gotos here. Just generate a code_ifthenelse with a then_case and an else_case. This avoids the static variable and synthetic labels, and will thus make the code much more concise."
There was a problem hiding this comment.
Ah, true. I wrote this a long time ago when I thought that was how things were supposed to work here (since the Java frontend never generates high-level constructs, because bytecode). I'll take another look at this tomorrow.
|
@owen-jones-diffblue @tautschnig OK, I think however I still will want the splitting out of |
This splits the nondet-if-then-else concept into a utility. It only has one user here, but downstream branches already have several users. This reduces the diff between branches for easier future merges.