Tool strucure
Stanse is completely written in Java. (The only exception is the fast C parser for the includes.) In addition to checkers, there are 4 basic modules:
- C parsing and analysis
- Error reporting
- GUI
- CLI
Checkers
Currently there are two checkers implemented in Stanse. There is a good infrastructure in place to easily add another checker. More information in the API documentation.
AutomatonChecker
- Uses state automata to decribe errorneous behaviour.
- Multiple automata can be run in parallel.
- Automata are specified using readable XML files.
- Great variability due to using patterns on the AST structure.
ThreadChecker
- Finds a locking discipline violation among all created threads.
- Uses patterns on the AST specified by XML as well.
C parsing and analysis
- ANTLRv3 is the underlying parser generator.
- Internally the code is represented as an XML-encoded AST.
- Control-flow graphs, call graphs and variable tables are available to checkers.
- Code is preprocessed using
cpp. - Leading includes are stripped from the code and fast C parser is used to extract the relevant information from these includes.