Celina G. Val
Celina G. Val
@zhassan-aws Haven't you fixed this yet?
I do remember it being broken before we introduced `kani-driver`. @danielsn what do you think?
I tried adding `any_string` but I either bumped into really poor performance or linking issues. Hopefully we can get back to it once we fix the std lib linking.
As discussed offline, regarding the first topic, we will do the following: - [x] Deprecate `Invariant` trait and `impl Arbitrary for Invariant` for now (pending on @YoshikiTakashima potential use case)....
> Ok fixed the various comments from @danielsn > > That being said, after rereading my PR with a fresh post-weekend mind, I'm a bit unhappy with a Poison expression....
This problem seems to be related to many BuiltIn functions. Their C declaration doesn't always match their rust one. For example, `memcmp` in Rust takes `*const u8` while in C...
I changed Kani to insert the casts. I have another blocker with the std sockets library. I haven't had time to figure out what's wrong
I think this might be a name resolution issue. When the user crate invokes `libc::bind` we see the function signature and types as belonging to `libc`, however, when we are...
This might be related to https://github.com/model-checking/kani/issues/450
Note to self: refactor the logic here a bit and handle Variant separate from Type. In order to check the Variant, we need more information than provided here.