4. Containment, review, and testing

Review unsafe code by invariant, not by line count. For every raw access, name who established address validity, size, alignment, initialization, aliasing, mutability, and lifetime. For every allocation, name the single cleanup owner and what happens on every earlier failure. For every native call, name the ABI source and supported targets.

Test the safe wrapper at zero, one, boundary, and invalid sizes; null and empty inputs; repeated calls; injected allocation failure where supported; and cleanup after partial progress. Run compiler sanitizers for the compiler itself and native sanitizers for C/C++ fixtures, while remembering that a passing sanitizer run is evidence, not a proof.

Keep the unsafe module private, expose typed operations, document the invariant next to the boundary, and require focused review for changes. If a later safe feature or library wrapper can express the operation, delete the unsafe path.

Tested example

Keep raw access inside two short blocks and verify the safe value before and after the boundary.

File: curriculum/main-evidence/single/unsafe_pointers.fl

// Build: build/flecha build examples/unsafe_pointers.fl -o build/unsafe_pointers
// Prints 42 and exits with 42. All pointers below refer to live local storage.

unsafe void write(constptr i32 destination, i32 value) {
    // The pointer binding is fixed; its target remains writable.
    *destination = value;
}

unsafe i32 read(*const i32 source) {
    // The target is read-only, including inside this unsafe function.
    return *source;
}

*i32 pass_pointer(*i32 pointer) {
    // Copying an address does not access its target and needs no unsafe block.
    return pointer;
}

i32 main() {
    i32 value = 0;
    *i32 pointer = none;
    if pointer != null { return 1; }

    unsafe {
        pointer = &raw value;
        write(pointer, 40);
        constptr i32 fixed = pointer;
        *fixed = *fixed + 2;

        // Read-only access may be added, but never removed implicitly.
        *const i32 readOnly = fixed;
        if read(readOnly) != 42 { return 2; }

        // Nested pointers preserve each layer's qualifiers.
        **i32 slot = &raw pointer;
        if **slot != 42 { return 3; }
    }

    pointer = pass_pointer(pointer);
    unsafe {
        // value still lives here. The unsafe block did not free anything.
        if *pointer != 42 { return 4; }
    }
    stdoutln(value);
    return value;
}

The block above is the complete file executed by the commands below.

The two raw accesses are short and surrounded by safe values that can be checked before and after the boundary. Expanding the raw region would make the same invariant apply to more code without adding capability.

Commands

flecha check curriculum/main-evidence/single/unsafe_pointers.fl
flecha build curriculum/main-evidence/single/unsafe_pointers.fl -o build/unsafe_pointers
build/unsafe_pointers

Expected output

42
exit status: 42

Related reference: /examples/unsafe_pointers/.

Curriculum complete

Use examples for complete applications and the reference documentation for precise contracts. Neither adds an accidental Next step to this learning sequence.