Support extracting specific foreign items

[Nadrieril]

--extract-opaque-bodies extracts all the foreign definitions it can. It would be useful to be able to specify only specific ones. E.g. in Charon.toml:

[charon]
extract = [
  "trait core::convert::Into",
  "fn core::convert::{impl core::convert::Into<@U> for @T}::into",
]

This would extract the Into trait and the blanket From => Into implementation, which could be useful if the crate defines any From impls.

[msprotz]

FYI I tried this just now and I got this:

[Charon__GAstOfJson.type_decl_kind_of_json] failed on: `Assoc ([("Error",
          `String ("Unsupported type: foreign type: core::fmt::rt::{extern#0}::Opaque"))
          ])

to reproduce, add --extract-opaque-bodies to $(CHARON) in eurydice/Makefile, then run make test-where_clauses_closure.

[Nadrieril]

With https://github.com/AeneasVerif/charon/pull/316, charon --include "core::convert::{impl core::convert::Into<_> for _}::into" will translate precisely the requested method. This avoids the issue of --extract-opaque-bodies extracting too much.