Download User Manual - Frama-C

CONTENTS
Contents
Foreword
7
1
Introduction
9
1.1
9
2
3
Overview
11
2.1
What is Frama-C? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
11
2.2
Frama-C as a Static Analysis Tool . . . . . . . . . . . . . . . . . . . . . . . . .
11
2.2.1
Frama-C as a Lightweight Semantic-Extractor Tool
. . . . . . . . . . .
12
2.2.2
Frama-C for Formal Verication of Critical Software
. . . . . . . . . .
12
2.3
Frama-C as a tool for C programs . . . . . . . . . . . . . . . . . . . . . . . . .
12
2.4
Frama-C as an Extensible Platform . . . . . . . . . . . . . . . . . . . . . . . .
12
2.5
Frama-C as a Collaborative Platform
. . . . . . . . . . . . . . . . . . . . . . .
13
2.6
Frama-C as a Development Platform
. . . . . . . . . . . . . . . . . . . . . . .
13
Getting Started
15
3.1
Installation
3.2
One Framework, Four Executables
. . . . . . . . . . . . . . . . . . . . . . . .
16
3.3
Frama-C Command Line and General Options . . . . . . . . . . . . . . . . . .
16
3.3.1
Getting Help
17
3.3.2
Frama-C Version
3.3.3
Verbosity and Debugging Levels
3.3.4
Getting time
3.3.5
Inputs and Outputs of source code
3.4
4
Organization of the Document . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15
17
. . . . . . . . . . . . . . . . . . . . .
17
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
18
. . . . . . . . . . . . . . . . . . . .
18
The share directory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
18
Working with Plug-ins
19
4.1
The Plug-in Taxonomy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
19
4.2
Installing Internal Plug-ins . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
19
4.3
Installing External Plug-ins
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
20
4.4
Using Plug-ins
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
20
5