DESIGN RECORDS
The RFC library
Every major model decision has a written record: the problem, the proposed semantics, the tradeoffs, and the evidence required. These RFCs are the authoritative design references for WeaveC.
Accepted records specify the design. Implemented records have completed their defined implementation and test criteria. A status is not a guarantee about arbitrary C programs; consult each RFC’s scope and validation.
28 design records
- RFC 0001Ownership, borrowing and lifetimes for CAccepted
- RFC 0002Sound intra-procedural checkingImplemented
- RFC 0003Signature inferenceImplemented
- RFC 0004Unsafe boundaries: raw pointers, unsafe regions and indirect callsImplemented
- RFC 0005Whole-program analysis: cross-translation-unit summaries and the compiler driverImplemented
- RFC 0006Precision: non-lexical loans, condition facts, element places and outcome-conditional summariesAccepted
- RFC 0007Resource lifecycle: leaks, release families and owned fieldsAccepted
- RFC 0008Pointer validity: null dereferences, uninitialised pointers, invalid releases and replaced valuesAccepted
- RFC 0009Value-conditional behaviour: scalar facts, guarded effects and inferred noreturnAccepted
- RFC 0010Shared ownership: reference counts, ownership by outcome and per-outcome factsAccepted
- RFC 0011Spatial safety: derived pointers, extents and boundsAccepted
- RFC 0012Spatial safety II: strings, sized fields, offset relations and assumptionsAccepted
- RFC 0013Interprocedural heap state and value identityAccepted
- RFC 0014Pointer identity and precise call effectsImplemented
- RFC 0015Array elements, range operations, and container ownershipImplemented
- RFC 0016Compositional call checking under caller alias relationshipsImplemented
- RFC 0017C integer semantics and compositional spatial safetyImplemented
- RFC 0018Compositional safety contracts and checked codeAccepted
- RFC 0019Practical checked memory contracts for buffers and heap objectsImplemented
- RFC 0020Scalable modular checked analysisImplemented
- RFC 0021Practical C traversal and inductive buffer contractsImplemented
- RFC 0022Compositional checked interfaces for opaque pointers and callbacksImplemented
- RFC 0023Inductive ownership contracts for linked containersImplemented
- RFC 0024Checked C runtime contracts and variadic interfacesImplemented
- RFC 0025Case-sensitive checked contracts and discriminated C objectsImplemented
- RFC 0026Inferred relational contracts for growable buffers and vectorsImplemented
- RFC 0027Recursive object ownership and complete cleanup contractsImplemented
- RFC 0028Inferred contracts for opaque objects and private library stateImplemented
No matching records. Try a shorter title or choose all statuses.
Propose a change
Section titled “Propose a change”Read the RFC process for when a proposal is required, how to draft one, and how statuses change. For implementation evidence, see the validation records.