Documentation roadmap

[shaobo-he]

This issue consolidates the currently open documentation-specific issues into one documentation roadmap.

Scope

Use this issue to track documentation work that explains how to use SMACK effectively, rather than feature implementation or verifier behavior changes.

Merged Issues

• Improve “Running Smack” documentation #206: Improve "Running Smack" documentation.
  • Add a basic getting-started path with assertions, assumptions, nondeterministic inputs, loops, bounded unrolling, and expected verification outcomes.
• Document SMACK command line options #747: Document SMACK command-line options.
  • Provide a maintained option reference and clarify commonly confused flags.
• Document how to use whole-program-llvm with SMACK #407: Document how to use whole-program-llvm with SMACK.
  • Add a short tutorial for project/build-system workflows, including the existing idea of a make-like workflow.
• Advanced SMACK guide #798: Advanced SMACK guide.
  • Document advanced uses such as __SMACK_code, __SMACK_top_decl, custom uninterpreted functions, and modeling patterns at the C level.

Proposed Structure

1. Quick start: minimal C example, running SMACK, interpreting verified/error/unknown.
2. Core verification concepts: assertions, assumptions, nondeterminism, loops, unrolling, entry points.
3. Command-line reference: stable user-facing options grouped by task.
4. Build workflows: single file, LLVM IR input, and whole-program/project workflows.
5. Advanced modeling: __SMACK_code, top-level declarations, custom abstractions, and caveats.
6. Troubleshooting: common failures, missing tools, verifier output, and when a result is approximate.

Done Criteria

• The older issues listed above are represented here with enough detail that they can remain closed.
• The documentation has clear examples that can be copied into tests or examples where practical.
• Command-line documentation is generated or checked against the implementation where feasible, so it does not drift immediately.