AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
62 stars 15 forks source link

Make built-in functions less special #232

Open Nadrieril opened 3 weeks ago

Nadrieril commented 3 weeks ago

Today, built-in functions and place operations are represented as FunId::Assumed. Since they don't correspond to a normal FunDecl, consumers must know the correct type signature to use. We could instead declare a FunDecl with a special kind, so that users don't need to handle these builtins unless they care.