--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on March 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about slicer



Hello,

> The program is of an interrupt
> driven device and each thread modifies a shared global variable
> ErrorStatus. So you can imagine many |= and &= type assignments to the
> variable from the threads and the some nested if tests. There is a main
> function with an infinite loop(i dont know whether that is significant
> for code slicing). My aim is to slice the threads and the main function
> giving me a reduced set of instructions that each thread performs on
> ErrorStatus. I get no output from attempting to slice the main loop so I
> added fake assignments such as ErrorStatus=someconstant to see how far
> it gets. It gets to a certain point in the main loop even under the
> infinite while loop but it stops just before one assignment.

Out of curiosity, what happens if you make it look as if the infinite
loop might terminate (such a transformed program has all the behaviors
of the original program and then some more, so this won't make any
code that should have been kept disappear)? Say, replacing

while(1)

with:

while(unknown_condition())

where no code is provided for the function unknown_condition().

Pascal