Download Plug-In Development Guide - Frama-C

CONTENTS
3.3
Kernel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
35
3.4
Plug-ins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
36
4 Advanced Plug-in Development
39
4.1
File Tree Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
39
4.2
Frama-C Configure.in . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
40
4.2.1
Principle
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
40
4.2.2
Addition of a Simple Plug-in . . . . . . . . . . . . . . . . . . . . . . .
41
4.2.3
Configuration of New Libraries or Tools . . . . . . . . . . . . . . . . .
41
4.2.4
Addition of Library/Tool Dependencies . . . . . . . . . . . . . . . . .
42
4.2.5
Addition of Plug-in Dependencies . . . . . . . . . . . . . . . . . . . . .
43
4.3
Plug-in Specific Configure.in . . . . . . . . . . . . . . . . . . . . . . . . . . . .
43
4.4
Frama-C Makefile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
44
4.5
Plug-in Specific Makefile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
45
4.5.1
Using Makefile.dynamic . . . . . . . . . . . . . . . . . . . . . . . . .
46
4.5.2
Compiling Frama-C and external plug-ins at the same time . . . . . .
46
4.6
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
47
4.6.1
Using ptests . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
47
4.6.2
Configuration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
48
4.6.3
Alternative Testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
49
4.6.4
Detailed options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
50
4.6.5
Detailed directives . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
51
4.7
Plug-in General Services . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
53
4.8
Logging Services . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
53
4.8.1
From printf to Log . . . . . . . . . . . . . . . . . . . . . . . . . . . .
54
4.8.2
Log Quick Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . .
55
4.8.3
Logging Routine Options . . . . . . . . . . . . . . . . . . . . . . . . .
56
4.8.4
Advanced Logging Services . . . . . . . . . . . . . . . . . . . . . . . .
57
The Type library: Type Values and Datatypes . . . . . . . . . . . . . . . . . .
59
4.9.1
Type Value . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
60
4.9.2
Datatype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
60
4.10 Plug-in Registration and Access . . . . . . . . . . . . . . . . . . . . . . . . . .
64
4.10.1 Registration through a .mli File . . . . . . . . . . . . . . . . . . . . .
64
4.10.2 Kernel-integrated Registration and Access . . . . . . . . . . . . . . . .
65
4.10.3 Dynamic Registration and Access . . . . . . . . . . . . . . . . . . . . .
66
4.11 Journalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
69
4.12 Project Management System . . . . . . . . . . . . . . . . . . . . . . . . . . .
69
4.12.1 Overview and Key Notions . . . . . . . . . . . . . . . . . . . . . . . .
69
4.9
Testing
6