From 181b39778ec904e2f0352811a69539bfb3e53bf0 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 1 May 2018 11:02:58 +0100 Subject: [PATCH 1/2] Set mode when creating if_exprt goto_convert may create temporary symbols for if-expression, these symbols need to have a mode set, so setting them at the creation of the if_exprt ensures the mode is correct. --- .../java_bytecode_convert_method.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 9b221d4298c..8a0b369c55e 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -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, @@ -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); @@ -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))); From b7541393815763e5bd418bae38c0c1b76109b799 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 1 May 2018 11:04:41 +0100 Subject: [PATCH 2/2] Add precondition ensuring mode is not empty This ensures goto_convert does not create symbols with empty mode, which could create issues in the later steps of cbmc analysis. --- src/goto-programs/goto_convert.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index c662c5a4c2f..72da12547af 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -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,