expr_query.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Unit test utilities
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_TESTING_UTILS_EXPR_QUERY_H
#define CPROVER_TESTING_UTILS_EXPR_QUERY_H
 
#include <testing-utils/use_catch.h>
 
#include <util/expr_cast.h>
 
template <typename T = exprt>
class expr_queryt
{
  static_assert(
    std::is_base_of<exprt, T>::value,
    "T should inherit from exprt");
 
public:
  explicit expr_queryt(T e) : value(std::move(e))
  {
  }
  explicit expr_queryt(T e) : value(std::move(e)) {…}
 
  template <typename targett>
  expr_queryt<targett> as() const
  {
    auto result = expr_try_dynamic_cast<targett>(static_cast<exprt>(value));
    REQUIRE(result);
    return expr_queryt<targett>(*result);
  }
  expr_queryt<targett> as() const {…}
 
  expr_queryt<exprt> operator[](const std::size_t i) const
  {
    REQUIRE(value.operands().size() > i);
    return expr_queryt<exprt>(value.operands()[i]);
  }
  expr_queryt<exprt> operator[](const std::size_t i) const {…}
 
  T get() const
  {
    return value;
  }
  T get() const {…}
 
private:
  T value;
};
class expr_queryt {…};
 
inline expr_queryt<exprt> make_query(exprt e)
{
  return expr_queryt<exprt>(std::move(e));
}
inline expr_queryt<exprt> make_query(exprt e) {…}
 
#endif // CPROVER_TESTING_UTILS_EXPR_QUERY_H