--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2009 ---
> 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