let verifast_both
verifast
verifast -prover redux
in
dlsymtool MockKernelModule.dlsymspec
verifast_both -emit_dll_vfmanifest MockKernelModule_proxy.o contrib.o ghost_sets.o libraries.o lists.o sockets.o threading.o MockKernel.c
dlsymtool MockKernelModule.dlsymspec AdderModule
verifast_both -shared MockKernel.dll.vfmanifest AdderModule.c -export MockKernelModule_AdderModule.vfmanifest
del MockKernelModule_proxy.h
del MockKernelModule_proxy.c
del MockKernelModule_proxy.vfmanifest
del MockKernelModule_AdderModule.vfmanifest
del MockKernel.dll.vfmanifest