ssyram
ssyram
Currently, the `drop` statements in the translated LLBC are not working properly. Particularly: 1. It is often called for types like unit, i32 or so, which is dummy; 2. The...
As the title, support for float & double, namely, `Float32` and `Float64` are added to the `Constant.ml`. Relevant parts are fixed. This is required from the project [Eurydice](https://github.com/AeneasVerif/eurydice). Question left:...
The following codes: ```Rust struct Fields { a: i32, b: String, } fn use_box(b: Box) { let str = b.b; assert!(str.len() > 0); } fn main() { } ``` When...
The following codes: ```Rust fn main() { let _ = panic::catch_unwind(|| { }); } ``` Produces the following errors: ``` warning: found a built-in trait impl we did not recognize:...
> This PR is a re-submission of #871 , as @Sam-Ni does not have the permission of running the CI, I resubmit for him to view the CI results. This...
Now in file `charon-ml/src/NameMatcher.ml`, the function `ty_to_pattern_aux`, the conversion from `ty` to the pattern `expr` is *PARTIAL* and may lead to failure in Eurydice. Specifically, the problem is caused by...
This problem should be somehow related to #790 . **Code snippet to reproduce the bug**: I simplified the production, and simply have: ```Rust trait Internal { type IntAssoc; fn internal_method(&self)...
Thanks to the hard and quick work by @Nadrieril , now most parts of this PR have been merged into the main branch, with only two non-urgent parts: - The...
The following codes produce `Not_found` error in the `main` function when calls Charon with `--monomorphize`. This seems to be something to do with the NameMatcher mechanism. ```Rust trait SomeTrait {...
Now for quite some large crate (several hundred MB), Charon usually takes quite a long time to process (or simply when `generate-ml` in my Mac). This appears as a pure...