search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Reporting LLVM function coverage #643

Open brianhuffman opened 4 years ago

brianhuffman commented 4 years ago

It would be useful to be able to have saw generate a summary of which C/LLVM functions have been verified by a crucible_llvm_verify command, or an entire proof script. We should ask crucible to keep track of which C/LLVM function definitions are traversed during symbolic simulation, and store a summary somewhere. Then maybe we could have another saw command to print out the summary or write it to a file.

brianhuffman commented 3 years ago

@atomb, does #767 take care of this issue, or is there something else left to do?