Slides of a famous random test+symbolic execution software test tool issue



  • I am reading the slides of a famous random test+symbolic execution software test tool cute's slides. In one slide, I see this claim on classic symbolic execution: So my question is : Why author claims that "Symbolic execution will say both branches are reachable"? From my understanding, symbolic execution needs to solve the constrains of branch conditions, and basically if((x%10)*4!=17) { }else{ } else statement's constrain can not be solved, am I right? Could anyone give me some help? Thank you!



  • The symbolic solver in the slide cannot deduce that an integer multiplied by 4 cannot be 17. This is a statement about that particular solver at that point in time, not about solvers in general.



Suggested Topics

  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2