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] The Capabilities of Frama-C

>By the way, aren't Binary Decision Diagrams used in Frama-C?

It is natural to think that they could, because
value analysis with separation of states feels
very much like "symbolic model checking" where
the "model" is the C program being analyzed.
In particular, if the C program happened to be
a simulation, using boolean variables,
of some kind of logic circuit, the value analysis
(with separation of states) of the program would be
equivalent to model-checking the circuit.
But actual C programs do not have just boolean variables
or variables whose values can conveniently be
encoded in tuples of booleans, so the value
analysis borrows ideas and algorithms from
model-checking without literally relying on BDDs.

And truth be told, "hash-consing" was invented
in functional programming before being popularized
with BDDs, so it's only fair to borrow it back.

Pascal