Supporting specifying command line options in C source file comments with SMACK-OPTIONS.