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
Share
Long
Short