While ensuring the correctness of an implementation based on a formal functional specification provides the strongest guarantee, it can be prohibitively expensive to achieve. In practice, a combination of formal methods is commonly employed to attain an appropriate level of assurance. This includes static analyses to ensure the absence of runtime errors, deductive verification for functional correctness, and dynamic verification for components that cannot be proven through deductive verification. Frama-C is a source code analysis platform designed for the verification of large-scale programs written in ISO C source code. It offers comprehensive support for the integration of formal methods, offering users a set of plug-ins that facilitate static and dynamic analysis of safety-critical and security-critical software. Furthermore, the collaborative verification capabilities are achieved through the integration of these plug-ins on a shared kernel and their adherence to a standardized specification language known as ACSL (ANSI/ISO C Specification Language). This tutorial is an introduction, including hands-on sessions, to the analysis and verification of C programs using Frama-C. The main plug-ins of Frama-C are presented, as well as their combination in a verification project. We illustrate these plug-ins on several examples taken from Contiki, a lightweight operating system for the Internet of Things.