GitLab

Note : the issue is still present later in Duplicateproof. This is
because I am examining an "identity ptree" which is way too big. I am
having a look to see if I could make this ptree less big - to not
include nodes that are identity

Merge branch 'master' of gricad-gitlab.univ-grenoble-alpes.fr:certicompil/compcert-kvx into kvx-work

There are now too many loads turned into non trap. To be investigated

Loops with multiple CBs were only partially predicted for some cases
(the header CB would get predicted, but not the CBs inside)

This would happen in the case of breaks leading to another loop, such
as:

```c
void lift_check_level()
{
  int i;
  int middle = lift_one_level >> 2;
  if ( lift_cntValid ) {

    for ( lift_level = 1; lift_level < 14; ++lift_level ) {
      if ( lift_cnt < lift_levelPos[lift_level] - middle )
        break; /* This break */
    }
  } else
    lift_level = 0;

  for ( i = 0; i < 14; ++i )
    lift_ctrl_io_led[i] = ( i == lift_level - 1 );
}
```

Various typos made the code fail silently for certain loops

It was too permissive

Outside of -interp mode, -main has no (known) effect but could be
confused for a linker option that sets the program's entrypoint, say.
It's safer to reject the option.

Inlined built-in functions destroy GPR0

Pflid destroys IR14
Inlined built-in functions destroy IR14