[kernel] fix missing function designator conversions to function ptr.

See merge request frama-c/frama-c!4328

[doc] fix devman tutorial Makefile and update test oracle

See merge request frama-c/frama-c!4340

[Ivette] Eva table: adds a button to globally control the view by callstacks.

See merge request frama-c/frama-c!4237

Populate specification

Closes #1090, #1078, #1045, and #982

See merge request frama-c/frama-c!3575

Thibault Martin authored 1 year ago and Allan Blanchard committed 1 year ago

- Hashtbl stores a bool to remember if bhv has assumes clauses
-  When looking for clauses to combine for default behavior, we search
   in that order (and stop if we found some clauses) :
   - unguarded behaviors (no assumes).
   - complete behaviors (each one of them needs to be in our table).
   - all behaviors in our table.
     It is a generic function used by {!Generator.get_clauses}.

David Bühler authored 1 year ago and Allan Blanchard committed 1 year ago

- Only generates assigns clauses when required:
  - when the analysis uses the specification to analyze a function
    (decided in function_calls.ml)
  - for Frama_C_* builtins, such as Frama_C_assert. Others builtins should
    already have a specification.
  - when interpreting a Frama_C_show_each directive, so other plugins known
    these functions have no effect.
  - in [Logic_inout.valid_behaviors], used by inout and from plugins to
    interpret a function specification.

- Also generates assigns clauses for functions with a body: this is required
  for the analysis of recursive functions and of functions specified in the
  -eva-use-spec parameter (in both case, a specific Eva warning is emitted).

- In recursion.ml, renames get_spec to check_spec.
  The generation of assigns clauses is now uniformly done in function_calls.