Xiao

Hi @HowToNamene, The current saber does not distinguish between true/false branches because of the solver (CUDD). We are replacing CUDD with Z3, and saber will support this feature in the...

Hi @acidghost , can you try this patch #1282 to check if it fixes your issue?

Hello @tianxinghe, Thanks for reporting this, and sorry for the late reply. Your observation is correct. The false positive is caused by the limitation of the SMT solver. We conservatively...

Hi @251 Thanks for reporting this. I will investigate this case. BTW, can you kindly send me a simplified bitcode or the bitcode for od_bloaty.c?

You may want to look into the graphtraits specification, e.g., https://github.com/SVF-tools/SVF/blob/master/svf/lib/Graphs/ICFG.cpp#L547.

I think this part is contributed by @sheisc.

Thanks for reporting. Should be fixed via PR #1443. Actually the type inference site for `%3` should be `%7 = getelementptr inbounds %struct.ll, ptr %6, i32 0, i32 0` because...

The bug is caused by trying connecting a direct value-flow from an integer to pointer (int2ptr instruction) when building a PTR only value flow graph. The source PAGNode (integer) does...

https://github.com/ives-nx/dwk_preprocess/tree/main/joern_slicer/joern

Thank you for your question. Here are the steps to use joern: 1. clone https://github.com/ives-nx/dwk_preprocess/tree/main/joern_slicer/joern 2. build joern to produce joern-parse 3. put the path to joern-parse in your local...