CT extraction: incorrect with "downto" for loops

[cassiersg]

Using the following test.jazz file:

export fn test(reg u32 x) -> reg u32 {
    inline int i;
    for i = 1 downto 0 {
        x = x + 1;
    }
    return x;
}

running the extraction as

jasminc -ec test -oec test.ec test.jazz
jasminc -ec test -CT -oec test_ct.ec test.jazz

gives for test.ec:

module M = {
  proc test (x:W32.t) : W32.t = {
    var aux: int;
    
    var i:int;
    
    i <- 1;
    while (0 < i) {
      x <- (x + (W32.of_int 1));
      i <- i - 1;
    }
    return (x);
  }
}.

while for test_ct.ec, the i initialization and bound are incorrect:

module M = {
  var leakages : leakages_t
  
  proc test (x:W32.t) : W32.t = {
    var aux: int;
    var aux_0: W32.t;
    
    var i:int;
    
    leakages <- LeakFor(0,1) :: LeakAddr([]) :: leakages;
    i <- 0;
    while (1 < i) {
      leakages <- LeakAddr([]) :: leakages;
      aux_0 <- (x + (W32.of_int 1));
      x <- aux_0;
      i <- i - 1;
    }
    return (x);
  }
}.