title: FRAMA-C/WP Goals not being proved
body: <p>I am trying to prove a simplified version of an example from the WP manual but I keep getting an error for one of the ensures clauses.</p>
  <p>Here is my code:</p>
  <pre><code>/*@ requires \valid(a) &amp;&amp; \valid(b);
  @ ensures A: *a == \old(*b) ;
  @ ensures B: *b == \old(*a) ;
  @ assigns *a,*b ;
  @*/
  void swap(int *a,int *b)
  {
      int tmp = *a;
      *a = *b;
      *b = tmp;
  }
  </code></pre>
  <p>When I run <code>frama-c -wp -wp-rte swap.c</code>, I am getting the following error:</p>
  <pre><code>[kernel] Parsing main_wp.c (with preprocessing)
  [rte] annotating function swap
  Collecting axiomatic usagewarning: [Warning] cannot load an editor: missing field 'options'
  
  warning: [Warning] cannot load an editor: missing field 'options'
  
  warning: [Warning] cannot load an editor: missing field 'options'
  
  warning: [Warning] cannot load an editor: missing field 'options'
  
  warning: [Warning] cannot load an editor: missing field 'options'
  
  [wp] 8 goals scheduled
  [wp] [Alt-Ergo 2.0.0] Goal typed_swap_ensures_A : Failed
  [wp] [Cache] found:3
  [wp] Proved goals:    7 / 8
    Qed:               5  (1ms-2ms-4ms)
    Alt-Ergo 2.0.0:    2  (12ms-15ms) (22) (cached: 3) (failed: 1)
  </code></pre>
  <p>I was wondering if I am doing something wrong, or if this is an issue with the provers, as I have been facing similar errors with Alt-Ergo when testing files from larger codebases.</p>
  <p>I am using Frama-C 24.0 and Alt-Ergo 2.0.0</p>