Hi Frank, Thanks a lot for the explanations.
Best Regards, Pansilu On Wed, Jul 7, 2021, 12:21 AM Frank Busse <[email protected]> wrote: > 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
