-
Notifications
You must be signed in to change notification settings - Fork 16
Open
Labels
bugSomething isn't workingSomething isn't working
Description
The following codes:
fn id(s: i32) -> i32 { s }
fn pipe<A, B, F: FnMut(A) -> B>(x: A, mut func: F) -> B { func(x) }
fn main() { assert!(pipe(10, id) > 0) }will produce the following errors:
ERROR translating test::main: Failure("Can't convert type to pattern: test::id")
After fixing that by ignoring the stuff (charon-ml/src/NameMatcher.ml:line 1040 to just EVar None), we will have:
ERROR translating test::main: Failure("Don't know how to resolve trait_ref above (2)")
If we ignore this error by ignoring the fn_ptr problem:
let expression_of_fn_ptr env (fn_ptr : C.fn_ptr) = expression_of_fn_ptr env "" fn_ptrby:
let expression_of_fn_ptr env (fn_ptr : C.fn_ptr) =
try expression_of_fn_ptr env "" fn_ptr
with e ->
Printf.eprintf "Error in expression_of_fn_ptr: %s with error: %s\n"
(Charon.PrintTypes.fn_ptr_to_string env.format_env fn_ptr)
(Printexc.to_string e);
if !Options.keep_going then begin
Printf.printf "Continuing with a placeholder expression...\n%!";
Krml.Helpers.any, false, TAny
end
else
raise eThen, we will reach the error:
Cannot re-check test.main as valid Low* and will not extract it. If test.main is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.
Warning 4: in the sequence statement at index 3, after the definition of uu____8, in top-level declaration test.main, in file test: Malformed input:
subtype mismatch:
int32_t (a.k.a. int32_t) vs:
int32_t -> int32_t* -> int32_t -> int32_t (a.k.a. int32_t -> int32_t* -> int32_t -> int32_t)
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working