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

Crash when concrete non-undef structs contain floats #138

Closed sebastianpoeplau closed 1 year ago

sebastianpoeplau commented 1 year ago

The code that we introduced to fix #134 doesn't handle floats correctly; it crashes trying to bswap an expression of floating-point kind. We need to convert the expression to bit-vector kind before using it; the same is likely true for Booleans (just like in the symbolic handling of store, so let's reuse the function we introduced there).