Linux Driver Verification

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.