anchor.diff:        // structure.
         EUnit
   
  +   (*
  +    * AR: TODO: FIXME:
  +    *     temporarily extraction of new_drgn and free_drgn is same just unit
  +    *)
  +  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ _rid ])
  +    when (string_of_mlpath p = "FStar.HyperStack.ST.free_drgn") ||
  +         (string_of_mlpath p = "FStar.HyperStack.ST.new_drgn") ->
  +      EUnit
  +
     | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _ebuf; _eseq ])
       when (string_of_mlpath p = "LowStar.Monotonic.Buffer.witness_p" ||
             string_of_mlpath p = "LowStar.Monotonic.Buffer.recall_p" ||
  
positive.code:          string_of_mlpath p = "LowStar.ImmutableBuffer.igcmalloc_of_list" ->
        EBufCreateL (Eternal, List.map (translate_expr env) (list_elements e2))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ _rid; init ])
      when (string_of_mlpath p = "FStar.HyperStack.ST.ralloc") ->
        EBufCreate (Eternal, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _e0; e1; e2 ])
  
negative.code:     when string_of_mlpath p = "LowStar.UninitializedBuffer.ugcmalloc" ->
        EBufCreateNoInit (Eternal, translate_expr env elen)
  
     (*
      * AR: TODO: FIXME:
      *     temporarily extraction of ralloc_drgn_mm is same as ralloc_mm
      *)
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ _rid; init ])
      when (string_of_mlpath p = "FStar.HyperStack.ST.ralloc_mm") ||
           (string_of_mlpath p = "FStar.HyperStack.ST.ralloc_drgn_mm") ->
        EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _e0; e1; e2 ])
  