☰
↑
←
→
🔍
TOC
The CiaoPP Program Processor
»
Table of Contents
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)
fd (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
Display information about CiaoPP files
CiaoPP batch processing
XML report for ciaopp-batch output
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
Adding a new analysis domain to CiaoPP
Plug-in points for abstract domains
PART IV - CiaoPP Internals
Frontend driver (monolithic)
Advanced output of preprocessor
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
Analysis 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
Fixpoint tracer
view_fixp (library)
Batch analysis client
ciaopp_master (application)
Worker for CiaoPP batch processing
Auxiliary predicates
Database for ciaopp_batch process
tasks_db (library)