C: False positive about "Potential double free" with negative array indices

Description of the false positive

CodeQL warns about potential double free, in situations where there's clearly no such situation. It seems to be related to the use of negative indices

Code samples or links to source code

Cf https://github.com/MapServer/MapServer/security/code-scanning/3

The code at https://github.com/MapServer/MapServer/blob/0cb56232d4ca0e64d747efa1db602ff08e0ea42f/src/mapparser.c#L1787 (which is C code generated from a Bison grammar)

    free((yyvsp[-2].strval));
    free((yyvsp[0].strval));

generates "Memory pointed to by may already have been freed by. ", but this is obviously wrong as the memory locations are disjoint.

Extract of "Show path" in the report:

Step 1 pointer to free output argument
Source
src/mapparser.c:1787
      }
    }

    free((yyvsp[-2].strval));
    free((yyvsp[0].strval));
  }
#line 1791 "/vagrant/mapparser.c" /* yacc.c:1646  */
Step 2 *access to array [post update] [YYSTYPE]
src/mapparser.c:1787
      }
    }

    free((yyvsp[-2].strval));
    free((yyvsp[0].strval));
  }
#line 1791 "/vagrant/mapparser.c" /* yacc.c:1646  */
Step 3 *access to array [YYSTYPE]
src/mapparser.c:1788
    }

    free((yyvsp[-2].strval));
    free((yyvsp[0].strval));
  }
#line 1791 "/vagrant/mapparser.c" /* yacc.c:1646  */
    break;
Step 4 strval
Sink
src/mapparser.c:1788
    }

    free((yyvsp[-2].strval));
    free((yyvsp[0].strval));
Memory pointed to by
may already have been freed by
.
  }
#line 1791 "/vagrant/mapparser.c" /* yacc.c:1646  */
    break;

github / codeql

C: False positive about "Potential double free" with negative array indices #16643