Lotus

User Guide

  • Major Components Overview
  • Architecture Overview
  • Quick Start Guide
  • Installation Guide
  • Tutorials and Examples
  • Bug Detection with Lotus
  • PDG Query Language (Cypher)
  • Property-Based Slicing
  • Verification Backend Abstraction
  • Instrumentation Passes
  • Troubleshooting and FAQ
  • Command-Line Tools

Core Components

  • Alias Analysis
  • Analysis Framework
  • Annotations
  • Applications
  • Context-Free Language Analysis
  • Data Flow Analysis
  • Intermediate Representations
    • ICFG — Interprocedural Control Flow Graph
    • Overview
    • Key Features
    • Components
    • Usage
    • Integration
    • PDG — Program Dependence Graph
    • Overview
    • Core Passes
    • Unified Query API
    • High-Level Usage
    • pdg-query Analysis Mode
    • SSI — Static Single Information
    • Overview
    • Key Features
    • SSI Formalism
    • Components
    • SSI Instructions
    • Algorithm
    • Usage
    • Integration
    • vSSA — Variable Static Single Assignment
    • Overview
    • Key Features
    • vSSA Instructions
    • Algorithm
    • Components
    • Usage
    • Integration with SRAA
    • Example
    • References
    • SVFG — Sparse Value-Flow Graph
    • Overview
    • Key Features
    • Node Types
    • Edge Types
    • Architecture
    • Usage
    • Integration
    • Components
    • References
    • GVFG
    • GSA — Gated SSA
    • Overview
    • Key Features
    • Core Types
    • Passes
    • Usage
    • Command-Line Options
    • Behavior Notes
    • MemorySSA — Memory Static Single Assignment
    • Overview
    • Key Features
    • Shadow Memory Instructions
    • Components
    • Usage
    • Integration
  • Overview
  • MemoryMLFeaturesPass
  • Features Extracted
  • Feature Output
  • Analysis Dependencies
  • Integration Notes
  • Related Components
  • Optimization
  • Solvers
  • Transforms
  • Utilities
  • Verification
  • Checker Framework

Developer Documentation

  • API Reference
  • Developer Guide
Lotus
  • Intermediate Representations
  • View page source

Intermediate Representations

This section covers the intermediate representations used in Lotus.

  • ICFG — Interprocedural Control Flow Graph
  • Overview
  • Key Features
  • Components
  • Usage
  • Integration
  • PDG — Program Dependence Graph
  • Overview
  • Core Passes
  • Unified Query API
  • High-Level Usage
  • pdg-query Analysis Mode
  • SSI — Static Single Information
  • Overview
  • Key Features
  • SSI Formalism
  • Components
  • SSI Instructions
  • Algorithm
  • Usage
  • Integration
  • vSSA — Variable Static Single Assignment
  • Overview
  • Key Features
  • vSSA Instructions
  • Algorithm
  • Components
  • Usage
  • Integration with SRAA
  • Example
  • References
  • SVFG — Sparse Value-Flow Graph
  • Overview
  • Key Features
  • Node Types
    • Statement Nodes (Top-Level Pointers)
    • PHI Nodes
    • Memory SSA Nodes (Address-Taken Variables)
    • Parameter Nodes
  • Edge Types
    • Intra-Procedural Edges
    • Inter-Procedural Edges
    • Thread Edges
  • Architecture
  • Usage
    • Basic Construction
    • Configuration
    • Querying Value Flows
    • Memory SSA Queries
    • Interprocedural Queries
    • On-the-Fly Call Graph Refinement
    • Type-Safe Node Casting
    • Serialization
  • Integration
    • AserPTA Integration
    • ICFG Integration
    • DDA Integration
  • Components
    • Core Files
    • Dependencies
  • References
  • GVFG
    • Overview
    • Main components
    • Use cases
    • See also
  • GSA — Gated SSA
  • Overview
  • Key Features
  • Core Types
  • Passes
  • Usage
  • Command-Line Options
  • Behavior Notes
  • MemorySSA — Memory Static Single Assignment
  • Overview
  • Key Features
  • Shadow Memory Instructions
  • Components
  • Usage
  • Integration
Previous Next

© Copyright 2024-2025, ZJU Programming Languages and Automated Reasoning Group.

Built with Sphinx using a theme provided by Read the Docs.