File tree 1 file changed +12
-4
lines changed 1 file changed +12
-4
lines changed Original file line number Diff line number Diff line change @@ -9,11 +9,19 @@ CBMC and the assorted CProver tools.
9
9
The ` goto_modelt ` is the main data structure that CBMC (and the other tools) use to
10
10
represent GOTO-IR (the ` GOTO ` Intermediate Representation).
11
11
12
- A ` goto_modelt ` is effectively a product type , consisting of:
12
+ A ` goto_modelt ` is effectively a pair , consisting of:
13
13
14
- * A list of GOTO functions (pseudocode: ` type goto_functionst = list<goto_functiont> ` )
15
- * A symbol table containing symbol references for the symbols contained in the
16
- GOTO functions (pseudocode: ` type symbol_tablet = map<identifier, symbolt> ` ).
14
+ * A list of GOTO functions,
15
+ * A symbol table containing symbol references for the symbols contained in the GOTO functions.
16
+
17
+ In pseudocode, the type looks this:
18
+
19
+ ``` js
20
+ type goto_modelt {
21
+ type goto_functionst = list< goto_functiont>
22
+ type symbol_tablet = map< identifier, symbolt>
23
+ }
24
+ ```
17
25
18
26
The abstract interface of ` goto_modelt ` is outlined in the file
19
27
[ ` src/goto-programs/abstract_goto_model.h ` ] ( ../../src/goto-programs/abstract_goto_model.h ) .
You can’t perform that action at this time.
0 commit comments