[klee-dev] .kteest & .kquery files

[Frank Busse]

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