How to run Frama-c WP plug-in with Coq interactive theorem prover?

Question

Here is the swap example form WP plug-in tutorial;

/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a, int *b)
{
  int tmp;

  tmp = *a;
  *a = *b;
  *b = tmp;
  return;
}

And here is the result when I run frama-c on it with coq;

frama-c -wp -wp-rte -wp-proof coq swap.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[rte] annotating function swap
[wp] 9 goals scheduled
[wp] [Coq] Goal typed_swap_assert_rte_mem_access : Unknown
[wp] [Coq] Goal typed_swap_post_A : Unknown
[wp] [Coq] Goal typed_swap_assert_rte_mem_access_3 : Unknown
[wp] Proved goals:    6 / 9
     Qed:             6  (0.13ms-0.71ms-2ms)
     Coq:             0  (unknown: 3)

So Coq returns Unknown for all three Proof obligations that remained to it.

Is it normal? and why?

Am I supposed to manually prove proofs for them mnually?

Can anybody get this example running okay with coq?

Versions; Frama-c Magnesium-20151002, Coq 8.4.6, OCaml 4.02.3 running on MacOS 10.11.4

Answer 1

Indeed, Coq is an interactive theorem prover. Which means that you must write the proofs yourselves (maybe some default tactics are tried, but generally you end up doing it manually). You can see the goals using coqide instead of coq: frama-c -wp -wp-rte -wp-proof coqide swap.c.