CBMC
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_violation.h"
7 #include "goto_symex_state.h"
8 
12 {
13 public:
14  virtual void transform(
15  const complexity_violationt heuristic_result,
16  goto_symex_statet &current_state)
17  {
18  current_state.reachable = false;
19  }
21  {
22  }
23 };
24 
25 #endif // CPROVER_GOTO_SYMEX_SYMEX_COMPLEXITY_LIMIT_EXCEEDED_ACTION_H
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:62
Central data structure: state.
Default heuristic transformation that cancels branches when complexity has been breached.
virtual void transform(const complexity_violationt heuristic_result, goto_symex_statet &current_state)
complexity_violationt
What sort of symex-complexity violation has taken place.
Symbolic Execution.