adjust_float_expressions.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
 
#include <goto-programs/goto_functions.h>
 
class exprt;
class namespacet;
class goto_modelt;
 
void adjust_float_expressions(
  exprt &expr,
  const namespacet &ns);
 
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode);
 
void adjust_float_expressions(
  goto_functionst::goto_functiont &goto_function,
  const namespacet &ns);
 
void adjust_float_expressions(
  goto_functionst &goto_functions,
  const namespacet &ns);
 
void adjust_float_expressions(goto_modelt &goto_model);
 
irep_idt rounding_mode_identifier();
 
#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H