From 3dc2244a574322634ee237e02c278f40ef0b850c Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 26 Apr 2018 12:43:11 +0100 Subject: [PATCH 1/3] Move adjust_float_expressions to goto-programs --- src/cbmc/cbmc_parse_options.cpp | 3 ++- src/clobber/Makefile | 1 - src/goto-diff/Makefile | 1 - src/goto-diff/goto_diff_parse_options.cpp | 2 +- src/goto-programs/Makefile | 3 ++- .../adjust_float_expressions.cpp | 2 +- .../adjust_float_expressions.h | 6 +++--- src/goto-symex/Makefile | 3 +-- src/jbmc/jbmc_parse_options.cpp | 4 ++-- 9 files changed, 12 insertions(+), 13 deletions(-) rename src/{goto-symex => goto-programs}/adjust_float_expressions.cpp (99%) rename src/{goto-symex => goto-programs}/adjust_float_expressions.h (79%) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index bedc9ae667d..45cef6eaba2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -26,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include #include @@ -49,7 +51,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/clobber/Makefile b/src/clobber/Makefile index aa195f87233..4f9562e354b 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -13,7 +13,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../goto-symex/adjust_float_expressions$(OBJEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/dump_c$(OBJEXT) \ diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 9325b323c64..648aa90b9a2 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -25,7 +25,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ ../goto-instrument/cover_instrument_other$(OBJEXT) \ ../goto-instrument/cover_util$(OBJEXT) \ - ../goto-symex/adjust_float_expressions$(OBJEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 889fee4c0ed..e32b36ae50b 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -24,6 +24,7 @@ Author: Peter Schrammel #include +#include #include #include #include @@ -45,7 +46,6 @@ Author: Peter Schrammel #include #include -#include #include diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index c90d750b1d9..98d2cc2a47f 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,4 +1,5 @@ -SRC = basic_blocks.cpp \ +SRC = adjust_float_expressions.cpp \ + basic_blocks.cpp \ builtin_functions.cpp \ class_hierarchy.cpp \ class_identifier.cpp \ diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp similarity index 99% rename from src/goto-symex/adjust_float_expressions.cpp rename to src/goto-programs/adjust_float_expressions.cpp index 89abaf65757..c7163c8b19b 100644 --- a/src/goto-symex/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include "goto_model.h" static bool have_to_adjust_float_expressions( const exprt &expr, diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-programs/adjust_float_expressions.h similarity index 79% rename from src/goto-symex/adjust_float_expressions.h rename to src/goto-programs/adjust_float_expressions.h index bd011641d54..eaa5417b75d 100644 --- a/src/goto-symex/adjust_float_expressions.h +++ b/src/goto-programs/adjust_float_expressions.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution -#ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H -#define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H +#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H +#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H #include @@ -31,4 +31,4 @@ void adjust_float_expressions( const namespacet &ns); void adjust_float_expressions(goto_modelt &goto_model); -#endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H +#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index dc4c73f3c15..79e2084a297 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -1,5 +1,4 @@ -SRC = adjust_float_expressions.cpp \ - auto_objects.cpp \ +SRC = auto_objects.cpp \ build_goto_trace.cpp \ goto_symex.cpp \ goto_symex_state.cpp \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 2be5ebd63c6..9e0bd748f7a 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -26,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include #include @@ -41,8 +43,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include #include From 5f7bc1540d63078bdc48775c66ca198f0d3f42cf Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 17 Apr 2018 13:32:29 +0100 Subject: [PATCH 2/3] Add float support to constant propagator domain --- .../main.c | 9 ++++ .../test.desc | 8 +++ .../constant_propagation_rounding_mode/main.c | 12 +++++ .../test.desc | 9 ++++ src/analyses/constant_propagator.cpp | 52 +++++++++++-------- src/analyses/constant_propagator.h | 2 + 6 files changed, 70 insertions(+), 22 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_floating_point_div/main.c create mode 100644 regression/goto-analyzer/constant_propagation_floating_point_div/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_rounding_mode/main.c create mode 100644 regression/goto-analyzer/constant_propagation_rounding_mode/test.desc diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/main.c b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c new file mode 100644 index 00000000000..f80f5f042d4 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c @@ -0,0 +1,9 @@ +#include + +#define ROUND_F(x) ((int)((x) + 0.5f)) +int eight = ROUND_F(100.0f / 12.0f); + +int main() +{ + assert(eight == 8); +} diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc new file mode 100644 index 00000000000..2fc631c1933 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_rounding_mode/main.c new file mode 100644 index 00000000000..ace3fe60eb5 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_rounding_mode/main.c @@ -0,0 +1,12 @@ +#include + +int main(void) +{ + __CPROVER_rounding_mode = 0; + float rounded_up = 1.0f / 10.0f; + __CPROVER_rounding_mode = 1; + float rounded_down = 1.0f / 10.0f; + assert(rounded_up - 0.1f >= 0); + assert(rounded_down - 0.1f < 0); + return 0; +} diff --git a/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc new file mode 100644 index 00000000000..c7c1e94639c --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: Success +^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: Success +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index bbf20546b68..71018dd923a 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -22,6 +22,7 @@ Author: Peter Schrammel #include #include +#include void constant_propagator_domaint::assign_rec( valuest &values, @@ -35,8 +36,7 @@ void constant_propagator_domaint::assign_rec( const symbol_exprt &s=to_symbol_expr(lhs); exprt tmp=rhs; - values.replace_const(tmp); - simplify(tmp, ns); + try_evaluate(tmp, ns); if(tmp.is_constant()) values.set_to(s, tmp); @@ -99,10 +99,10 @@ void constant_propagator_domaint::transform( // Comparing iterators is safe as the target must be within the same list // of instructions because this is a GOTO. if(from->get_target()==to) - g=simplify_expr(from->guard, ns); + g = from->guard; else - g=simplify_expr(not_exprt(from->guard), ns); - + g = not_exprt(from->guard); + try_evaluate(g, ns); if(g.is_false()) values.set_to_bottom(); else @@ -269,10 +269,7 @@ bool constant_propagator_domaint::ai_simplify( exprt &condition, const namespacet &ns) const { - bool b=values.replace_const.replace(condition); - b&=simplify(condition, ns); - - return b; + return try_evaluate(condition, ns); } @@ -504,6 +501,21 @@ bool constant_propagator_domaint::merge( return values.merge(other.values); } +/// Attempt to evaluate expression using domain knowledge +/// This function changes the expression that is passed into it. +/// \param expr The expression to evaluate +/// \param ns The namespace for symbols in the expression +/// \return True if the expression is unchanged, false otherwise +bool constant_propagator_domaint::try_evaluate( + exprt &expr, + const namespacet &ns) const +{ + adjust_float_expressions(expr, ns); + bool did_not_change_anything = values.replace_const.replace(expr); + did_not_change_anything &= simplify(expr, ns); + return did_not_change_anything; +} + void constant_propagator_ait::replace( goto_functionst &goto_functions, const namespacet &ns) @@ -529,38 +541,34 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { - s_it->second.values.replace_const(it->guard); - simplify(it->guard, ns); + s_it->second.try_evaluate(it->guard, ns); } else if(it->is_assign()) { exprt &rhs=to_code_assign(it->code).rhs(); - s_it->second.values.replace_const(rhs); - simplify(rhs, ns); + s_it->second.try_evaluate(rhs, ns); if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { - s_it->second.values.replace_const( - to_code_function_call(it->code).function()); - - simplify(to_code_function_call(it->code).function(), ns); + exprt &function = to_code_function_call(it->code).function(); + s_it->second.try_evaluate(function, ns); exprt::operandst &args= to_code_function_call(it->code).arguments(); - for(exprt::operandst::iterator o_it=args.begin(); - o_it!=args.end(); ++o_it) + for(auto &arg : args) { - s_it->second.values.replace_const(*o_it); - simplify(*o_it, ns); + s_it->second.try_evaluate(arg, ns); } } else if(it->is_other()) { if(it->code.get_statement()==ID_expression) - s_it->second.values.replace_const(it->code); + { + s_it->second.try_evaluate(it->code, ns); + } } } } diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0fc4796e8b7..61dd564fe83 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -138,6 +138,8 @@ class constant_propagator_domaint:public ai_domain_baset valuest values; + bool try_evaluate(exprt &expr, const namespacet &ns) const; + protected: void assign_rec( valuest &values, From a05545408726f62f4a611a9a071f0ce329aa41d3 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Wed, 18 Apr 2018 17:49:38 +0100 Subject: [PATCH 3/3] Try all rounding modes when domain is unknown For rounding modes in constant propagator domain --- .../main.c | 27 +++++++ .../test.desc | 13 ++++ src/analyses/constant_propagator.cpp | 78 ++++++++++++++++--- src/analyses/constant_propagator.h | 8 +- src/cbmc/cbmc_parse_options.cpp | 1 - .../goto_analyzer_parse_options.cpp | 2 + src/jbmc/jbmc_parse_options.cpp | 1 - src/util/ieee_float.h | 4 + 8 files changed, 120 insertions(+), 14 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c create mode 100644 regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c new file mode 100644 index 00000000000..6b1e90e3427 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c @@ -0,0 +1,27 @@ +#include +#include +#include + +int nondet_rounding_mode(void); + +int main(void) +{ + // slightly bigger than 0.1 + float f = 1.0f / 10.0f; + + // now we don't know what rounding mode we're in + __CPROVER_rounding_mode = nondet_rounding_mode(); + // depending on rounding mode 1.0f/10.0f could + // be greater or smaller than 0.1 + + // definitely not smaller than -0.1 + assert((1.0f / 10.0f) - f < -0.1f); + // might be smaller than 0 + assert((1.0f / 10.0f) - f < 0.0f); + // definitely smaller or equal to 0 + assert((1.0f / 10.0f) - f <= 0.0f); + // might be greater or equal to 0 + assert((1.0f / 10.0f) - f >= 0.0f); + // definitely not greater than 0 + assert((1.0f / 10.0f) - f > 0.0f); +} diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc new file mode 100644 index 00000000000..12b4b6443a2 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: Failure \(if reachable\) +\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: Unknown +\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: Success +\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: Unknown +\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: Failure \(if reachable\) + +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 71018dd923a..452e8355a93 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -16,13 +16,16 @@ Author: Peter Schrammel #include #endif +#include #include #include #include #include #include -#include + +#include +#include void constant_propagator_domaint::assign_rec( valuest &values, @@ -36,7 +39,7 @@ void constant_propagator_domaint::assign_rec( const symbol_exprt &s=to_symbol_expr(lhs); exprt tmp=rhs; - try_evaluate(tmp, ns); + partial_evaluate(tmp, ns); if(tmp.is_constant()) values.set_to(s, tmp); @@ -102,7 +105,7 @@ void constant_propagator_domaint::transform( g = from->guard; else g = not_exprt(from->guard); - try_evaluate(g, ns); + partial_evaluate(g, ns); if(g.is_false()) values.set_to_bottom(); else @@ -269,7 +272,7 @@ bool constant_propagator_domaint::ai_simplify( exprt &condition, const namespacet &ns) const { - return try_evaluate(condition, ns); + return partial_evaluate(condition, ns); } @@ -506,11 +509,64 @@ bool constant_propagator_domaint::merge( /// \param expr The expression to evaluate /// \param ns The namespace for symbols in the expression /// \return True if the expression is unchanged, false otherwise -bool constant_propagator_domaint::try_evaluate( +bool constant_propagator_domaint::partial_evaluate( + exprt &expr, + const namespacet &ns) const +{ + // 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(!values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str))) + { + return partial_evaluate_with_all_rounding_modes(expr, ns); + } + return replace_constants_and_simplify(expr, ns); +} + +/// Attempt to evaluate an expression in all rounding modes. +/// +/// If the result is the same for all rounding modes, change +/// expr to that result and return false. Otherwise, return true. +bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( + exprt &expr, + const namespacet &ns) const +{ // NOLINTNEXTLINE (whitespace/braces) + auto rounding_modes = std::array{ + // NOLINTNEXTLINE (whitespace/braces) + {ieee_floatt::ROUND_TO_EVEN, + ieee_floatt::ROUND_TO_ZERO, + ieee_floatt::ROUND_TO_MINUS_INF, + // NOLINTNEXTLINE (whitespace/braces) + ieee_floatt::ROUND_TO_PLUS_INF}}; + exprt first_result; + for(std::size_t i = 0; i < rounding_modes.size(); ++i) + { + constant_propagator_domaint child(*this); + child.values.set_to( + ID_cprover_rounding_mode_str, + from_integer(rounding_modes[i], integer_typet())); + exprt result = expr; + if(child.replace_constants_and_simplify(result, ns)) + { + return true; + } + else if(i == 0) + { + first_result = result; + } + else if(result != first_result) + { + return true; + } + } + expr = first_result; + return false; +} + +bool constant_propagator_domaint::replace_constants_and_simplify( exprt &expr, const namespacet &ns) const { - adjust_float_expressions(expr, ns); bool did_not_change_anything = values.replace_const.replace(expr); did_not_change_anything &= simplify(expr, ns); return did_not_change_anything; @@ -541,33 +597,33 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { - s_it->second.try_evaluate(it->guard, ns); + s_it->second.partial_evaluate(it->guard, ns); } else if(it->is_assign()) { exprt &rhs=to_code_assign(it->code).rhs(); - s_it->second.try_evaluate(rhs, ns); + s_it->second.partial_evaluate(rhs, ns); if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { exprt &function = to_code_function_call(it->code).function(); - s_it->second.try_evaluate(function, ns); + s_it->second.partial_evaluate(function, ns); exprt::operandst &args= to_code_function_call(it->code).arguments(); for(auto &arg : args) { - s_it->second.try_evaluate(arg, ns); + s_it->second.partial_evaluate(arg, ns); } } else if(it->is_other()) { if(it->code.get_statement()==ID_expression) { - s_it->second.try_evaluate(it->code, ns); + s_it->second.partial_evaluate(it->code, ns); } } } diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 61dd564fe83..e32a14bc0f2 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -138,7 +138,7 @@ class constant_propagator_domaint:public ai_domain_baset valuest values; - bool try_evaluate(exprt &expr, const namespacet &ns) const; + bool partial_evaluate(exprt &expr, const namespacet &ns) const; protected: void assign_rec( @@ -149,6 +149,12 @@ class constant_propagator_domaint:public ai_domain_baset bool two_way_propagate_rec( const exprt &expr, const namespacet &ns); + + bool partial_evaluate_with_all_rounding_modes( + exprt &expr, + const namespacet &ns) const; + + bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const; }; class constant_propagator_ait:public ait diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 45cef6eaba2..35069fc9665 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 04cd02412d1..296d3965782 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -56,6 +56,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "taint_analysis.h" #include "unreachable_instructions.h" @@ -477,6 +478,7 @@ int goto_analyzer_parse_optionst::doit() /// Depending on the command line mode, run one of the analysis tasks int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) { + adjust_float_expressions(goto_model); if(options.get_bool_option("taint")) { std::string taint_file=cmdline.get_value("taint"); diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 9e0bd748f7a..328dc639156 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 2127c89386a..52ece8d191f 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -14,10 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "mp_arith.h" #include "format_spec.h" +#include "irep.h" +#include "cprover_prefix.h" class constant_exprt; class floatbv_typet; +const char ID_cprover_rounding_mode_str[] = CPROVER_PREFIX "rounding_mode"; + class ieee_float_spect { public: