logoalt Hacker News

RossBencinalast Sunday at 12:13 AM1 replyview on HN

In general, symbolic execution will consider all code paths. If it can't (or doesn't want to) prove that the condition is always true or false it will check that the code is correct in two cases: (1) true branch taken, (2) false branch taken.


Replies

thealistralast Sunday at 11:05 PM

I understand how this works in general. I had static analyzers at Uni, I know lattice theory and all this - I am just wondering how Xr0 handles it.