Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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