search

GaloisInc / crucible

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

Implement byte-to-char casts for crucible-mir. #1191

Closed sauclovian-g closed 3 days ago

RyanGlScott commented 4 months ago

Thanks, @sauclovian-g! I can believe that this fixes the issue, but I would feel better if we added a regression test alongside it. Can you add this test case to crux-mir's test suite? I'm not too bothered about the exact location where we put the test—somewhere in test/conc_eval/num would work, for instance.

RyanGlScott commented 1 month ago

@sauclovian-g, do you plan on finishing this?

sauclovian-g commented 1 month ago

Yes, we need it for FV, just disorganized/behind on everything :-|

sauclovian-g commented 4 days ago

This should be ready to go now.

(I think I should rebase it on master before merging, and probably squash the two commits together too, but probably you should look at it first)

sauclovian-g commented 3 days ago

I rebased it on master and squashed the commits together. Since it's small and isolated this is pretty harmless, and it's been sitting around for a while.