skip/enable assertions by a configuration file or by annotation

[bitcalc]

When I use SMACK to verify the memory safety of some programs, I found a much-needed feature. It is skipping certain functions but keeping the environment they set up.

My code has big initialization functions, which build some memory objects, and they are used by other functions. It takes a long time (over ten hours) to check all assertions in these initialization functions. I want to skip memory checking in those functions after running checks once.

In general, this feature allows a user to skip or enable certain verification goals easily by some criteria, such as by function name or file location, etc, by a configuration file or by special annotation as comments in the code.