Can ikos support comparison with vector?

[neon12345]

There is support for VectorType with translate_binary_operator for llvm::BinaryOperator but not for llvm::CmpInst.

Is it possible to transfer the vector handling from translate_binary_operator to translate_cmp and extend Type::is_unsigned_integer(), Type::is_signed_integer() for VectorType?

It seems to run this way but is it correct?

[arthaud]

Hi @neon12345,

I'm not working on ikos anymore, but just to answer your question: yes, it should be possible to support llvm::VectorType in llvm::CmpInst. Note that the analysis ignores all VectorType instructions anyway, while being sound (For instance, https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/include/ikos/analyzer/analysis/execution_engine/numerical.hpp#L1337)