SMV-AV: Redefining NT_VERIFY and procedure replication

[shuvendu-lahiri]

The LI generation creates two copies of a procedure invoked within NT_VERIFY (entrypoint BdpReserveScratchVa). See email titled "Understanding the BPL" on 3/31/2017. Some context below

You can see there are two calls to BlMmFreeVirualPages (on blocks D_24 and D_30). You can also see a self loop on D_29, which I believe is SMV’s way of encoding an “assume false”. This is definitely the case that SDV (before slam.exe is run) is redefining NT_VERIFY to something else and we need to change this. But I cannot figure out where this happens. It must be in slamcl, I would guess...