diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index d0e3898b..1016deab 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -1023,7 +1023,7 @@ bool twols_parse_optionst::process_goto_program( remove_returns(goto_model); if(options.get_bool_option("competition-mode")) - assert_no_atexit(goto_model); + assert_no_unsupported_function_calls(goto_model); // now do full inlining, if requested if(options.get_bool_option("inline")) diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 329a2738..bdee884a 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -186,7 +186,7 @@ class twols_parse_optionst: void memory_assert_info(goto_modelt &goto_model); void handle_freed_ptr_compare(goto_modelt &goto_model); void assert_no_unsupported_functions(goto_modelt &goto_model); - void assert_no_atexit(goto_modelt &goto_model); + void assert_no_unsupported_function_calls(goto_modelt &goto_model); void fix_goto_targets(goto_modelt &goto_model); void make_assertions_false(goto_modelt &goto_model); void make_symbolic_array_indices(goto_modelt &goto_model); diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index a23215f1..a692ea3b 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -22,6 +22,8 @@ Author: Peter Schrammel #include "2ls_parse_options.h" +#define NOT_MATH_FUN(call, fun) call != fun &&call != fun "f" && call != fun "l" + void twols_parse_optionst::inline_main(goto_modelt &goto_model) { irep_idt start=goto_functionst::entry_point(); @@ -678,9 +680,13 @@ void twols_parse_optionst::assert_no_unsupported_functions( } } -/// Prevents usage of atexit function which is not supported, yet -/// Must be called before inlining since it will lose the calls -void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model) +/// Fail if the program contains a call to an unsupported function. These +/// include the atexit function and advanced math functions from math.h ( +/// these are either not defined in CBMC at all, or defined very imprecisely, +/// e.g. the result of cos is in <-1, 1> without any further information). +/// Must be called before inlining since it will lose the calls. +void twols_parse_optionst::assert_no_unsupported_function_calls( + goto_modelt &goto_model) { for(const auto &f_it : goto_model.goto_functions.function_map) { @@ -693,6 +699,23 @@ void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model) continue; auto &name=id2string(to_symbol_expr(function).get_identifier()); assert(name!="atexit"); + assert( + // Trigonometry + NOT_MATH_FUN(name, "cos") && NOT_MATH_FUN(name, "acos") && + NOT_MATH_FUN(name, "sin") && NOT_MATH_FUN(name, "asin") && + NOT_MATH_FUN(name, "tan") && NOT_MATH_FUN(name, "atan") && + NOT_MATH_FUN(name, "atan2") && + // Hyperbolic + NOT_MATH_FUN(name, "cosh") && NOT_MATH_FUN(name, "acosh") && + NOT_MATH_FUN(name, "sinh") && NOT_MATH_FUN(name, "asinh") && + NOT_MATH_FUN(name, "tanh") && NOT_MATH_FUN(name, "atanh") && + // Exponential + NOT_MATH_FUN(name, "exp") && NOT_MATH_FUN(name, "exp2") && + NOT_MATH_FUN(name, "expm1") && NOT_MATH_FUN(name, "log") && + NOT_MATH_FUN(name, "log10") && NOT_MATH_FUN(name, "log2") && + NOT_MATH_FUN(name, "log1p") && + // Other + NOT_MATH_FUN(name, "erf")); } } }