Bug #1018
closedUndefined functions should be listed in our config in CPAchecker frontend
0%
Description
Vadim says that we should add our model functions that return a nondetermined int to our config in CPAchecker's frontend. I haven't checked if it's the case, but here's what Vadim says:
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 Alexey Khoroshilov over 13 years ago
- Priority changed from Normal to High
Updated by Vadim Mutilin over 13 years ago
- Status changed from New to Resolved
- Published in build set to 60f0768a
Fixed in 60f0768a
The config file
dscv/rcv/cpachecker.config/cpa.cfg.pattern
now contains the nondeterministic functions
cpa.predicate.nondetFunctions = malloc, random, int_nondet, nondet_int, ldv_undefined_int, ldv_undefined_pointer, ldv_undefined_ulong
Updated by Pavel Shved over 13 years ago
Let's first analyze results of CPAchecker launch
Updated by Pavel Shved over 13 years ago
- Status changed from Resolved to Closed
Vadim says it doesn't appear anymore. Closing.