Closed RaitoBezarius closed 1 month ago
I'm not sure what you'd like charon to do differently here, isn't that just an issue of setting up cargo/rustc properly? You can indeed pass cargo and rustc flags to charon with --rustc-arg
and --cargo-arg
.
This is the bit I'm uncertain about, is there a way to tell rustc to extern crate std;
to a certain crate?
Another way to see this issue is to add a --features
flag but maybe you're right and we should just use --cargo-arg features=std
in those cases.
--cargo-arg
does work for features. If you want to add the extern crate std;
, you can pass --rustc-arg=--extern=std
I think. Or you can add it in your source under a feature gate
Thanks, I think this is all I needed. We can close this.
Code snippet:
Taking example from https://github.com/rust-lang/rfcs/issues/2505, ignoring the
unsafe
part, which is not relevant to this issue.Without
libm
, a call tosqrt
is not possible, but some libraries are offered inno_std
/std
variants, it may make sense to extract certain code with letting the user decide which level ofstd
is available?Current Charon output:
Not relevant as it fails earlier in the Rust compilation.
Extra context:
While
no_std
may be simpler, if certain functions are unavailable such assqrt
,ceil
,ln
, they need to be reimplemented vialibm
or LLVM intrinsics (which can translate to hardware optimized instructions or re-implement the function inline, see the RFC above), whether they are part of the extraction output should probably be a user choice.std
can be simpler also because it makes use of lessunsafe
or reuse more of the standard library which can already be verified and can be a simpler model of the code.Desired behavior: A knob to control
-Z build-std
or similar during Charon extraction? (--rustc-flag
could be enough but I'm not exactly sure.)