You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This issue is meant to document improvements I think would be helpful after trying out assess in the wild:
Two new tables would be helpful:
Assess should classify failures to build/analyze packages #2058 - Presently you need to look through the log output, which is not hard, but it requires effort for something that should be easily summarizable. Further, I think it'd be cool if we can link known ones to open issues on our repo. :)
New unsupported features table for assess #1819 - The second half. We now see unsupported_construct get hit by tests, so we really need the unsupported features table to have columns for features actually hit by tests and sort according to that data.
The "successful tests" table could be aggregated by file. When I had a lot of results (600+ tests) ignoring the tests themselves and looking at the files containing any successful tests was most interesting. (Although longer term it might be more interesting based on coverage...)
Things to investigate:
The "Reason for failure" table contains entries that look like missing_definition and ioctl, which is odd. I'd expect one or the other, not both. This needs investigation, as it's probably a bug in how we parse CBMC properties results.
Might want to start tracking possible targets for "default stubs" that Kani (or assess) might ship with turned on by default. Started to see some interesting possibilities: clock_gettime, uname, rdtsc, getrlimit, sysconf, __libc_current_sigrtmin
I had to add a memory limit with ulimit -v, but I don't see crashed/killed verifier runs reported separately in that test failure table. I'm not sure what it's doing: skipping them possibly? I need to look into this.
There's a few things like --only-codegen we pass down through scan, but this list should be expanded. --all-features in particular is needed. -j--ignore-global-asm
This issue is meant to document improvements I think would be helpful after trying out assess in the wild:
Two new tables would be helpful:
unsupported_construct
get hit by tests, so we really need the unsupported features table to have columns for features actually hit by tests and sort according to that data.Things to investigate:
missing_definition
andioctl
, which is odd. I'd expect one or the other, not both. This needs investigation, as it's probably a bug in how we parse CBMC properties results.ulimit -v
, but I don't see crashed/killed verifier runs reported separately in that test failure table. I'm not sure what it's doing: skipping them possibly? I need to look into this.Problems:
assert!
macro #1597Nice-to-haves:
--only-codegen
we pass down through scan, but this list should be expanded.--all-features
in particular is needed.-j
--ignore-global-asm
Standing issues:
unwind(1)
: RFC: Resource limits for proof harnesses #1687The text was updated successfully, but these errors were encountered: