search

swtv-kaist / cs458-fall22

1 stars 0 forks source link

bv1 definition? #36

Open bltnynk opened 1 year ago

bltnynk commented 1 year ago

Dear professor. May I ask is about the definition of bv0 and bv1? I thought that bv1 is the bitvector with all 1 bits? According to the lecture slide, I find that:

image

But some online sources say that:

image

So may I ask if bv1 is not 111...111, then what is it?

Thank you!

moonzoo commented 1 year ago

bv0 in BitVec[32] is 0x 0000 0000

bv1 in BitVec[32] is 0x 0000 0001