Bug #716
closedCPAchecker is not supported in master
0%
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.
Updated by Vadim Mutilin over 13 years ago
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.
Updated by Evgeny Novikov about 13 years ago
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!
Updated by Pavel Shved about 13 years ago
Vadim, thus bug is not about these functions. Is there a bug for the issue you're talking about?
Updated by Vadim Mutilin about 13 years ago
This is a separate issue. By the way it does not allow to use new envmodel seq_inf_ws with CPAchecker
Updated by Pavel Shved about 13 years ago
Created a separate bug #1018 for nondetermined return value functions
Updated by Alexey Khoroshilov about 13 years ago
- Priority changed from Normal to High
Updated by Pavel Shved about 13 years ago
- Status changed from New to Open
No, the bug is still relevant. We should sort out that issue with nondetermined functions.
Updated by Pavel Shved almost 13 years ago
- 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
Updated by Pavel Shved almost 13 years ago
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.
Updated by Pavel Shved almost 13 years ago
- Status changed from Resolved to Verified
Updated by Pavel Shved almost 13 years ago
Wow, Redmine doesn't let me close a bug if it has an open blocker! It's a nice feature, actually!
Updated by Evgeny Novikov almost 13 years ago
And this should be closed after #1018 closing.
Updated by Pavel Shved almost 13 years ago
- Status changed from Verified to Closed
As we're actively running CPAchecker in master, and it works, closing.