- 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.