MCPcopy Create free account
hub / github.com/AliveToolkit/alive2 / load_bv

Function load_bv

ir/memory.cpp:197–205  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

195}
196
197static expr load_bv(const expr &var, const expr &idx0) {
198 auto bw = var.bits();
199 if (!bw)
200 return {};
201 if (var.isAllOnes())
202 return true;
203 auto idx = idx0.zextOrTrunc(bw);
204 return var.lshr(idx).extract(0, 0) == 1;
205}
206
207static void store_bv(Pointer &p, const expr &val, expr &local,
208 expr &non_local, bool assume_local = false,

Callers 1

isBlockAliveMethod · 0.85

Calls 5

isAllOnesMethod · 0.80
lshrMethod · 0.80
bitsMethod · 0.45
zextOrTruncMethod · 0.45
extractMethod · 0.45

Tested by

no test coverage detected