Frama-C with Coq interactive prover

Question

I am trying to run Frama-C on a small code sample.
It works pretty well:

# frama-c -wp bubble_sort.c              
[kernel] Parsing bubble_sort.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] bubble_sort.c:15: Warning: 
  Missing assigns clause (assigns 'everything' instead)
[wp] bubble_sort.c:8: Warning: 
  Missing assigns clause (assigns 'everything' instead)
[wp] 13 goals scheduled
[wp] [Timeout] typed_bubble_sort_ensures (Qed 1ms) (Alt-Ergo)
[wp] [Timeout] typed_bubble_sort_terminates_part2 (Qed 1ms) (Alt-Ergo)
[wp] [Timeout] typed_bubble_sort_loop_invariant_established (Qed 2ms) (Alt-Ergo)
[wp] [Timeout] typed_bubble_sort_loop_invariant_4_established (Qed 2ms) (Alt-Ergo)
[wp] Proved goals:   10 / 14
  Unreachable:       1
  Qed:               7
  Alt-Ergo 2.5.4:    2 (17ms-20ms)
  Timeout:           4
[wp:pedantic-assigns] bubble_sort.c:6: Warning: 
  No 'assigns' specification for function 'bubble_sort'.
  Callers assumptions might be imprecise.

So there remain 4 proof obligations to be proved.

I want to prove them with the Coq interactive prover.
I've found several options that all look obsolete/irrelevant.

How can I run Coq to prove those proof obligations?

# frama-c -version         
28.1 (Nickel)

Running on Macbook M3 (ARM64)

I didn't manage to run frama-c-gui.
I can run Ivette, but I understand that it doesn't support WP yet, right?

#frama-c-gui              
zsh: command not found: frama-c-gui

frama-c -plugins
Alias Analysis      Lightweight May-Alias Analysis (experimental) (-alias-h)
Aorai               verification of behavioral properties (experimental)
                    (-aorai-h)
Callgraph           automatically compute the callgraph of the program. Using
                    Eva might improve the precision of this plug-in (-cg-h)
Dive                An interactive imprecision graph generator for Eva.
                    (-dive-h)
Dominators          Compute postdominators of statements (-dominators-h)
E-ACSL              Executable ANSI/ISO C Specification Language --- runtime
                    assertion checker generator (-e-acsl-h)
Eva                 automatically computes variation domains for the
                    variables of the program (-eva-h)
From analysis       functional dependencies (-from-h)
Impact              impact analysis (-impact-h)
Inout               operational, imperative and all kinds of inputs/outputs
                    (-inout-h)
Instantiate         Overrides standard library functions (-instantiate-h)
Loop                Find maximum number of iterations in loops (-loop-h)
Markdown report     generates a report in markdown format (-mdr-h)
Metrics             syntactic metrics (-metrics-h)
Nonterm             Warns when definitively non-terminating functions/loops
                    are detected (e.g. reachable functions with unreachable
                    returns). (-nonterm-h)
Obfuscator          obfuscator for confidential code (-obfuscator-h)
Occurrence          automatically computes where variables are used
                    (-occurrence-h)
Pdg                 Program Dependence Graph (-pdg-h)
Postdominators      computing postdominators of statements
                    (-postdominators-h)
Reduction           Generate ACSL annotations from Eva information (-reduc-h)
Report              Properties Status Report (-report-h)
Rtegen              generates annotations for runtime error checking (-rte-h)
Scope               data dependencies higher level functions (-scope-h)
Security-slicing    security slicing (experimental, undocumented)
                    (-security-slicing-h)
Semantic constant folding  propagates constants semantically (-scf-h)
Server              Frama-C Request Server (experimental) (-server-h)
Server TypeScript API  Generate TypeScript API for Server (-server-tsc-h)
Slicing             code slicer (-slicing-h)
Sparecode           code cleaner (-sparecode-h)
Studia              Tools for Eva case studies (-studia-h)
Users               function callees (-users-h)
Variadic            Variadic functions translation (-variadic-h)
WP                  Proof by Weakest Precondition Calculus (-wp-h)