I just went through the CBMC tutorial[1] to make sure I'm not crazy. Yes, CBMC is a bounded model checker, as I thought.

  CBMC can also be used for programs with unbounded loops. In this
  case, CBMC is used for bug hunting only; CBMC does not attempt to
  find all bugs.

Frama-C is about eliminating ALL bugs, you are allowed to prove your "unbounded" loop algorithm actually terminates, and terminates with the correct solution, if you are willing to learn to use the manual proof assistant. CBMC can check for an extremely important class of errors, but it doesn't let you prove, say, your traveling salesman solver always returns a shortest trip T through the graph G, or that the graph coloring register allocator for your C compiler always correctly colors the graph, something that is actually done for the CompCert formally verified C compiler (using the Coq/Gallina proof assistant, which can be used with Frama-C).

However, having now gone through the CBMC manual, it appears to be much faster and easier to use for my own limited purposes than Frama-C. I don't need a sledgehammer to swat flies. I also like that the installation procedure on my machine was simply,

  $ sudo apt install cbmc

So I plan to give cprover a shot now, thanks for the heads up. : )

[1] http://www.cprover.org/cprover-manual/cbmc/tutorial/