CBMC
Loading...
Searching...
No Matches
uninitialized.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Detection for Uninitialized Local Variables
4
5Author: Daniel Kroening
6
7Date: January 2010
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H
15#define CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H
16
17#include <iosfwd>
18
19class goto_modelt;
20
22
24 const goto_modelt &,
25 std::ostream &out);
26
27#define OPT_UNINITIALIZED_CHECK "(uninitialized-check)"
28
29#define HELP_UNINITIALIZED_CHECK \
30 " {y--uninitialized-check} \t " \
31 "add checks for uninitialized locals (experimental)\n"
32
33#endif // CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H
void add_uninitialized_locals_assertions(goto_modelt &)
void show_uninitialized(const goto_modelt &, std::ostream &out)