Hi Cristi, I submitted a patch for this to klee-commits... Waiting for Daniel to commit it.
-David ------Original Message------ From: Cristian Zamfir Sender: klee-dev-bounces at keeda.stanford.edu To: klee-dev at keeda.stanford.edu Subject: [klee-dev] support for X86_FP80TyID Sent: Mar 11, 2010 4:07 PM Hi, Currently, when testing the printf tool from coreutils, Klee will hit an assert in ConstantExpr::fromMemory because it does not handle X86_FP80TyID (80 bit float). Adding support for this seems like it requires quite a few changes: - adding support for the 80 bit float type in Expr.h - modifying the create and alloc functions in ConstantExpr to accept types with more than 64 bits. -fix other places in the code that may assume that a ConstantExpr is at most 64 bits wide (I am not sure yet if this will be required). I am currently implementing this and I was wondering if you know a better way to solve it. Did anyone else ran into this problem? Thanks, Cristi _______________________________________________ klee-dev mailing list klee-dev at keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev Sent via BlackBerry from T-Mobile
