diff --git a/nt/shvos.c b/nt/shvos.c
index 5e44bd6..4049d39 100644
--- a/nt/shvos.c
+++ b/nt/shvos.c
@@ -56,7 +56,7 @@ VOID
 __cdecl
 RtlRestoreContext (
     _In_ PCONTEXT ContextRecord,
-    _In_opt_ struct _EXCEPTION_RECORD * ExceptionRecord
+    _In_opt_ PEXCEPTION_RECORD ExceptionRecord
     );
 
 typedef struct _SHV_DPC_CONTEXT
@@ -70,14 +70,14 @@ typedef struct _SHV_DPC_CONTEXT
 
 VOID
 ShvVmxCleanup (
-    _In_ UINT16 Data,
-    _In_ UINT16 Teb
+    _In_ const UINT16 Data,
+    _In_ const UINT16 Teb
     );
 
 NTSTATUS
 FORCEINLINE
 ShvOsErrorToError (
-    INT32 Error
+    CONST INT32 Error
     )
 {
     //
@@ -109,12 +109,12 @@ ShvOsErrorToError (
 VOID
 ShvOsDpcRoutine (
     _In_ struct _KDPC *Dpc,
-    _In_opt_ PVOID DeferredContext,
-    _In_opt_ PVOID SystemArgument1,
-    _In_opt_ PVOID SystemArgument2
+    _In_ PVOID DeferredContext,
+    _In_ PVOID SystemArgument1,
+    _In_ PVOID SystemArgument2
     )
 {
-    PSHV_DPC_CONTEXT dpcContext = DeferredContext;
+    PSHV_DPC_CONTEXT const dpcContext = DeferredContext;
     UNREFERENCED_PARAMETER(Dpc);
 
     //
@@ -153,7 +153,7 @@ ShvOsDpcRoutine (
 
 VOID
 ShvOsPrepareProcessor (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     )
 {
     //
@@ -165,7 +165,7 @@ ShvOsPrepareProcessor (
 
 VOID
 ShvOsUnprepareProcessor (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     )
 {
     //
@@ -180,9 +180,12 @@ ShvOsUnprepareProcessor (
     __lidt(&VpData->SpecialRegisters.Idtr.Limit);
 }
 
+//
+// Is there supposed to be a size parameter?
+//
 VOID
 ShvOsFreeContiguousAlignedMemory (
-    _In_ PVOID BaseAddress
+    _In_ _Frees_ptr_ PVOID CONST BaseAddress
     )
 {
     //
@@ -191,9 +194,11 @@ ShvOsFreeContiguousAlignedMemory (
     MmFreeContiguousMemory(BaseAddress);
 }
 
+_Ret_maybenull_
+_When_(return != NULL, _Post_writable_byte_size_(Size))
 PVOID
 ShvOsAllocateContigousAlignedMemory (
-    _In_ SIZE_T Size
+    _In_ SIZE_T CONST Size
     )
 {
     PHYSICAL_ADDRESS lowest, highest;
@@ -218,19 +223,23 @@ ShvOsAllocateContigousAlignedMemory (
 
 ULONGLONG
 ShvOsGetPhysicalAddress (
-    _In_ PVOID BaseAddress
+    _In_ VOID *CONST BaseAddress
     )
 {
     //
     // Let the memory manager convert it
     //
+
+    //
+    // is MmGetPhysicalAddress incorrectly non-const?
+    //
     return MmGetPhysicalAddress(BaseAddress).QuadPart;
 }
 
 VOID
 ShvOsRunCallbackOnProcessors (
     _In_ PSHV_CPU_CALLBACK Routine,
-    _In_opt_ PVOID Context
+    _Inout_opt_ VOID *Context
     )
 {
     SHV_DPC_CONTEXT dpcContext;
@@ -247,18 +256,22 @@ DECLSPEC_NORETURN
 VOID
 __cdecl
 ShvOsRestoreContext (
-    _In_ PCONTEXT ContextRecord
+    _In_ PCONTEXT const ContextRecord
     )
 {
     //
     // Windows provides a nice OS function to do this
     //
+
+    //
+    // is RtlRestoreContext correctly non-const?
+    //
     RtlRestoreContext(ContextRecord, NULL);
 }
 
 VOID
 ShvOsCaptureContext (
-    _In_ PCONTEXT ContextRecord
+    _Out_ PCONTEXT ContextRecord
     )
 {
     //
@@ -267,6 +280,7 @@ ShvOsCaptureContext (
     RtlCaptureContext(ContextRecord);
 }
 
+_Ret_range_(>=, 0)
 INT32
 ShvOsGetCurrentProcessorNumber (
     VOID
@@ -278,6 +292,7 @@ ShvOsGetCurrentProcessorNumber (
     return (INT32)KeGetCurrentProcessorNumberEx(NULL);
 }
 
+_Ret_range_(>=, 0)
 INT32
 ShvOsGetActiveProcessorCount (
     VOID
@@ -291,7 +306,7 @@ ShvOsGetActiveProcessorCount (
 
 VOID
 ShvOsDebugPrint (
-    _In_ PCCH Format,
+    _In_z_ _Printf_format_string_ PCCH CONST Format,
     ...
     )
 {
@@ -305,6 +320,8 @@ ShvOsDebugPrint (
     va_end(arglist);
 }
 
+DRIVER_UNLOAD DriverUnload;
+
 VOID
 DriverUnload (
     _In_ PDRIVER_OBJECT DriverObject
@@ -318,6 +335,8 @@ DriverUnload (
     ShvUnload();
 }
 
+DRIVER_INITIALIZE DriverEntry;
+
 NTSTATUS
 DriverEntry (
     _In_ PDRIVER_OBJECT DriverObject,
diff --git a/ntint.h b/ntint.h
index 9fcb1d7..71d1843 100644
--- a/ntint.h
+++ b/ntint.h
@@ -36,6 +36,12 @@ Header Name:
 #define FALSE               0
 #endif
 
+#ifndef CONST
+#define CONST const
+#endif
+typedef char CHAR;
+typedef CONST CHAR *LPCCH, *PCCH;
+
 #define KERNEL_STACK_SIZE   24 * 1024
 
 typedef struct DECLSPEC_ALIGN(16) _M128A
diff --git a/shv.h b/shv.h
index 452c116..ca71f75 100644
--- a/shv.h
+++ b/shv.h
@@ -41,13 +41,14 @@ typedef struct _SHV_VP_STATE
     UINT16 ExitReason;
     UINT8 ExitVm;
 } SHV_VP_STATE, *PSHV_VP_STATE;
+typedef const SHV_VP_STATE *PCSHV_VP_STATE;
 
 typedef struct _SHV_CALLBACK_CONTEXT
 {
     UINT64 Cr3;
-    volatile long InitCount;
-    INT32 FailedCpu;
-    INT32 FailureStatus;
+    _Field_range_(>=, 0) volatile long InitCount;
+    _Field_range_(>=, -1) INT32 FailedCpu;
+    _Field_range_(SHV_STATUS_NOT_PRESENT, SHV_STATUS_SUCCESS) INT32 FailureStatus;
 } SHV_CALLBACK_CONTEXT, *PSHV_CALLBACK_CONTEXT;
 
 SHV_CPU_CALLBACK ShvVpLoadCallback;
@@ -60,22 +61,24 @@ ShvVmxEntry (
 
 INT32
 ShvVmxLaunchOnVp (
-    _In_ PSHV_VP_DATA VpData
+    _Inout_ PSHV_VP_DATA CONST VpData
     );
 
 VOID
 ShvUtilConvertGdtEntry (
-    _In_ VOID* GdtBase,
-    _In_ UINT16 Offset,
-    _Out_ PVMX_GDTENTRY64 VmxGdtEntry
+    _In_ VOID* CONST GdtBase,
+    _In_ CONST UINT16 Offset,
+    _Out_ PVMX_GDTENTRY64 CONST VmxGdtEntry
     );
 
 UINT32
 ShvUtilAdjustMsr (
-    _In_ LARGE_INTEGER ControlValue,
+    _In_ CONST LARGE_INTEGER ControlValue,
     _In_ UINT32 DesiredValue
     );
 
+_Ret_maybenull_
+_When_ (return != NULL, _Post_writable_size_(CpuCount))
 PSHV_VP_DATA
 ShvVpAllocateData (
     _In_ UINT32 CpuCount
@@ -83,7 +86,7 @@ ShvVpAllocateData (
 
 VOID
 ShvVpFreeData  (
-    _In_ PSHV_VP_DATA Data,
+    _In_ _Frees_ptr_ PSHV_VP_DATA Data,
     _In_ UINT32 CpuCount
     );
 
@@ -99,7 +102,7 @@ ShvVmxProbe (
 
 VOID
 ShvVmxEptInitialize (
-    _In_ PSHV_VP_DATA VpData
+    _Inout_ PSHV_VP_DATA CONST VpData
     );
 
 DECLSPEC_NORETURN
@@ -115,29 +118,31 @@ DECLSPEC_NORETURN
 VOID
 __cdecl
 ShvOsRestoreContext (
-    _In_ PCONTEXT ContextRecord
+    _In_ PCONTEXT const ContextRecord
     );
 
 VOID
 ShvOsCaptureContext (
-    _In_ PCONTEXT ContextRecord
+    _Out_ PCONTEXT ContextRecord
     );
 
 VOID
 ShvOsUnprepareProcessor (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     );
 
 INT32
 ShvOsPrepareProcessor (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     );
 
+_Ret_range_(>=, 0)
 INT32
 ShvOsGetActiveProcessorCount (
     VOID
     );
 
+_Ret_range_(>=, 0)
 INT32
 ShvOsGetCurrentProcessorNumber (
     VOID
@@ -145,10 +150,12 @@ ShvOsGetCurrentProcessorNumber (
 
 VOID
 ShvOsFreeContiguousAlignedMemory (
-    _In_ VOID* BaseAddress,
-    _In_ size_t Size
+    _In_ _Frees_ptr_ VOID* CONST BaseAddress,
+    _In_ CONST size_t Size
     );
 
+_Ret_maybenull_
+_When_ (return != NULL, _Post_writable_byte_size_ (Size))
 VOID*
 ShvOsAllocateContigousAlignedMemory (
     _In_ size_t Size
@@ -156,19 +163,19 @@ ShvOsAllocateContigousAlignedMemory (
 
 UINT64
 ShvOsGetPhysicalAddress (
-    _In_ VOID* BaseAddress
+    _In_ VOID *BaseAddress
     );
 
 #ifndef __BASE_H__
 VOID
 ShvOsDebugPrint (
-    _In_ const char* Format,
+    _In_z_ _Printf_format_string_ PCCH CONST Format,
     ...
     );
 #else
 VOID
 ShvOsDebugPrintWide (
-    _In_ const CHAR16* Format,
+    _In_z_ _Printf_format_string_ CONST CHAR16* CONST Format,
     ...
     );
 #define ShvOsDebugPrint(format, ...) ShvOsDebugPrintWide(_CRT_WIDE(format), __VA_ARGS__)
@@ -177,7 +184,7 @@ ShvOsDebugPrintWide (
 VOID
 ShvOsRunCallbackOnProcessors (
     _In_ PSHV_CPU_CALLBACK Routine,
-    _In_opt_ VOID* Context
+    _Inout_opt_ VOID* Context
     );
 
 extern PSHV_VP_DATA* ShvGlobalData;
diff --git a/shv_x.h b/shv_x.h
index 624b978..ba5e119 100644
--- a/shv_x.h
+++ b/shv_x.h
@@ -35,7 +35,7 @@ struct _SHV_CALLBACK_CONTEXT;
 typedef
 void
 SHV_CPU_CALLBACK (
-    struct _SHV_CALLBACK_CONTEXT* Context
+    _Inout_ struct _SHV_CALLBACK_CONTEXT* CONST Context
     );
 typedef SHV_CPU_CALLBACK *PSHV_CPU_CALLBACK;
 
@@ -52,6 +52,7 @@ typedef struct _SHV_SPECIAL_REGISTERS
     KDESCRIPTOR Idtr;
     KDESCRIPTOR Gdtr;
 } SHV_SPECIAL_REGISTERS, *PSHV_SPECIAL_REGISTERS;
+typedef CONST SHV_SPECIAL_REGISTERS *PCSHV_SPECIAL_REGISTERS;
 
 typedef struct _SHV_VP_DATA
 {
@@ -79,12 +80,13 @@ typedef struct _SHV_VP_DATA
     DECLSPEC_ALIGN(PAGE_SIZE) VMX_VMCS VmxOn;
     DECLSPEC_ALIGN(PAGE_SIZE) VMX_VMCS Vmcs;
 } SHV_VP_DATA, *PSHV_VP_DATA;
+typedef CONST SHV_VP_DATA *PCSHV_VP_DATA;
 
 C_ASSERT(sizeof(SHV_VP_DATA) == (KERNEL_STACK_SIZE + 5 * PAGE_SIZE));
 
 VOID
 _sldt (
-    _In_ UINT16* Ldtr
+    _Out_ UINT16* Ldtr
     );
 
 VOID
@@ -94,12 +96,12 @@ _ltr (
 
 VOID
 _str (
-    _In_ UINT16* Tr
+    _Out_ UINT16* CONST Tr
     );
 
 VOID
 __lgdt (
-    _In_ VOID* Gdtr
+    _In_ CONST VOID* Gdtr
     );
 
 INT32
diff --git a/shvutil.c b/shvutil.c
index d64a307..7d17896 100644
--- a/shvutil.c
+++ b/shvutil.c
@@ -24,12 +24,12 @@ Module Name:
 
 VOID
 ShvUtilConvertGdtEntry (
-    _In_ VOID* GdtBase,
-    _In_ UINT16 Selector,
-    _Out_ PVMX_GDTENTRY64 VmxGdtEntry
+    _In_ VOID* CONST GdtBase,
+    _In_ CONST UINT16 Selector,
+    _Out_ PVMX_GDTENTRY64 CONST VmxGdtEntry
     )
 {
-    PKGDTENTRY64 gdtEntry;
+    PCKGDTENTRY64 gdtEntry;
 
     //
     // Reject LDT or NULL entries
@@ -90,7 +90,7 @@ ShvUtilConvertGdtEntry (
 
 UINT32
 ShvUtilAdjustMsr (
-    _In_ LARGE_INTEGER ControlValue,
+    _In_ CONST LARGE_INTEGER ControlValue,
     _In_ UINT32 DesiredValue
     )
 {
diff --git a/shvvmx.c b/shvvmx.c
index f4f39b9..08b9729 100644
--- a/shvvmx.c
+++ b/shvvmx.c
@@ -24,7 +24,7 @@ Module Name:
 
 VOID
 ShvVmxEptInitialize (
-    _In_ PSHV_VP_DATA VpData
+    _Inout_ PSHV_VP_DATA CONST VpData
     )
 {
     UINT64 i;
@@ -55,10 +55,10 @@ ShvVmxEptInitialize (
 
 UINT8
 ShvVmxEnterRootModeOnVp (
-    _In_ PSHV_VP_DATA VpData
+    _Inout_ PSHV_VP_DATA CONST VpData
     )
 {
-    PSHV_SPECIAL_REGISTERS Registers = &VpData->SpecialRegisters;
+    PSHV_SPECIAL_REGISTERS CONST Registers = &VpData->SpecialRegisters;
 
     //
     // Ensure the the VMCS can fit into a single page
@@ -161,13 +161,12 @@ ShvVmxEnterRootModeOnVp (
 
 VOID
 ShvVmxSetupVmcsForVp (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     )
 {
-    PSHV_SPECIAL_REGISTERS state = &VpData->SpecialRegisters;
-    PCONTEXT context = &VpData->ContextFrame;
+    PCSHV_SPECIAL_REGISTERS CONST state = &VpData->SpecialRegisters;
+    CONST CONTEXT *CONST context = &VpData->ContextFrame;
     VMX_GDTENTRY64 vmxGdtEntry;
-    VMX_EPTP vmxEptp;
 
     //
     // Begin by setting the link pointer to the required value for 4KB VMCS.
@@ -182,6 +181,7 @@ ShvVmxSetupVmcsForVp (
         //
         // Configure the EPTP
         //
+        VMX_EPTP vmxEptp;
         vmxEptp.AsUlonglong = 0;
         vmxEptp.PageWalkLength = 3;
         vmxEptp.Type = MTRR_TYPE_WB;
@@ -444,7 +444,7 @@ ShvVmxProbe (
 
 INT32
 ShvVmxLaunchOnVp (
-    _In_ PSHV_VP_DATA VpData
+    _Inout_ PSHV_VP_DATA CONST VpData
     )
 {
     UINT32 i;
diff --git a/shvvmxhv.c b/shvvmxhv.c
index 310f378..d120c56 100644
--- a/shvvmxhv.c
+++ b/shvvmxhv.c
@@ -41,7 +41,7 @@ ShvVmxResume (
 uintptr_t
 FORCEINLINE
 ShvVmxRead (
-    _In_ UINT32 VmcsFieldId
+    _In_ _In_range_(VIRTUAL_PROCESSOR_ID, HOST_RIP) _Notliteral_ CONST UINT32 VmcsFieldId
     )
 {
     size_t FieldData;
@@ -96,7 +96,7 @@ ShvVmxHandleInvd (
 
 VOID
 ShvVmxHandleCpuid (
-    _In_ PSHV_VP_STATE VpState
+    _Inout_ PSHV_VP_STATE CONST VpState
     )
 {
     INT32 cpu_info[4];
@@ -151,7 +151,7 @@ ShvVmxHandleCpuid (
 
 VOID
 ShvVmxHandleXsetbv (
-    _In_ PSHV_VP_STATE VpState
+    _In_ PCSHV_VP_STATE CONST VpState
     )
 {
     //
@@ -165,7 +165,7 @@ ShvVmxHandleXsetbv (
 
 VOID
 ShvVmxHandleVmx (
-    _In_ PSHV_VP_STATE VpState
+    _Inout_ PSHV_VP_STATE CONST VpState
     )
 {
     //
@@ -181,7 +181,7 @@ ShvVmxHandleVmx (
 
 VOID
 ShvVmxHandleExit (
-    _In_ PSHV_VP_STATE VpState
+    _Inout_ PSHV_VP_STATE CONST VpState
     )
 {
     //
@@ -230,11 +230,11 @@ ShvVmxHandleExit (
 DECLSPEC_NORETURN
 VOID
 ShvVmxEntryHandler (
-    _In_ PCONTEXT Context
+    _Inout_ PCONTEXT CONST Context
     )
 {
     SHV_VP_STATE guestContext;
-    PSHV_VP_DATA vpData;
+    PCSHV_VP_DATA vpData;
 
     //
     // Because we had to use RCX when calling ShvOsCaptureContext, its value
@@ -246,7 +246,7 @@ ShvVmxEntryHandler (
     //
     // Get the per-VP data for this processor.
     //
-    vpData = (VOID*)((uintptr_t)(Context + 1) - KERNEL_STACK_SIZE);
+    vpData = (CONST VOID*)((uintptr_t)(Context + 1) - KERNEL_STACK_SIZE);
 
     //
     // Build a little stack context to make it easier to keep track of certain
diff --git a/shvvp.c b/shvvp.c
index 1b34069..8b7b3af 100644
--- a/shvvp.c
+++ b/shvvp.c
@@ -57,7 +57,7 @@ ShvIsOurHypervisorPresent (
 
 VOID
 ShvCaptureSpecialRegisters (
-    _In_ PSHV_SPECIAL_REGISTERS SpecialRegisters
+    _Out_ PSHV_SPECIAL_REGISTERS CONST SpecialRegisters
     )
 {
     //
@@ -109,9 +109,10 @@ ShvVpRestoreAfterLaunch (
     ShvOsRestoreContext(&vpData->ContextFrame);
 }
 
+_Success_(return == SHV_STATUS_SUCCESS)
 INT32
 ShvVpInitialize (
-    _In_ PSHV_VP_DATA Data
+    _Inout_ PSHV_VP_DATA CONST Data
     )
 {
     INT32 status;
@@ -146,6 +147,10 @@ ShvVpInitialize (
         // If the AC bit is not set in EFLAGS, it means that we have not yet
         // launched the VM. Attempt to initialize VMX on this processor.
         //
+
+        //
+        // NOTE: why isn't status checked?
+        //
         status = ShvVmxLaunchOnVp(Data);
     }
 
@@ -157,7 +162,7 @@ ShvVpInitialize (
 
 VOID
 ShvVpUnloadCallback (
-    _In_ PSHV_CALLBACK_CONTEXT Context
+    _Inout_ PSHV_CALLBACK_CONTEXT CONST Context
     )
 {
     INT32 cpuInfo[4];
@@ -182,6 +187,8 @@ ShvVpUnloadCallback (
     }
 }
 
+_Ret_maybenull_
+_When_ (return != NULL, _Post_writable_size_(CpuCount))
 PSHV_VP_DATA
 ShvVpAllocateData (
     _In_ UINT32 CpuCount
@@ -209,7 +216,7 @@ ShvVpAllocateData (
 
 VOID
 ShvVpFreeData (
-    _In_ PSHV_VP_DATA Data,
+    _In_ _Frees_ptr_ PSHV_VP_DATA Data,
     _In_ UINT32 CpuCount
     )
 {
@@ -221,7 +228,7 @@ ShvVpFreeData (
 
 VOID
 ShvVpLoadCallback (
-    _In_ PSHV_CALLBACK_CONTEXT Context
+    _Inout_ PSHV_CALLBACK_CONTEXT CONST Context
     )
 {
     PSHV_VP_DATA vpData;
@@ -283,7 +290,7 @@ ShvVpLoadCallback (
     //
     // This CPU is hyperjacked!
     //
-    _InterlockedIncrement((volatile long*)&Context->InitCount);
+    _InterlockedIncrement(&Context->InitCount);
     return;
 
 Failure:
diff --git a/uefi/shvos.c b/uefi/shvos.c
index db19f21..0f326e7 100644
--- a/uefi/shvos.c
+++ b/uefi/shvos.c
@@ -75,7 +75,7 @@ EFI_MP_SERVICES_PROTOCOL* _gPiMpService;
 EFI_STATUS
 __forceinline
 ShvOsErrorToError (
-    INT32 Error
+    CONST INT32 Error
     )
 {
     //
@@ -106,7 +106,7 @@ ShvOsErrorToError (
 
 VOID
 _str (
-    _In_ UINT16* Tr
+    _Out_ UINT16* Tr
     )
 {
     //
@@ -117,7 +117,7 @@ _str (
 
 VOID
 _sldt (
-    _In_ UINT16* Ldtr
+    _Out_ UINT16* Ldtr
     )
 {
     //
@@ -128,7 +128,7 @@ _sldt (
 
 VOID
 __lgdt (
-    _In_ IA32_DESCRIPTOR* Gdtr
+    _In_ CONST IA32_DESCRIPTOR* Gdtr
     )
 {
     //
@@ -139,7 +139,7 @@ __lgdt (
 
 VOID
 ShvOsUnprepareProcessor (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     )
 {
     UNREFERENCED_PARAMETER(VpData);
@@ -151,7 +151,7 @@ ShvOsUnprepareProcessor (
 
 INT32
 ShvOsPrepareProcessor (
-    _In_ PSHV_VP_DATA VpData
+    _In_ PCSHV_VP_DATA CONST VpData
     )
 {
     PKGDTENTRY64 TssEntry, NewGdt;
@@ -228,13 +228,13 @@ ShvOsPrepareProcessor (
 VOID
 ShvOsRunCallbackOnProcessors (
     _In_ PSHV_CPU_CALLBACK Routine,
-    _In_ VOID* Context
+    _Inout_opt_ VOID *Context
     )
 {
     //
     // Call the routine on the current CPU
     //
-    Routine(Context);
+    (*Routine)(Context);
 
     //
     // And then on all other processors
@@ -250,8 +250,8 @@ ShvOsRunCallbackOnProcessors (
 
 VOID
 ShvOsFreeContiguousAlignedMemory (
-    _In_ VOID* BaseAddress,
-    _In_ size_t Size
+    _In_ _Frees_ptr_ VOID* CONST BaseAddress,
+    _In_ CONST size_t Size
     )
 {
     //
@@ -260,9 +260,11 @@ ShvOsFreeContiguousAlignedMemory (
     FreeAlignedPages(BaseAddress, Size);
 }
 
+_Ret_maybenull_
+_When_(return != NULL, _Post_writable_byte_size_(Size))
 VOID*
 ShvOsAllocateContigousAlignedMemory (
-    _In_ size_t Size
+    _In_ CONST size_t Size
     )
 {
     //
@@ -273,7 +275,7 @@ ShvOsAllocateContigousAlignedMemory (
 
 UINT64
 ShvOsGetPhysicalAddress (
-    _In_ VOID* BaseAddress
+    _In_ VOID *BaseAddress
     )
 {
     //
@@ -332,7 +334,7 @@ ShvOsGetActiveProcessorCount (
 
 VOID
 ShvOsDebugPrintWide (
-    _In_ CHAR16* Format,
+    _In_z_ _Printf_format_string_ CONST CHAR16* CONST Format,
     ...
     )
 {
diff --git a/vmx.h b/vmx.h
index a3c2371..64a5b16 100644
--- a/vmx.h
+++ b/vmx.h
@@ -82,6 +82,7 @@ typedef union _KGDTENTRY64
         INT64 DataHigh;
     };
 } KGDTENTRY64, *PKGDTENTRY64;
+typedef const KGDTENTRY64* PCKGDTENTRY64;
 
 #pragma pack(push,4)
 typedef struct _KTSS64