complexity_limiter.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: John Dumbell
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
#define CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
 
#include <util/message.h>
 
#include "complexity_violation.h"
#include "symex_complexity_limit_exceeded_action.h"
 
class optionst;
 
class complexity_limitert
{
public:
  complexity_limitert() = default;
 
  complexity_limitert(message_handlert &logger, const optionst &options);
 
  inline bool complexity_limits_active()
  {
    return this->complexity_active;
  }
 
  complexity_violationt check_complexity(goto_symex_statet &state);
 
  void run_transformations(
    complexity_violationt complexity_violation,
    goto_symex_statet &current_state);
 
  static std::size_t bounded_expr_size(const exprt &expr, std::size_t limit);
 
protected:
  mutable messaget log;
 
  bool complexity_active = false;
 
  std::vector<symex_complexity_limit_exceeded_actiont>
    violation_transformations;
 
  symex_complexity_limit_exceeded_actiont default_transformation;
 
  std::size_t max_complexity = 0;
 
  std::size_t max_loops_complexity = 0;
 
  bool are_loop_children_too_complicated(call_stackt &current_call_stack);
 
  static bool in_blacklisted_loop(
    const call_stackt &current_call_stack,
    const goto_programt::const_targett &instr);
 
  static framet::active_loop_infot *
  get_current_active_loop(call_stackt &current_call_stack);
};
 
#endif // CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H