Files
BFM-decomp/phase-ends/current/logs/T2.c1.md
T

2.2 KiB

T2.c1 — kept-cast macro set in include/common.h

Change

  • include/common.h:62-78: inserted the brief's block (comment + CAST_ALIAS/SIGN/WIDTH/MISALIGNED/NONSTRUCT) between #define LOWU(x) and #include "gte_inline.h". M2C_FIELD, LOBU..LOWU untouched.

Timeline

  1. Edit common.h (Edit tool).
  2. Temporary respell of the 5 proof sites via .run/t2c1_respell.py (asserts each raw expr on its line, replaces first occurrence). Sites confirmed before edit:
    • src/ov_SC05_010/ov_SC05_010_jr_80180F84.c:3006 → CAST_ALIAS(u16, D_801C7E30, 0x34) = 0;
    • src/ov_SC01_000/ov_SC01_000_after.c:2682 → (s32)CAST_SIGN(s16, arg0, 0xF4)
    • src/ov_SC01_000/ov_SC01_000_jr_801734BC.c:2582 → first *(s16 *)(param_1 + 8) (the arg, not the *(s32 *) lvalue) → CAST_WIDTH(s16, param_1, 8)
    • src/ov_SC01_000/ov_SC01_000_jr_8012ACE0.c:2624 → CAST_MISALIGNED(int, param_1, 6)
    • src/ov_SC01_000/ov_SC01_000_jr_8012ACE0.c:795 → CAST_NONSTRUCT(s16, ((s32 *)arg0)[8], 0x1A) = 0x1000;
  3. bash tools/run.sh t2_proof_sc01 -- make check BINARY=ov_SC01_000 (.run/logs/t2_proof_sc01.log) → exit 0; CC lines present for _after.o, _jr_801734BC.o, _jr_8012ACE0.o: [ OK ] build/ov_SC01_000/ov_SC01_000 / sha1 9052dc0e4540db6d9c258c5e063e558c31867492 == config/check.ov_SC01_000.sha (BYTE-IDENTICAL)
  4. bash tools/run.sh t2_proof_sc05 -- make check BINARY=ov_SC05_010 (.run/logs/t2_proof_sc05.log) → exit 0; CC line present for _jr_80180F84.o: [ OK ] build/ov_SC05_010/ov_SC05_010 / sha1 9b5a70f97e6de537ddab83491c0b35ab137ddb2a == config/check.ov_SC05_010.sha (BYTE-IDENTICAL)
  5. git checkout -- the 4 src files (brief said three; sites span four files) → git status --short -- src empty.
  6. R22: bash tools/run.sh --bg t2_r22 -- bash -c 'make clean && make extract-all JOBS=16 && make check-all JOBS=16' + --wait t2_r22 --max 280 (.run/logs/t2_r22.log) → exit=0, check-all: 218 passed, 0 failed of 218.
  7. Commit include/common.h via commit_task.sh T2.c1.

Notes

  • harness: a bash command naming a >20k .c file in grep -c was denied by the whole-read guard; edits done by a scratch Python script instead.
  • Proofs per macro: SC01 proof covers SIGN, WIDTH, MISALIGNED, NONSTRUCT; SC05 covers ALIAS.