|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <goto-programs/goto_functions_algorithm.h>#include <util/arith/mp_arith.h>#include <irep2/irep2.h>Go to the source code of this file.
Classes | |
| class | goto_check_excessive_alloc |
| Detect memory allocations whose requested size can exceed a configurable byte bound K (CWE-789, "Memory Allocation with Excessive Size Value"). More... | |