Klever

In Klever 2.0 EMG puts generated models into separate C files that are not instrumented. Because of this, say, when models use kzalloc, this function definition calls kmalloc with a special flag for zeroing memory that is not known by verification backends. The particular example is the alloc_etherdev_mqs model, but likely there are other ones.