Klee с STP против Klee с другим спутниковым решателем
Klee использует STP в качестве решателя ограничений, но теоретически можно изменить его решатель. STP не разрешает операции с плавающей запятой. Если мы решим заменить STP другим решателем ограничений, скажем, z3, сможет ли Klee генерировать ограничения с плавающей запятой?
Поток такой: C code -> llvm bitcode -> klee -> предложения stp -> klee -> output
Если klee получает инструкции с плавающей запятой llvm, сможет ли он их интерпретировать? Создает ли он ограничения fp на языке smt, что stp не может их обработать, или он вообще не генерирует ограничения fp?
Любая ссылка на ваш ответ будет принята с благодарностью.
1 ответ
Решение
Эта ссылка содержит форк KLEE с поддержкой плавающей запятой. Хотя понятия не имею, насколько он зрелый.