cprover
goto_program_template.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Goto Program Template
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
goto_program_template.h
"
13
14
#include <ostream>
15
16
std::ostream &
operator<<
(std::ostream &out,
goto_program_instruction_typet
t)
17
{
18
switch
(t)
19
{
20
case
NO_INSTRUCTION_TYPE
: out <<
"NO_INSTRUCTION_TYPE"
;
break
;
21
case
GOTO
: out <<
"GOTO"
;
break
;
22
case
ASSUME
: out <<
"ASSUME"
;
break
;
23
case
ASSERT
: out <<
"ASSERT"
;
break
;
24
case
OTHER
: out <<
"OTHER"
;
break
;
25
case
DECL
: out <<
"DECL"
;
break
;
26
case
DEAD
: out <<
"DEAD"
;
break
;
27
case
SKIP
: out <<
"SKIP"
;
break
;
28
case
START_THREAD
: out <<
"START_THREAD"
;
break
;
29
case
END_THREAD
: out <<
"END_THREAD"
;
break
;
30
case
LOCATION
: out <<
"LOCATION"
;
break
;
31
case
END_FUNCTION
: out <<
"END_FUNCTION"
;
break
;
32
case
ATOMIC_BEGIN
: out <<
"ATOMIC_BEGIN"
;
break
;
33
case
ATOMIC_END
: out <<
"ATOMIC_END"
;
break
;
34
case
RETURN
: out <<
"RETURN"
;
break
;
35
case
ASSIGN
: out <<
"ASSIGN"
;
break
;
36
case
FUNCTION_CALL
: out <<
"FUNCTION_CALL"
;
break
;
37
default
:
38
out <<
"?"
;
39
}
40
41
return
out;
42
}
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition:
goto_program_template.h:28
FUNCTION_CALL
Definition:
goto_program_template.h:46
START_THREAD
Definition:
goto_program_template.h:36
ASSUME
Definition:
goto_program_template.h:32
RETURN
Definition:
goto_program_template.h:42
DEAD
Definition:
goto_program_template.h:45
SKIP
Definition:
goto_program_template.h:35
operator<<
std::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Definition:
goto_program_template.cpp:16
ATOMIC_END
Definition:
goto_program_template.h:41
goto_program_template.h
Goto Program Template.
END_THREAD
Definition:
goto_program_template.h:37
ATOMIC_BEGIN
Definition:
goto_program_template.h:40
GOTO
Definition:
goto_program_template.h:31
DECL
Definition:
goto_program_template.h:44
ASSERT
Definition:
goto_program_template.h:33
NO_INSTRUCTION_TYPE
Definition:
goto_program_template.h:30
END_FUNCTION
Definition:
goto_program_template.h:39
OTHER
Definition:
goto_program_template.h:34
LOCATION
Definition:
goto_program_template.h:38
ASSIGN
Definition:
goto_program_template.h:43
goto-programs
goto_program_template.cpp
Generated by
1.8.14