Evaluation: GCC/Frama-C dataflow analysis for ownership annotations (owned/borrowed/moved/dropped)

[Fikoko]

Summary

Canon-C's ownership annotations (owned(), borrowed(), moved(), dropped())
are documentation-level markers in C99, with DEFINE_OWNED(T) / DEFINE_BORROWED(T)
covering the type-distinction case at API boundaries (see docs/design-decisions.md,
OWN-001..003). For everything the C99 type system cannot express, the README
currently defers to external static analyzers.

This issue tracks evaluating that claim empirically: can Frama-C (and GCC's
-fanalyzer) actually perform the dataflow analysis needed to enforce the
lowercase annotations?

Properties to evaluate

For each tool, determine whether it can detect:

• Use-after-move — reading a variable after it was passed to a
  moved() / consuming parameter
• Double-drop — passing the same pointer to a dropped() parameter twice
• Lifetime parameters across function calls — a borrowed() value
  outliving the region/arena it was stamped with
• Ownership flow through pointer aliases — tracking owned() semantics
  when the pointer is copied, cast, or stored in a struct

Candidate approaches

• Frama-C: mapping the lowercase annotations onto ACSL contracts
  (e.g. \valid, allocates/frees clauses, ghost state for move status);
  evaluate WP vs. EVA for which properties each can carry
• GCC -fanalyzer: whether __attribute__((malloc)), ownership attributes,
  or custom plugin work can encode drop/move semantics
• Optionally: whether the annotation macros should expand to tool-visible
  markers under a CANON_ANALYSIS build flag instead of expanding to nothing

Deliverables

• A test corpus of small programs, one per violation class (use-after-move,
  double-drop, stale borrow, aliased ownership), each in a "should flag" and
  "should pass" variant
• A results matrix: tool × property → detected / not detected / detected-with-annotations
• Documented recipe in docs/ for whichever combination works, or a recorded
  negative result in docs/design-decisions.md if neither tool can carry a property

Status

Future work — not scheduled.