A tool that uses annotations to determine which code paths are taken.