cprover
set_properties.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Set the properties to check
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
13
#define CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
14
15
#include "
goto_model.h
"
16
17
void
set_properties
(
18
goto_functionst
&goto_functions,
19
const
std::list<std::string> &properties);
20
21
void
set_properties
(
22
goto_modelt
&goto_model,
23
const
std::list<std::string> &properties);
24
25
void
make_assertions_false
(
goto_functionst
&);
26
void
make_assertions_false
(
goto_modelt
&);
27
28
void
label_properties
(
goto_functionst
&);
29
void
label_properties
(
goto_programt
&);
30
void
label_properties
(
goto_modelt
&);
31
32
#endif // CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition:
goto_model.h:26
label_properties
void label_properties(goto_functionst &)
Definition:
set_properties.cpp:120
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:73
set_properties
void set_properties(goto_functionst &goto_functions, const std::list< std::string > &properties)
Definition:
set_properties.cpp:103
make_assertions_false
void make_assertions_false(goto_functionst &)
Definition:
set_properties.cpp:136
goto-programs
set_properties.h
Generated by
1.8.20