Official LSV Web Site
 |
|
 |
Tools of the Csur Project
The csur project comes with a set of tools. The architecture of tools follows the scheme defined in the documentation section (see OVERVIEW ).The csur compiler : csurcc and csurar
csurcc compiles source code and generates a table containing all functions of the source code.The csur C analyzer : csurrun
csurrun is a generic C code analyzer. This analyzer is a classical (see references ) C static analyzer. We use csurcc to generate control flow graphs for each function in programs. Then, csurrun performs functions analysis and generates dumps of abstract memory at each control points. Actually this analyzer works on:- basic numeric types : integer ( int , unsigned int , long ...), float, Char as interval values.
- basic C statements (assignment, while, for, switch, if, ... )
- interprocedural analysis with dynamic partitioning
- records and arrays analysis
- pointers analysis including indirect function call
- cryptographic protocols analysis using a new hybrid abstract semantics
- ...
- backward analysis (really need ??)
- improve protocols analysis
REFERENCES
- Andersen, L. O, "Program Analysis and Specialization for the {C} Programming Language" Phd thesis, DIKU, University of Copenhagen , 1994
- Bjarne Steensgaard , "Points-to analysis in almost linear time", Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 1996)
- Bruno Blanchet and Patrick Cousot and Radhia Cousot and Jérôme Feret and Laurent Mauborgne and Antoine Miné and David Monniaux and Xavier Rival "A Static Analyzer for Large Safety-Critical Software" ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 196--207, 2003, San Diego, California.
- Cousot, P. "The Calculational Design of a Generic Abstract Interpreter", Calculational System Design, NATO ASI IOS Press, M. Broy and R. Steinbruggen editor, 1999.
- Thomas Reps and Susan Horwitz and Mooly Sagiv, "Precise Interprocedural Dataflow Analysis via Graph Reachability", Conference Record of 22nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, San Francisco, California, 1995
- Maryam Emami and Rakesh Ghiya and Laurie J. Hendren, "Context-Sensitive Interprocedural Points-to Analysis in the Presence of Function Pointers", SIGPLAN Conference on Programming Language Design and Implementation, 1994
- Michael Hind "Pointer analysis: haven't we solved this problem yet?", Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, ACM Press, 2001
- Francois Bourdoncle, "Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity", Proceedings of the International Workshop PLILP'90, Springer- Verlag, LNCS 456, 1990
© Copyright Fabrice Parrennes, March 2004