#!/bin/sh
# DF-4533 static proof: drm_open()'s success-path drm_minor_acquire() is
# never balanced on any live path.
#
# Exits 0 (PROVEN) when:
#  - drm_open() acquires a minor at entry and only releases it on the
#    err_undo FAILURE path (success keeps it — by design, the file owns it)
#  - drm_close() releases only the minor it acquires itself
#  - drm_release() is dead on DragonFly (returns before any release)
#  - drm_cdevpriv_dtor (the would-be balance) is never registered
set -e
cd "$(dirname "$0")/../../.."
[ -d sys/dev/drm ] || cd /home/maxx/dfbsd/dfbsd

echo "== every drm_minor_acquire / drm_minor_release site =="
grep -rn "drm_minor_acquire\|drm_minor_release" sys/dev/drm/*.c

echo
echo "== drm_open(): acquire at entry, release only under err_undo =="
sed -n '320,359p' sys/dev/drm/drm_file.c

echo
echo "== drm_release() dead on DragonFly =="
sed -n '595,605p' sys/dev/drm/drm_file.c

echo
echo "== drm_cdevpriv_dtor never registered (no devfs_set_cdevpriv caller) =="
if grep -rn "devfs_set_cdevpriv" sys/dev/drm/ ; then
	echo "FAIL: registered somewhere — recheck"; exit 1
else
	echo "(none: dtor dead)"
fi

echo
echo "PROVEN: open's acquire leaks; per open/close cycle net +1 dev kref."