search

ftsrg / gazer

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

Missing support for Rem expressions during Theta CFA generation #61

Open sallaigy opened 3 years ago

sallaigy commented 3 years ago

The expression transformer in tools/gazer-theta/lib/ThetaExpr.cpp does not handle Rem expressions, resulting in warnings and invalid Theta CFAs, e.g.:

Unhandled expr Int Rem(Int main/main/bb1165/a17.0_inlined0,71)
Unhandled expr Int Rem(Int main/main/bb1165/a17.0_inlined0,299872)
Unhandled expr Int Rem(Int Add(Int main/main/bb1165/a2.0_inlined0,252809),45)
[...]
Verification INTERNAL ERROR.
  Theta returned unrecognizable output. Raw output is:
Exception occurred, message: Could not parse CFA: Line 10006 col 48: Identifier '__UNHANDLED_EXPR__' cannot be resolved