search

GaloisInc / crucible

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

`crux-mir`: Avoid pointer arithmetic in `vec::IntoIter` #1157

Closed qsctr closed 8 months ago

qsctr commented 9 months ago

We do the same thing as 69e92cb for vec::IntoIter.

Fixes #1144.

qsctr commented 9 months ago

@RyanGlScott Is there a place to put the test case? I saw there is crux-mir/test/symb_eval/alloc but the tests in there seem to be for allocate from the crucible crate and not the standard Rust alloc.

RyanGlScott commented 9 months ago

Thanks, @qsctr!

Is there a place to put the test case? I saw there is crux-mir/test/symb_eval/alloc but the tests in there seem to be for allocate from the crucible crate and not the standard Rust alloc.

Indeed, all of the test cases in the symb_eval subdirectly rely on symbolic branching in some way. The test case in https://github.com/GaloisInc/crucible/issues/1144#issuecomment-1833765009, however, is entirely concrete. For that reason, I'd favor placing the test case under crux-mir/tests/conc_eval. I'm not picky about which conc_eval subdirectory to use—something like conc_eval/vec should be fine.