Open HalosGhost opened 5 years ago
On looking further into this, this error:
Allocation, initialization and danglingness not yet implemented
(\initialized(param0))
refers to the fact that the function relies on dynamic memory allocation (either explicitly in the function itself, or implicitly via something the function calls). The result is that frama-c
cannot actually verify the code (as it does not support dynamic memory allocation.
This gives us a couple options: we can refactor enlighten.c
to be entirely pure and have the code calling it do all the memory allocation (this would be a reasonably large refactor, but shouldn't add too much weight over all), or abandon formal verification for 1.0 (and instead seek this as a primary feature for the next release).
I am undecided for the moment, but if anyone has any opinions, I would be interested in hearing them.
The current output from
make verify
is as follows:This gives us a great starting list of things we know we need. But it may still be better to try to make a specification for each function in
enlighten.c
, and see where that gets us. That is the next step.