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
771 stars 137 forks source link

Handle concrete Booleans in load/store #124

Closed sebastianpoeplau closed 1 year ago

sebastianpoeplau commented 1 year ago

The code introduced to fix eurecom-s3/symcc#112 can't handle concrete values (i.e., nullptr expressions). Detecting nullptr and skipping the symbolic computations in bitcode would have complicated the code of the pass and the generated IR a lot for an unclear benefit (basically just preventing the call to and immediate return from the runtime functions).