Code

Improve the check_generics pass#515

Code

Merged

Nadrieril merged 8 commits intoAeneasVerif:mainAeneasVerif/charon:mainfrom Nadrieril:generics-sourceNadrieril/charon:generics-sourceCopy head branch name to clipboardJan 6, 2025

+467-314

Commits

Commits on Jan 4, 2025

• Name matcher: Clearer support for patterns without generics

  Nadrieril

  committed
  d1547e4

  Copy full SHA for d1547e4

• Track the target of each GenericArgs

  Nadrieril

  committed
  a0c6bcb

  Copy full SHA for a0c6bcb

• Simplify check_generics

  Nadrieril

  committed
  135dccd

  Copy full SHA for 135dccd

• Run check_generics before transformation passes too

  Nadrieril

  committed
  17d754e

  Copy full SHA for 17d754e

Commits on Jan 5, 2025

• Run check_generics at the end even in ullbc mode

  Nadrieril

  committed
  e7230d3

  Copy full SHA for e7230d3

• Make CFG reconstruction and reorder_decls into passes

  Nadrieril

  committed
  c37224b

  Copy full SHA for c37224b

Commits on Jan 6, 2025

• Write test output on failure too

  Nadrieril

  committed
  b0b84d8

  Copy full SHA for b0b84d8

• Add context to check_generics errors

  Nadrieril

  committed
  52221b2

  Copy full SHA for 52221b2