Currently, the MIR backend lacks a way to extract a Rust function into a SAWScript Term. This would be useful in tandem with the prove and sat commands.
To do so, we should make MIR versions of the following, existing commands:
[ ] llvm_extract (which only allows scalar types)
[ ] llvm_compositional_extract (which also allows reference types).
Currently, the MIR backend lacks a way to extract a Rust function into a SAWScript
Term. This would be useful in tandem with theproveandsatcommands.To do so, we should make MIR versions of the following, existing commands:
llvm_extract(which only allows scalar types)llvm_compositional_extract(which also allows reference types).