search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
617 stars 42 forks source link

`crucible_mir`: Add overrides for `is_null` #1179

Closed RyanGlScott closed 4 months ago

RyanGlScott commented 5 months ago

It would be helpful to have crucible-mir overrides for the is_null family of functions. There is one such function for constant pointers, and another such function for mutable pointers, both of which have nearly identical implementations. The crucible-mir overrides themselves would be simple: just check if a reference is equal to MirIntegerToRef with a payload of 0, as that is how the overrides for ptr::null and ptr::null_mut work.

RyanGlScott commented 4 months ago

On second thought, I am mistaken: we already have special support for is_null as of https://github.com/GaloisInc/crucible/commit/93c803177ceb96a3af2240df4340b0b08b6d702e. (I mistakenly concluded that we didn't because I invoked crux-mir without first setting CRUX_RUST_LIBRARY_PATH.)