0001
0002
0003
0004
0005
0006
0007
0008
0009
0010 awk 'BEGIN { num = -1; } # Ignore the beginning of the file
0011 /^#/ { next; }
0012 /^[ \t]*$/ { next; }
0013 /^START_TABLE/ { num = 0; next; }
0014 /^END_TABLE/ {
0015 if (num != $2) {
0016 printf "Error: NR_syscalls (%s) is not one more than the last syscall (%s)\n",
0017 $2, num - 1;
0018 exit(1);
0019 }
0020 num = -1; # Ignore the rest of the file
0021 }
0022 {
0023 if (num == -1) next;
0024 if (($1 != -1) && ($1 != num)) {
0025 printf "Error: Syscall %s out of order (expected %s)\n",
0026 $1, num;
0027 exit(1);
0028 };
0029 num++;
0030 }' "$1"