Skip to content

Add typet and symbol_typet documentation to util README [DOC-12] #2823

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 17, 2018
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions src/util/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ CPROVER codebase.
See detailed documentation at \ref irept.

[irept](\ref irept)s are generic tree nodes. You
should think of each node as holding a single string ([data](irept::data),
should think of each node as holding a single string ([data](\ref irept::data),
actually an \ref irep_idt) and lots of child nodes, some of which are numbered
([sub](\ref irept::dt::sub)) and some of which are labelled, and the label
can either start with a “\#” ([comments](\ref irept::dt::comments)) or without
Expand Down Expand Up @@ -101,15 +101,15 @@ See documentation at \ref dstringt.

\subsection typet_section typet

See \ref typet.

To be documented.
\ref typet represents the type of an expression. Types may have subtypes,
stored in two [sub](\ref irept::dt::sub)s named “subtype” (a single type) and
“subtypes” (a vector of types). For pre-defined types see `std_types.h` and
`mathematical_types.h`.

\subsubsection symbol_typet_section symbol_typet

See \ref symbol_typet.

To be documented.
\ref symbol_typet is a type used to store a reference to the symbol table. The
full \ref symbolt can be retrieved using the identifier of \ref symbol_typet.

\subsection exprt_section exprt

Expand Down