Coding Standards

This document describes a few coding standards that are used in IKOS.

C++ Standard Version

IKOS is currently written in C++14.

Use 2 spaces for indentation (Google Style Guide)
Do not indent inside a namespace (LLVM Coding Standards)
Indent each case in a switch statement (Google Style Guide)
No trailing whitespaces at the end of a line (Google Style Guide)
Remove unnecessary parenthesis around returned values (Google Style Guide)
Binary operators usually have spaces around them (Google Style Guide)
No extra space between a function name and arguments
Do not align variable definitions (Python Style Guide)
Prefix member variables with an underscore (Arnaud's Style)
Do not use using namespace in header files (Google Style Guide, LLVM Coding Standards)
Sort included headers in the following order: standards, 3rd-party, our own
Use Doxygen comments (LLVM Coding Standards)
Each line should fit within 80 columns (LLVM Coding Standards)
Treat compiler warnings like errors (LLVM Coding Standards)
Use struct only when all members are public, otherwise use class (LLVM Coding Standards)
Use auto to make the code more readable (LLVM Coding Standards)
Use early exit and continue (LLVM Coding Standards)
Assert liberally (LLVM Coding Standards)
Don't evaluate end() every time through a loop (LLVM Coding Standards)
Avoid std::endl (LLVM Coding Standards)
Naming conventions are specified in the .clang-tidy configuration file
Use K&R style:

if (cond) {
  f();
} else if (cond1) {
  g();
} else {
  h();
}

IKOS developers should use clang-format to format the source code with a predefined set of style rules.

See .clang-format for the set of rules.

Always run the following command before committing any changes:

$ git-clang-format -f

To run clang-format on the whole repository, use:

$ script/run-clang-format

IKOS developers should use clang-tidy to perform diagnosis for typical programming errors, style violation, interface misuse, etc.

See .clang-tidy for the set of checks.

To run clang-tidy on the whole repository, use:

$ mkdir build
$ cd build
$ cmake ..
$ ../script/run-clang-tidy

IKOS developers should use clang sanitizers to check for undefined behaviors at run-time.

To build IKOS with clang sanitizers, use the following cmake options: