--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Values] patch to access the several states attached to a statement



> However, since the code was identical in Lithium and actually worked, I
> wasn't sure it was the proper way to fix this.

Oops. I was the culprit then.
There was a technical limitation in Lithium 
(or a limitation in my understanding, anyway)
such that it wasn't possible to insert a hook
only if a certain option was set. Instead,
what was easy to do was to systematically insert
a hook that only did something if the
option was set. It was slightly less elegant,
but it worked.

This was fixed in Beryllium, and a consequence
is that while in Lithium 
"Db.Value.Record_Value_Callbacks" always returned
"true" because there was a hook that was called
everytime and everytime tested if the
option "-calldeps" was set, now it works properly
and may return false.

Pascal