cprover
symex_complexity_limit_exceeded_action.h
Go to the documentation of this file.
1 // Copyright 2016-2019 Diffblue Limited. All Rights Reserved.
2 
3 #ifndef CPROVER_GOTO_SYMEX_SYMEX_COMPLEXITY_LIMIT_EXCEEDED_ACTION_H
4 #define CPROVER_GOTO_SYMEX_SYMEX_COMPLEXITY_LIMIT_EXCEEDED_ACTION_H
5 
6 #include "complexity_limiter.h"
7 #include "complexity_violation.h"
8 #include <util/std_expr.h>
9 
13 {
14 public:
15  virtual void transform(
16  const complexity_violationt heuristic_result,
17  goto_symex_statet &current_state)
18  {
19  current_state.reachable = false;
20  }
22  {
23  }
24 };
25 
26 #endif // CPROVER_GOTO_SYMEX_SYMEX_COMPLEXITY_LIMIT_EXCEEDED_ACTION_H
goto_statet::reachable
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:54
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
symex_complexity_limit_exceeded_actiont::~symex_complexity_limit_exceeded_actiont
virtual ~symex_complexity_limit_exceeded_actiont()
Definition: symex_complexity_limit_exceeded_action.h:21
complexity_violationt
complexity_violationt
What sort of symex-complexity violation has taken place.
Definition: complexity_violation.h:18
symex_complexity_limit_exceeded_actiont::transform
virtual void transform(const complexity_violationt heuristic_result, goto_symex_statet &current_state)
Definition: symex_complexity_limit_exceeded_action.h:15
symex_complexity_limit_exceeded_actiont
Default heuristic transformation that cancels branches when complexity has been breached.
Definition: symex_complexity_limit_exceeded_action.h:13
complexity_limiter.h
Symbolic Execution.
complexity_violation.h
std_expr.h
API to expression classes.