Formalised Execution

• More rules:

  • i=jmp l; H(l)=code I'
  • i=cmp r1,r2; R'=R{cc:=cmp(R(v1),R(v2))}
  • i=jcc l; cc true; h(l)=code I'
  • i=jcc l; cc false; I'=I

Previous slide

Next slide

Back to first slide

View graphic version