@@ -7,7 +7,48 @@ CBMC and the assorted CProver tools.
77## goto_modelt
88
99The ` 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+ ```
1152
1253A ` goto_modelt ` is effectively a pair, consisting of:
1354
0 commit comments