search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Requesting traces with floats results in a crash #62

Closed sallaigy closed 3 years ago

sallaigy commented 3 years ago

Consider the following program:

int b;
void __VERIFIER_error();
float a();
int main() {
    float c = a();
    b = c != c; // CHECK: b := 0
    if (!b)
        __VERIFIER_error();
}

Running it with gazer-bmc -trace results in a crash due to an unhandled expression in ExprEvaluator:

Iteration 1                                                                                                                                                                                                                                  
  Under-approximating.                                                                                                                                                                                                                       
    Transforming formula...                                                                                                                                                                                                                  
    Running solver...                                                                                                                                                                                                                        
      Elapsed time: 0 s                                                                                                                                                                                                                      
  Under-approximated formula is SAT.
Unhandled expression type in ExprEvaluatorBase
UNREACHABLE executed at /home/gyula/projects/gazer/src/Core/Expr/ExprEvaluator.cpp:48!