Hi,
On Thu, 29 Apr 2021 23:25:13 +0800 (CST) 董弈伯 <[email protected]> wrote: > Also, the output of Klee test is shown in different encoding > methods (like 0xffff.., char, int ,unsigned), does that mean it > didn't keep the type information? Tests are written in KLEE's .ktest file format and currently we do not store type information in there (basically just a name, length and a byte vector for each symbolic input). Hence, ktest-tool has to "guess" types and prints common ones. > It seems that KLEE treat pointer as a continuous memory > piece, which means KLEE does not "look into" the types of the > pointers? If so, why then? Not sure what you're asking exactly. KLEE just interprets LLVM and when a program needs to "look into" a type, it does so on the LLVM level. Let's take a simple example with a struct: https://godbolt.org/z/cPbKz9bo8 Here you can see how the values are stored and how KLEE would get the value for member "a" via getelementptr. [1] Kind regards, Frank [1] https://llvm.org/docs/LangRef.html#getelementptr-instruction _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
