|
|
|---|
|
|
|
|---|
ATC tutorial.
This tutorial is work in progress, but it should be already useful in its current incomplete form. This tutorial's goal is to provide user-level pedagogical information on how ATC works and how to use ATC effectively. See the ATC manual page for the ATC reference documentation.
In this tutorial, we refer to the official C standard in the manner explained in the top-level XDOC topic of our C library.
This tutorial consists of this top-level page plus a number of hyperlinked pages, all of which are subtopics of this top-level page, listed below alphabetically for easy reference. Starting from this top-level page, we provide Start and Next links to navigate sequentially through all the tutorial pages; we also provide Previous links going the opposite direction. It is recommended to follow this order when reading this tutorial for the first time.
Some pages may be skipped at first reading, because they contain additional information that may not be necessary for a user to know in order to start using ATC; such pages include explicit text indicating that. However, it is recommended to read all the pages, eventually.
Start: Motivation for Generating C Code from ACL2