Content area
In our times, when the world is increasingly becoming more dependent on software programs, writing bug-free, correct programs is crucial. Program verification based on formal methods can guarantee this by detecting run-time errors in safety-critical systems to avoid possible adverse impacts on human life and save time and money. This project work tries to leverage Abstract Interpretation techniques for static analysis of C programs. C Analyzer is a tool developed for static analysis of C programs. This implementation of C Analyzer provides a plug-and-play domain architecture for multiple abstract domains to be used. C Analyzer supports four abstract domains - Interval, Octagon, Polyhedra, and Bit Vector. We use these different domains for required precision in program verification. C Analyzer tool uses LLVM C/C++ compiler frontend Clang API to generate and traverse the Control Flow Graph (CFG) of a given C program. This tool generates invariants in different abstract domains for statements in basic blocks of CFG during CFG traversal. Using these invariants, some properties of a program, such as dividing by zero, modulus zero, arithmetic overflow, etc., can be analyzed. We also use a source-to-source transformation tool, CIL (Common Intermediate language), to transform some C constructs into simpler constructs, such as transforming logical operators, switch statements, and conditional operators into if-else ladders and transforming do-while and for loops into while loops. Using C Analyzer, C program constructs such as declarations, assignments, binary operations (arithmetic, relational, bitwise shift, etc.), conditions (if-else), loops (while, do while, for loop), nested conditions, and nested loops can be analyzed. Currently, this tool does not support arrays, structures, unions, pointers, or function calls.