Updates the tutorial for Frama-C Scandium

[AllanBlanchard]

• General
  • Checked examples and screens for Frama-C 21
  • -wp-rte is now the rule
• I
• II
  • Adds smoke tests
  • More exercises for behaviors
    • Merge exercises 1 to 4 into a single one
    • Adds two simple exercises
  • Two new exercises for WP modularity
• IV
  • Removes a paragraph that was too dependent of provers versions
  • Slightly modify two exercises so that the proof is harder for Alt-Ergo
• V
  • Updates the section about ghosts with Frama-C 21 new features
  • Adds exercises about these new features
  • The verification that inductive definitions are well founded is now done through Why3
• VI
  • Updates ghost elements to be compliant with Frama-C 21