gcc_conditional_expression.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Lowering of GCC's `a ? : b` conditional expression
 
Author: Michael Tautschnig
 
\*******************************************************************/

 
#ifndef CPROVER_ANSI_C_GCC_CONDITIONAL_EXPRESSION_H
#define CPROVER_ANSI_C_GCC_CONDITIONAL_EXPRESSION_H
 
#include <util/invariant.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/std_types.h>

inline if_exprt lower_gcc_conditional_expression(const side_effect_exprt &expr)
{
  PRECONDITION(expr.get_statement() == ID_gcc_conditional_expression);
  const binary_exprt &binary = to_binary_expr(expr);
  if_exprt if_expr{
    typecast_exprt::conditional_cast(binary.op0(), bool_typet{}),
    binary.op0(),
    binary.op1(),
    expr.type()};
  if_expr.add_source_location() = expr.source_location();
  return if_expr;
}

inline void lower_gcc_conditional_expressions(exprt &expr)
{
  for(auto &op : expr.operands())
    lower_gcc_conditional_expressions(op);
 
  if(
    expr.id() == ID_side_effect &&
    to_side_effect_expr(expr).get_statement() ==
      ID_gcc_conditional_expression &&
    expr.operands().size() == 2)
  {
    if_exprt if_expr =
      lower_gcc_conditional_expression(to_side_effect_expr(expr));
    expr.swap(if_expr);
  }
}
 
#endif // CPROVER_ANSI_C_GCC_CONDITIONAL_EXPRESSION_H