1 files changed, 20 insertions, 0 deletions
diff --git a/scripts/check_size b/scripts/check_size
new file mode 100755
index 0000000000..54f02a63c5
--- /dev/null
+++ b/scripts/check_size
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+symbol="$1"
+file="$2"
+max="$3"
+
+# extract symbol offset from file, remove leading zeros
+ofs=$(nm -t d $file | grep "$symbol" | cut -d ' ' -f1 | sed "s/^[0]*//")
+
+if [ -z "${ofs}" ]; then
+	echo "symbol $symbol not found in $file"
+	exit 1
+fi
+
+if [[ $ofs -gt $max ]]; then
+	echo "symbol $symbol (offset $ofs) in $file exceeds maximum offset $max"
+	exit 1
+fi
+
+exit 0