Bug #716
closed
CPAchecker is not supported in master
Added by Pavel Shved almost 14 years ago.
Updated over 13 years ago.
Detected in build:
7394934
Description
The last version that supported CPAchecker was c47eb81. Version v0.2-rc2 (the latest stable one) supports it. However, parallel-friendly architecture doesn't support it (merged in 7394934), as the interface to RCV wrappers has changed, and I decided to debug it first on BLAST to transfer to CPAchecker's wrapper later.
Don't know if we should fix it now, I'd just rewrite the interface of RCV from scratch instead of making this bloat uglier.
To work correctly we should add our rule model's nondeterministic functions ldv_undefined_int, etc to CPAchecker configuration. Right now CPAchecker assumes that they are pure, so the result may not be as we expected. (See for example topic "Re: [CPAchecker Users: 77] Unsafe program reported as safe" at cpachecker mail list)
No problem, it is implemented in revision 2360. The name of the option is "cpas.symbpredabs.nondetFunctions". The default value is "int_nondet, malloc, nondet_int, random". If you specify it, the default functions are not included if you don't specify them explicitly.
Don't we want to make this simple fix to turn on CPAchecker again? It's said that we support at least 2 static verifiers!
Vadim, thus bug is not about these functions. Is there a bug for the issue you're talking about?
This is a separate issue. By the way it does not allow to use new envmodel seq_inf_ws with CPAchecker
Created a separate bug #1018 for nondetermined return value functions
- Priority changed from Normal to High
- Status changed from New to Open
No, the bug is still relevant. We should sort out that issue with nondetermined functions.
- Status changed from Open to Resolved
Ok, now CPAchecker as of Mar 16 15:46:52 is supported in master.
More recent CPAchecker versions have their parsers fixed, and can't process most of the Linux Driver Source code anymore. We should file the relevant bugs to the developers
Ok, the progress in undetermined functions and in integration of CPAchecker into cluster infrastructure is significant enough to close this one. If there are other issues, refer to bug #1018.
- Status changed from Resolved to Verified
Wow, Redmine doesn't let me close a bug if it has an open blocker! It's a nice feature, actually!
And this should be closed after #1018 closing.
- Status changed from Verified to Closed
As we're actively running CPAchecker in master, and it works, closing.
Also available in: Atom
PDF