Library topsy_hmFree_prg

Require Import bipl.
Require Import expr_b_dp.
Require Import topsy_hm.

Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.

Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.

Definition HM_FREEFAILED := cst_e 0.
Definition HM_FREEOK := cst_e 1.

Definition hmFree (address : nat) (entry addressEntry tmp result : var.v) :=
  entry <- var_e hmStart ;
  addressEntry <- (nat_e address .-e cst_e 2);
  while.while (var_e entry <>e null &e var_e entry <>e var_e addressEntry) (
     tmp <-* entry -.> next ;
     entry <- var_e tmp
  );
  ifte (var_e entry <>e null ) thendo (
    tmp <-* entry -.> next ;
    ifte (var_e tmp <>e null ) thendo (
      entry -.> status *<- Free ;
      result <- HM_FREEOK )
    elsedo
      (result <- HM_FREEFAILED )
  ) elsedo (
     result <- HM_FREEFAILED
).