search

mc-imperial / gpuverify

GPUVerify: a Verifier for GPU Kernels
http://multicore.doc.ic.ac.uk/tools/GPUVerify/
Other
58 stars 15 forks source link

Add command line option to limit the number of verification errors reported #5

Closed delcypher closed 7 years ago

delcypher commented 9 years ago

I think this can be done with --boogie-opt=/errorLimit:1 but we should expose a command argument in GPUVerify script so it is more user visible.

jeroenk commented 9 years ago

This depends on the kind of errors you want to limit. The option would be different for clang. I don't know about opt. Bugle is limited to reporting just one error.

delcypher commented 9 years ago

Sorry I should of been a bit clearer. I meant reported verifications errors.

jeroenk commented 7 years ago

I've added a --error-limit option in commit 50013ab on the llvm-trunk branch. The error limit applies both to clang and Boogie. Unfortunately, there seems to be a bug in the version of Boogie we are using testing against testsuite/OpenCL/pointeranalysistests/manyprocedures/kernel.cl, with an error limit of 1, I get back two errors.