Hi Pansilu,
On Thu, 1 Jul 2021 17:12:05 +0800 Pansilu Pitigalaarachchi <[email protected]> wrote: > a.Below test cases have 3 objects. Can you help clarify the > significance & usage of the 2nd('stat') and 3rd('model_version') > objects. > b.What is the logic for the content of the 'stat' object & > 'model_version' objects? Hard coded ? > c.Is the stat object always 144 bytes and 'model version' 4 bytes ? > d.Some of the generated test cases in different experiments did not > contain 'stat' object, also some did not contain both 'stat' & > 'model_version' objects. You get "model_version" as soon as you use --posix-runtime (it's in the startup code klee_init_fds) and "A-data/A-data-stat" when you use symbolic files (144 bytes is the size of the stat struct on your system - KLEE uses symbolic entries for some values, not always the best choice). example.c: -- int main(void) {} -- $ klee example.bc - 0 objects in KTest file $ klee --posix-runtime example.bc - 1 object in KTest file (model_version) $ klee --posix-runtime example.bc --sym-files 1 1 - 3 objects in KTest file (model_version and the symbolic file A with its stat structure) > Are these optional ? Can I omit these objects altogether If I'm > generating custom .ktest files ? Depends on your use case. For symbolic files keep them. Kind regards, Frank _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
