cprover
Data structures: from AST to GOTO program
Author
Martin Brain, Peter Schrammel

goto_programt

See goto_programt.

instructiont

See instructiont.

Types, motivation of each type

See instructiont.

Accepted code (codet) values

To be documented.

Accepted guard (exprt) values

To be documented.

goto_functionst

goto_functionst is a map from function names to function bodies (CFGs).

To be documented.

goto_modelt

goto_modelt is a compilation unit.

To be documented.

Example:

Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; }

To be documented.