My Frama-C install (through opam) looks like this
# Installed packages for 4.04.0:
alt-ergo 1.30 Alt-Ergo, an SMT Solver for Software Verification
base-bigarray base Bigarray library distributed with the OCaml compiler
base-threads base Threads library distributed with the OCaml compiler
base-unix base Unix library distributed with the OCaml compiler
camlp5 6.17 Preprocessor-pretty-printer of OCaml
camlzip 1.06 Provides easy access to compressed files in ZIP, GZIP and JAR format
cmdliner 0.9.8 Declarative definition of command line interfaces for OCaml
conf-autoconf 0.1 Virtual package relying on autoconf installation.
conf-gmp 1 Virtual package relying on a GMP lib system installation.
conf-gnomecanvas 2 Virtual package relying on a Gnomecanvas system installation.
conf-gtksourceview 2 Virtual package relying on a GtkSourceView system installation.
conf-m4 1 Virtual package relying on m4
conf-perl 1 Virtual package relying on perl
conf-which 1 Virtual package relying on which
coq 8.5.3 Formal proof management system.
coqide 8.5.3 IDE of the Coq formal proof management system.
depext 1.0.2 Query and install external dependencies of OPAM packages
frama-c 20161101 Platform dedicated to the analysis of source code written in C. Silico
frama-c-base 20161101 Platform dedicated to the analysis of source code written in C. Silico
lablgtk 2.18.5 OCaml interface to GTK+
menhir 20161115 LR(1) parser generator
ocamlbuild 0.9.3 OCamlbuild is a build system with builtin rules to easily build most O
ocamlfind 1.7.1 A library manager for OCaml
ocamlgraph 1.8.7 A generic graph library for OCaml
ocplib-simplex 0.3 A library implementing a simplex algorithm, in a functional style, for
why3 0.87.2 Why3 environment for deductive program verification.
why3-base 0.87.2 Why3 environment for deductive program verification (base)
zarith 1.4.1 Implements arithmetic and logical operations over arbitrary-precision