@@ -7,7 +7,48 @@ CBMC and the assorted CProver tools.
7
7
## goto_modelt
8
8
9
9
The ` goto_modelt ` is the top-level data structure that CBMC (and the other
10
- tools) use for holding the GOTO intermediate representation.
10
+ tools) use for holding the GOTO intermediate representation. The following
11
+ diagram is a simplified view of how the data structures relate to each other -
12
+
13
+ ``` mermaid
14
+ erDiagram
15
+ goto_modelt {
16
+ symbol_tablet symbol_table
17
+ goto_functionst goto_functions
18
+ }
19
+ goto_modelt ||--|| symbol_tablet : ""
20
+ goto_modelt ||--|| goto_functionst : ""
21
+ symbol_tablet {
22
+ symbol_map symbols
23
+ }
24
+ symbol_tablet ||--o{ symbolt : ""
25
+ symbolt {
26
+ string name
27
+ }
28
+ goto_functionst {
29
+ function_map functions
30
+ }
31
+ goto_functionst ||--o{ goto_functiont : ""
32
+ goto_functiont {
33
+ goto_programt body
34
+ ordered_collection_of parameter_identifiers
35
+ }
36
+ goto_functiont ||--|| goto_programt : ""
37
+ goto_programt {
38
+ ordered_collection_of instructions
39
+ }
40
+ goto_programt ||--o{ instructiont : ""
41
+ instructiont {
42
+ enumeration instruction_type
43
+ goto_program_codet code
44
+ boolean_expression guard
45
+ source_locationt source_location
46
+ }
47
+ instructiont ||--|| goto_program_instruction_typet : ""
48
+ instructiont ||--o| goto_program_codet : ""
49
+ instructiont ||--o| source_locationt : ""
50
+ goto_program_codet ||--o| source_locationt : ""
51
+ ```
11
52
12
53
A ` goto_modelt ` is effectively a pair, consisting of:
13
54
0 commit comments