I clicked on 2 links on the main page in the Learn F* section...
49 karma · joined December 12, 2023
" one\n"
" two\n"
" three\n"The __LINE__ macro is passed to the debugger only if the program itself outputs its value, and the "debugger" is a human reading that output :)
The "\t" in "split" is not a "slash-tee" but an actual tab character and then escape sequences in fields are handled by the "unescape" function.
So this comparison will be unsigned and will allow to set `npins` to any value, even negative:
npins = MAX(npins, syscalls[i].sysno)
Then `SYS_kbind` seems to be a signed int. So this comparison will be signed and "fix" the negative `npins` to `SYS_kbind`: npins = MAX(npins, SYS_kbind)
And finally the `sysno` index might be out of bounds here: pins[syscalls[i].sysno] = syscalls[i].offset
But maybe I'm completely wrong, I'm not interested in researching it too much.