First, I'm a klee noob, so I apologize if this has been previously
answered; I did check the archives but it didn't seem like there was an
equivalent post.
We are trying to use klee for bounded test generation for some embedded
controller for a microwave that we generate from MATLAB embedded code.
The software runs as a cyclic task: there is a "step" function that runs
one execution step; in the embedded system, this will be called forever.
Each "step", new inputs are sampled and outputs are computed. In our
initial driver for klee, we executed a bounded loop of n-steps and
repeatedly initialized the inputs as symbolic and passed them to the
step function. This didn't seem to work, so we took the symbolic
initialization out of the loop, instead initializing an array:
pre-computing the set of inputs, if you will.
This seems to work, mostly, but we get some warnings from klee when we
run the code. They are variations on this:
KLEE: WARNING: unable to compute initial values (invalid constraints?)!
array KP_CLEAR[1] : w32 -> w8 = symbolic
array KP_START[1] : w32 -> w8 = symbolic
array KP_CLEAR_2[1] : w32 -> w8 = symbolic
array KP_START_1[1] : w32 -> w8 = symbolic
array KP_1[1] : w32 -> w8 = symbolic
array KP_CLEAR_3[1] : w32 -> w8 = symbolic
array DOOR_CLOSED_1[1] : w32 -> w8 = symbolic
array KP_CLEAR_1[1] : w32 -> w8 = symbolic
(query [(Eq false
(Eq 0 (Read w8 0 KP_1)))
(Eq 0 (Read w8 0 KP_CLEAR))
(Eq 0 (Read w8 0 KP_CLEAR_1))
(Eq false
(Eq 0 (Read w8 0 KP_START_1)))
(Eq 0 (Read w8 0 KP_START))
(Eq 0 (Read w8 0 DOOR_CLOSED_1))
(Eq 0 (Read w8 0 KP_CLEAR_2))
(Eq false
(Eq 0 (Read w8 0 KP_CLEAR_3)))]
false)
KLEE: WARNING: unable to get symbolic solution, losing test case
We don't understand these warnings, and when I google, I don't see much.
Could you help us out? The code for the example is in github under
https://github.com/jbiatek/microwave.
Thank you in advance!
Jason and Mike
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
