Questions about uberXMHF's proof

1

Hi,

I try to verify my kernel with the same approach as uberXMHF. And I got some questions when reading its proof.
Much appreciated for any answers and suggestions!

In uberxmhf-6.1.0\uxmhf\xmhf-uobjs\geec_prime\gp_s1_scaniommu.c, in the

function, I got some questions to understand "//@assert xmhfhwm_cpu_gprs_esp == check_esp;" in the high level.

(1) The function <gp_s1_scaniommu> uses both C code and CASM code, and
the HW model (in uberspark-5.0\src\hwm) updates “xmhfhwm_cpu_gprs_esp”
in CASM code only. So there must be assumptions about the C code like
function stack frames are correctly initialized and finalized, right?
Otherwise, this assertion may not imply the property of the real ESP
register. Is my understanding correct?

(2) Functions like <impl_xmhfhwm*> in
uberspark-5.0\src\hwm\xmhfhwm_cpu.c do not have post-conditions. Then
how does Frama-C/WP verify “//@assert xmhfhwm_cpu_gprs_esp == check_esp;”?
I think Frama-C/WP only sees the properties of sub-functions, not the
body of these functions. So I tried a similar code with Frama-C/WP 24.0,
and the tool cannot verify it.

unsigned int ebx = 0;


void a()
{
     ebx = 1;
}

void b()
{
     ebx = 2;
}

int main()
{
     a();
     b();

     //@ assert ebx == 2;
}

(3) The code seems to compile <impl_xmhfhwm*> into binary after
expanding macros defined in xmhfhwm_cpu.h, is my understanding correct?
If so, is it OK to not compile these functions because they seem to be
function behavior specifications, not implementations?

Thanks a lot!