File tree Expand file tree Collapse file tree 1 file changed +12
-4
lines changed
Expand file tree Collapse file tree 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.
99The ` goto_modelt ` is the main data structure that CBMC (and the other tools) use to
1010represent GOTO-IR (the ` GOTO ` Intermediate Representation).
1111
12- A ` goto_modelt ` is effectively a product type , consisting of:
12+ A ` goto_modelt ` is effectively a pair , consisting of:
1313
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+ ```
1725
1826The abstract interface of ` goto_modelt ` is outlined in the file
1927[ ` 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