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
12
class
symex_complexity_limit_exceeded_actiont
13
{
14
public
:
15
virtual
void
transform
(
16
const
complexity_violationt
heuristic_result,
17
goto_symex_statet
¤t_state)
18
{
19
current_state.
reachable
=
false
;
20
}
21
virtual
~symex_complexity_limit_exceeded_actiont
()
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 ¤t_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.
goto-symex
symex_complexity_limit_exceeded_action.h
Generated by
1.8.20