Table of Contents
- Introduction
- PART I - Using CiaoPP
- The CiaoPP high-level interface
- The CiaoPP low-level interface
- The CiaoPP command-line interface
- Available abstract domains
- aeq (library)
- def (library)
- deftypes: defined types (based on termsd) (abstract domain)
- depthk (library)
- eterms: types with lnewiden_el/4 (abstract domain)
- etermsvar: eterms with variables (abstract domain)
- frdef (library)
- fr_top (library)
- Simple groundness abstract domain
- lsign domain
- lsigndiff domain
- detplai (library)
- nfplai (library)
- Interval Domain
- PD domain
- PD domain with bottom
- polyhedra (library)
- ptypes: types with topological class widening (abstract domain)
- sharing+freeness (abstract domain)
- amgu-based sharing+freeness domain
- CLIQUE-Sharing+Freeness domain
- CLIQUE-Sharing+Freeness+Def domain
- sharing+freeness+nonvar (abstract domain)
- shareson (library)
- sharing (abstract domain)
- amgu-based sharing domain
- CLIQUE-Sharing domain
- 1-CLIQUE-Sharing domain
- CLIQUE-Sharing+Def domain
- shfret (library)
- amgu-based sharing+freeness+linearity domain
- shfrson (library)
- sondergaard (library)
- svterms: eterms + same value (abstract domain)
- termsd: types with shortening (abstract domain)
- top_path_sharing (library)
- Available program transformations
- Available fixpoints
- Other commands
- PART II - The Assertion Language and Its Use
- Using assertions for preprocessing programs
- The Ciao assertion language
- Types and properties related to assertions
- Declaring regular types
- Basic data types and properties
- Properties which are native to analyzers
- Properties related to sharing/aliasing, groundness
- Properties related to determinacy, failure, choice-points
- Properties related to cardinality and exact solutions
- Properties related to exceptions and signals
- Properties related to side effects
- Properties related to polyhedral constraints
- Properties related to data sizes, cost, termination
- Run-time checking of assertions
- Applying assertions during fixpoint
- PART III - Extending CiaoPP
- PART IV - CiaoPP Internals
- Frontend driver (monolithic)
- Analyze driver (monolithic)
- Transform driver (monolithic)
- Modular driver
- Database for intermodular analysis driver
- Intermodular analysis scheduler
- Program structure for intermodular analysis
- Intermodular entry policy
- Intermodular success policy
- Preprocessing Flags
- Debugging PLAI analyses
- Incremental analysis (high level)
- Incremental analysis (low level)
- Update plai_db after clause deletion (incremental analysis)
- Database for incremental analysis
- Persistent database for incremental analysis
- Incremental computation of tarjan algorithm
- Diff algorithm
- fixpo_dd (library)
- The Preprocessing Unit Component
- The Preprocessing Unit
- Preprocessing Unit Information Server
- native (library)
- program_keys (library)
- tr_syntax (library)
- The Global Information Server
- The Abstract Interpretation Component -PLAI
- PLAI- Abstract Interpretation-based Analysis
- Program Analysis (PLAI)
- fixpo_plai (library)
- Available type domains and widenings
- plai_db (library)
- Improving Analysis Using Trust Assertions
- Debugging the fixpoint operations
- Batch analysis client