• Cerberus
    About Cerberus
    Cerberus implementation-defined choices
    Supported C11 standard library functions
    C11 International Standard (N1570 draft)
    REMS
  • File
    General
    New empty file
    Load from file
    Examples library
    PNVI-* N2263 examples
    CAV 2019
    POPL 2019: pointer provenance
    C defacto standard
    GCC Tools Chauldron 2018
  • Model
    Memory model
    Concrete-allocation-address memory model
    Symbolic-allocation-address memory model (using Z3)
    VIP
    Provenance options
    Integer provenance (PVI)
    No integer provenance (PNVI)
    No integer provenance (PNVI-address-exposed)
    No integer provenance (PNVI-address-exposed user disambiguated)
    Further options
    Forbid (non-one-past) out-of-bounds pointer construction (strict_pointer_arith)
    Permissive out-of-bounds pointer construction (permissive_pointer_arith)
    Forbid uninitialised memory read (strict_reads)
    Forbid free null pointers (forbid_nullptr_free)
    Forbid use of pointers passed their lifetime (zap_dead_pointers)
    Equality operator depends only on the address value of pointers (strict_pointer_equality)
    Forbid use of relational operators for objects in different allocations (strict_pointer_relationals)
  • Views
    Elaboration
    C abstract syntax (Cabs)
    C abstract syntax, typed and desugared (Ail_AST)
    C abstract syntax, typed and desugared (Ail)
    Core
    Interactive execution
    Memory graph
    Memory table
    Core runtime arena
    Execution graph
    Stdout
    Stderr
  • Step: 0 Forward
  • Step: 0 Left
  • Middle
  • Right
  • Back
  • Restart
  • Search
    Random (45s timeout)
    Exhaustive (45s timeout)
  • Compile
  • Options
    Core optimisation
    Basic rewrites
    Sequentialise operations
    Interface options
    Colour elaboration expression
    Colour every elaboration expression
    Show string literals
    Show pointer bytes
    Order allocations by addresss
    Align allocations in a single column
    Suppress tau transitions
    Execution options
    Link with the C standard library
    Interactive execution options
    Step to the next tau transition
    Step to the next eval transition
    Step to the next memory action
    Step to the next C line