NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library pick_sign_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.

Definition pick_sign rx a0 a1 :=
  lw a0 zero16 rx ;
  while.ifte (expr_m.beq a0 r0)
   (addiu a1 r0 zero16)
   (srl a1 a0 (Z2u 5 31) ;
    while.ifte (expr_m.beq a1 r0)
     (addiu a1 r0 one16)
     (addiu a1 r0 mone16)).