Progress on Formal Methods

[HalosGhost]

The current output from make verify is as follows:

[kernel] Warning: no input file.
[wp] 0 goal scheduled
[wp] Proved goals:    0 / 0
[kernel] Parsing src/enlighten.c (with preprocessing)
[kernel] Parsing src/main.c (with preprocessing)
[rte] annotating function bl_calc
[rte] annotating function bl_cmd_parse
[rte] annotating function bl_get
[rte] annotating function bl_list
[rte] annotating function bl_set
[rte] annotating function main
[wp] src/enlighten.c:43: Warning:
  Allocation, initialization and danglingness not yet implemented
  (\initialized(param0))
[wp] src/enlighten.c:41: Warning:
  Allocation, initialization and danglingness not yet implemented
  (\initialized(param0))
[wp] src/enlighten.c:40: Warning:
  Allocation, initialization and danglingness not yet implemented
  (\initialized(param0))
[wp] src/enlighten.c:25: Warning:
  Allocation, initialization and danglingness not yet implemented
  (\initialized(param0))
[wp] FRAMAC_SHARE/libc/stdlib.h:342: Warning:
  Allocation, initialization and danglingness not yet implemented
  (\freeable(p))
[wp] FRAMAC_SHARE/libc/stdlib.h:348: Warning:
  Allocation, initialization and danglingness not yet implemented
  (freed: \allocable(\at(p,wp:pre)))
[wp] src/enlighten.c:85: Warning:
  Missing assigns clause (assigns 'everything' instead)
[wp] Warning: No definition for 'format_length' interpreted as reads nothing
[wp] FRAMAC_SHARE/libc/stdlib.h:331: Warning:
  Allocation, initialization and danglingness not yet implemented
  (allocation: \fresh{Old, Here}(\at(\result,wp:post),\at(size,wp:pre)))
[wp] src/enlighten.c:76: Warning:
  Missing assigns clause (assigns 'everything' instead)
[wp] src/enlighten.c:68: Warning:
  Missing assigns clause (assigns 'everything' instead)
[wp] src/main.c:157: Warning:
  Cast with incompatible pointers types (source: char**) (target: sint8*)
[wp] FRAMAC_SHARE/libc/time.h:255: User Error:
  Non-assignable term (rmtp ≡ \null? \empty: *rmtp)
[kernel] Plug-in wp aborted: invalid user input.
make: *** [Makefile:47: verify] Error 1

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.

[HalosGhost]

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.