@@ -7,7 +7,7 @@ CBMC and the assorted CProver tools.
7
7
## goto_modelt
8
8
9
9
The ` goto_modelt ` is the main data structure that CBMC (and the other tools) used
10
- for the GOTO-IR (the ` GOTO ` Intermediate Representation) .
10
+ for the GOTO intermediate representation .
11
11
12
12
A ` goto_modelt ` is effectively a pair, consisting of:
13
13
@@ -29,7 +29,7 @@ The abstract interface of `goto_modelt` is outlined in the file
29
29
## goto_functiont
30
30
31
31
A ` goto_functiont ` is also defined as a pair. It's designed to represent a function
32
- at the IR level, and effectively it's the following data type (in pseudocode):
32
+ at the goto level, and effectively it's the following data type (in pseudocode):
33
33
34
34
``` js
35
35
type goto_functiont {
@@ -46,7 +46,7 @@ in the symbol-table for their values.
46
46
47
47
## goto_programt
48
48
49
- A ` goto_programt ` is a list of GOTO-IR instructions. In pseudocode, it would
49
+ A ` goto_programt ` is a list of GOTO instructions. In pseudocode, it would
50
50
look like ` type goto_programt = list<goto_instructiont> ` .
51
51
52
52
An instruction (` goto_instructiont ` ) is a triple (an element with three subcomponents),
@@ -88,7 +88,7 @@ tree that ends up modeling graphs like ASTs, CFGs, etc.
88
88
various expressions, usually the result of some early processing, e.g. the result of the
89
89
frontend parsing a file).
90
90
91
- This means that ` codet ` s, representing GOTO-IR instructions * also* have a ` source_locationt `
91
+ This means that ` codet ` s, representing GOTO instructions * also* have a ` source_locationt `
92
92
attached to them, by virtue of inheriting from ` exprt ` .
93
93
94
94
For the most part, ` source_locationt ` is something that is only being used when we print
0 commit comments