cprover
/builddir/build/BUILD/cbmc-cbmc-5.10/doc/architectural/data-structures-from-ast-to-goto-program.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page data-structures-from-ast-to-goto-program Data structures: from AST to GOTO program
3 
4 \author Martin Brain, Peter Schrammel
5 
6 ## goto_programt ##
7 
8 See \ref goto_programt.
9 
10 ### instructiont ###
11 
12 See [instructiont](\ref goto_programt::instructiont).
13 
14 #### Types, motivation of each type #####
15 
16 See [instructiont](\ref goto_programt::instructiont).
17 
18 #### Accepted code (codet) values ####
19 
20 To be documented.
21 
22 #### Accepted guard (exprt) values ####
23 
24 To be documented.
25 
26 ## goto_functionst ##
27 
28 \ref goto_functionst is a map from function names to function bodies (CFGs).
29 
30 To be documented.
31 
32 ## goto_modelt ##
33 
34 \ref goto_modelt is a compilation unit.
35 
36 To be documented.
37 
38 ## Example: ##
39 
40 ### Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; } ###
41 
42 To be documented.