Value-Set Analysis is a binary data-flow analysis for tracking the values that each variable may assume for each program point. You can find more information about VSA here and here.
For this project a static analyzer was developed for a lightweight version of the VSA, able to analyze each integer-type data object of a single-procedure program.
In order to analyze your programs, you must compile classes and modules following the order of dependencies:
- Expression.fs
- MemoryRegion.fs
- Values.fs
- INode.fsi
- Node.fs
- ICFG.fsi
- CFG.fs
- PreliminaryAnalysis.fs
- ILattice.fsi
- VSLattice.fs
- TransferFunctions.fs
- Work-List.fs
- Main.fs
After that, you can define your Control Flow Graph cfg using the language wrote in Expression.fs and the classes ICFG and INode, and run
main cfg
Each Abstract State corresponds to the node preceding the current node. Then the information about a node i is reported in the abstract state relative to the node i+1.