search

eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
773 stars 135 forks source link

added fseeko64 model (solve #16) #40

Closed borzacchiello closed 3 years ago

borzacchiello commented 3 years ago

Hi! I added the fseeko64 model. This solves #16 since objdump uses fseeko64 instead of fseek to rewind the input stream. Since SYMCC does not have the fseeko64 model, at some point a call to fread will increase the inputOffset beyond the input file dimension. This causes QSYM to generate a read expression with an index greater than the input size, leading to an overflow when it tries to generate a new testcase ( Solver::getConcreteValues https://github.com/eurecom-s3/qsym/blob/d17a39d40dc3ea1d17262dd52607f8a6527dde10/qsym/pintool/solver.cpp#L308 ).

sebastianpoeplau commented 3 years ago

Nice, good catch! And thanks for the implementation :)