safetylib/safetyAbsExpr.ml: Assertion failed

[jedisct1]

jasminc -checksafety hits the same assertion with these two files:

• https://github.com/jedisct1/aegis-jasmin/blob/master/src/aegis128l.jazz
• https://github.com/jedisct1/aegis-jasmin/blob/master/src/aegis256.jazz

Analyzing function _aegis256_encrypt
Fatal error: exception File "safetylib/safetyAbsExpr.ml", line 1010, characters 22-28: Assertion failed

  let mvar_of_lvar abs loc lv = match lv with
    | Lnone _ -> MLnone
    | Lmem _ -> MLnone
    | Lvar x  ->
      let ux = L.unloc x in
      begin match ux.v_kind, ux.v_ty with
 >>>    | Global,_ -> assert false (* this case should not be possible *)
        (* MLvar (Mglobal (ux.v_name,ux.v_ty)) *)
        | _, Bty _ -> MLvar (loc, Mlocal (Avar ux))
        | _, Arr _ -> MLvar (loc, Mlocal (Aarray ux)) end

[vbgl]

Thanks for your report. A possible workaround might be to move the global variables outside the scope of the functions.