[klee-dev] .kteest & .kquery files

[Pansilu Pitigalaarachchi]

Hi Frank,

Thanks a lot for the explanations.

Best Regards,
Pansilu

On Wed, Jul 7, 2021, 12:21 AM Frank Busse <f.busse at imperial.ac.uk> wrote:

> Hi Pansilu,
>
>
> On Thu, 1 Jul 2021 17:12:05 +0800
> Pansilu Pitigalaarachchi <pansilu.pitigalaarachchi at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed