Library topsy_hmFree_prg

Require Import ssreflect.
From mathcomp Require Import eqtype.
Require Import ZArith 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.
Local Open Scope Z_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 \- cst_e 2);
  While var_e entry \!= null \&& var_e entry \!= var_e addressEntry {{
     tmp <-* entry -.> next;
     entry <- var_e tmp
  }} ;
  If var_e entry \!= null Then
    tmp <-* entry -.> next;
    If var_e tmp \!= null Then
      entry -.> status *<- Free;
      result <- HM_FREEOK
    Else
      (result <- HM_FREEFAILED)
  Else
    result <- HM_FREEFAILED.