Skip to content

Fix mode of java if_exprt not being set #2140

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed

Fix mode of java if_exprt not being set #2140

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
181b397
Set mode when creating if_exprt
romainbrenguier May 1, 2018
b754139
Add precondition ensuring mode is not empty
romainbrenguier May 1, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/goto-programs/goto_convert.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2070,6 +2070,7 @@ symbolt &goto_convertt::new_tmp_symbol(
const source_locationt &source_location,
const irep_idt &mode)
{
PRECONDITION(!mode.empty());
symbolt &new_symbol = get_fresh_aux_symbol(
type,
tmp_symbol_prefix,
Expand Down
19 changes: 13 additions & 6 deletions src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -952,6 +952,14 @@ static unsigned get_bytecode_type_width(const typet &ty)
return ty.get_unsigned_int(ID_width);
}

/// Create an if-expression with mode set to Java
static if_exprt java_if_expr(const exprt &cond, const exprt &t, const exprt &f)
{
auto result = if_exprt(cond, t, f);
result.set(ID_mode, ID_java);
return result;
}

codet java_bytecode_convert_methodt::convert_instructions(
const methodt &method,
const code_typet &method_type,
Expand Down Expand Up @@ -1893,13 +1901,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
exprt one=from_integer(1, t);
exprt minus_one=from_integer(-1, t);

if_exprt greater=if_exprt(
auto greater = java_if_expr(
binary_relation_exprt(op[0], ID_gt, op[1]),
one,
minus_one);

results[0]=
if_exprt(
results[0] = java_if_expr(
binary_relation_exprt(op[0], ID_equal, op[1]),
from_integer(0, t),
greater);
Expand All @@ -1921,13 +1928,13 @@ codet java_bytecode_convert_methodt::convert_instructions(
exprt one=from_integer(1, result_type);
exprt minus_one=from_integer(-1, result_type);
results[0]=
if_exprt(
java_if_expr(
or_exprt(nan_op0, nan_op1),
nan_result,
if_exprt(
java_if_expr(
ieee_float_equal_exprt(op[0], op[1]),
from_integer(0, result_type),
if_exprt(
java_if_expr(
binary_relation_exprt(op[0], ID_lt, op[1]),
minus_one,
one)));
Expand Down