#!/bin/sh
# DF-4460 run (see VERDICT.md for preconditions)
cd "$(dirname "$0")"
sh run.sh sys/dev/drm/drm_gem.c   (static proof of the committed-before-checked ordering)