diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp index 631ed41ada1..cd90096e577 100644 --- a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp @@ -18,14 +18,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + void java_internal_additions(symbol_table_baset &dest) { // add __CPROVER_rounding_mode { symbolt symbol; - symbol.base_name = CPROVER_PREFIX "rounding_mode"; - symbol.name=CPROVER_PREFIX "rounding_mode"; + symbol.name = rounding_mode_identifier(); + symbol.base_name = symbol.name; symbol.type=signed_int_type(); symbol.mode=ID_C; symbol.is_lvalue=true; diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 5e159e0f438..193806c15b6 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -120,7 +121,7 @@ void java_static_lifetime_init( code_blockt code_block; const symbol_exprt rounding_mode = - symbol_table.lookup_ref(CPROVER_PREFIX "rounding_mode").symbol_expr(); + symbol_table.lookup_ref(rounding_mode_identifier()).symbol_expr(); code_block.add( code_assignt{rounding_mode, from_integer(0, rounding_mode.type())}); diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 8223bab00c9..6551cd208f3 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -11,6 +11,8 @@ Author: Peter Schrammel #include "constant_propagator.h" +#include + #ifdef DEBUG #include #include @@ -655,7 +657,7 @@ bool constant_propagator_domaint::partial_evaluate( // if the current rounding mode is top we can // still get a non-top result by trying all rounding // modes and checking if the results are all the same - if(!known_values.is_constant(ID_cprover_rounding_mode_str)) + if(!known_values.is_constant(rounding_mode_identifier())) return partial_evaluate_with_all_rounding_modes(known_values, expr, ns); return replace_constants_and_simplify(known_values, expr, ns); @@ -685,7 +687,7 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( { valuest tmp_values = known_values; tmp_values.set_to( - symbol_exprt(ID_cprover_rounding_mode_str, integer_typet()), + symbol_exprt(rounding_mode_identifier(), integer_typet()), from_integer(rounding_modes[i], integer_typet())); exprt result = expr; if(replace_constants_and_simplify(tmp_values, result, ns)) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index bccc13ab68e..3026d8abafb 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + const char gcc_builtin_headers_types[]= "# 1 \"gcc_builtin_headers_types.h\"\n" #include "gcc_builtin_headers_types.inc" @@ -205,7 +207,8 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "constant_infinity_uint];\n" // float stuff - "int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+ + "int " CPROVER_PREFIX "thread_local " + + id2string(rounding_mode_identifier()) + '='+ std::to_string(config.ansi_c.rounding_mode)+";\n" // pipes, write, read, close diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index b1a376f455d..aa581b155cf 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + std::string c2cpp(const std::string &s) { std::string result; @@ -108,7 +110,7 @@ void cpp_internal_additions(std::ostream &out) // float // TODO: should be thread_local - out << "int " CPROVER_PREFIX "rounding_mode = " + out << "int " << rounding_mode_identifier() << " = " << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n'; // pipes, write, read, close diff --git a/src/cpp/module_dependencies.txt b/src/cpp/module_dependencies.txt index 8bd4b3854cf..4ff08a34b34 100644 --- a/src/cpp/module_dependencies.txt +++ b/src/cpp/module_dependencies.txt @@ -1,5 +1,6 @@ ansi-c cpp +goto-programs langapi # should go away linking util diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 2e36a573506..68a0a2245e4 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include void full_slicert::add_dependencies( @@ -248,7 +249,7 @@ static bool implicit(goto_programt::const_targett target) const symbol_exprt &s=to_symbol_expr(a.lhs()); - return s.get_identifier()==CPROVER_PREFIX "rounding_mode"; + return s.get_identifier() == rounding_mode_identifier(); } void full_slicert::operator()( diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp index 6832e2dc2ec..e4decac0573 100644 --- a/src/goto-programs/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -21,6 +21,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" +irep_idt rounding_mode_identifier() +{ + return CPROVER_PREFIX "rounding_mode"; +} + /// Iterate over an expression and check it or any of its subexpressions are /// floating point operations that haven't been adjusted with a rounding mode /// yet. @@ -186,7 +191,7 @@ void adjust_float_expressions(exprt &expr, const namespacet &ns) return; symbol_exprt rounding_mode = - ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); + ns.lookup(rounding_mode_identifier()).symbol_expr(); rounding_mode.add_source_location() = expr.source_location(); diff --git a/src/goto-programs/adjust_float_expressions.h b/src/goto-programs/adjust_float_expressions.h index 43d9cb6c607..80401edcd0b 100644 --- a/src/goto-programs/adjust_float_expressions.h +++ b/src/goto-programs/adjust_float_expressions.h @@ -56,4 +56,8 @@ void adjust_float_expressions( /// \see adjust_float_expressions(goto_functionst &, const namespacet &) void adjust_float_expressions(goto_modelt &goto_model); +/// Return the identifier of the program symbol used to +/// store the current rounding mode. +irep_idt rounding_mode_identifier(); + #endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 84e973cb867..5cb7d3daaa3 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -16,6 +16,7 @@ Author: Michael Tautschnig, tautschn@amazon.com #include #include +#include #include #include @@ -33,8 +34,8 @@ static void create_initialize(symbol_tablet &symbol_table) namespacet ns(symbol_table); - symbol_exprt rounding_mode= - ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); + symbol_exprt rounding_mode = + ns.lookup(rounding_mode_identifier()).symbol_expr(); code_assignt a(rounding_mode, from_integer(0, rounding_mode.type())); init_code.add(a); diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp index bfcdd101871..636baf018a8 100644 --- a/src/jsil/jsil_internal_additions.cpp +++ b/src/jsil/jsil_internal_additions.cpp @@ -11,6 +11,8 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_internal_additions.h" +#include + #include #include #include @@ -25,8 +27,8 @@ void jsil_internal_additions(symbol_tablet &dest) { symbolt symbol; - symbol.base_name = CPROVER_PREFIX "rounding_mode"; - symbol.name=CPROVER_PREFIX "rounding_mode"; + symbol.name = rounding_mode_identifier(); + symbol.base_name = symbol.name; symbol.type=signed_int_type(); symbol.mode=ID_C; symbol.is_lvalue=true; diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index c5b7c985a61..9a7d69aa509 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening #include "remove_internal_symbols.h" +#include + #include #include #include @@ -119,7 +121,7 @@ void remove_internal_symbols( special.insert(CPROVER_PREFIX "malloc_size"); special.insert(CPROVER_PREFIX "deallocated"); special.insert(CPROVER_PREFIX "dead_object"); - special.insert(CPROVER_PREFIX "rounding_mode"); + special.insert(rounding_mode_identifier()); special.insert("__new"); special.insert("__new_array"); special.insert("__placement_new"); diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index 8c61f16eaf5..c9969611da3 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/src/statement-list/statement_list_entry_point.cpp @@ -11,6 +11,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include "statement_list_entry_point.h" +#include #include #include @@ -21,9 +22,6 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include -/// Name of the CPROVER-specific variable that specifies the rounding mode. -#define ROUNDING_MODE_NAME CPROVER_PREFIX "rounding_mode" - /// Postfix for the artificial data block that is created when calling a main /// symbol that is a function block. #define DB_ENTRY_POINT_POSTFIX "_entry_point" @@ -146,7 +144,7 @@ static void generate_statement_list_init_function(symbol_tablet &symbol_table) static void generate_rounding_mode(symbol_tablet &symbol_table) { symbolt rounding_mode; - rounding_mode.name = ROUNDING_MODE_NAME; + rounding_mode.name = rounding_mode_identifier(); rounding_mode.type = signed_int_type(); rounding_mode.is_thread_local = true; rounding_mode.is_static_lifetime = true; diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 540cff56b12..2f7041b014b 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -19,8 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com class constant_exprt; class floatbv_typet; -const char ID_cprover_rounding_mode_str[] = CPROVER_PREFIX "rounding_mode"; - class ieee_float_spect { public: