-
Notifications
You must be signed in to change notification settings - Fork 0
/
Tesi.tex
182 lines (151 loc) · 7.41 KB
/
Tesi.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
\documentclass[12pt, a4paper, twoside]{book}
%%%%%%%%%%%Pacchetti Per Compilazione%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage{graphicx}
\usepackage[a-1b]{pdfx}
\usepackage[justification=centering]{caption}
\usepackage{subcaption}
\usepackage{fancyhdr} % abstract
\usepackage[english,italian]{babel}
\usepackage{listings}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{todonotes}
\usepackage{color}
\usepackage{algorithm}
\usepackage{frontespizio}
\usepackage[noend]{algpseudocode}
\usepackage{tabularx}
\usepackage{hhline}
\usepackage[section]{placeins}
\hypersetup{hidelinks}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%Comandi per formattazione%%%%%%%%%%%
%Per mantenere i floats (immagini, tabelle etc.) all'interno delle sottosezioni
\makeatletter
\AtBeginDocument{%
\expandafter\renewcommand\expandafter\subsection\expandafter{%
\expandafter\@fb@secFB\subsection
}%
}
\makeatother
%Label in italiano
\makeatletter
\renewcommand{\ALG@name}{Algorithm}
\makeatother
\renewcommand{\lstlistingname}{Listing}
\renewcommand{\listalgorithmname}{List of algorithms}
%Pagina bianca post capitolo effettivamente vuota e senza header
\let\origdoublepage\cleardoublepage
\newcommand{\clearemptydoublepage}{%
\clearpage
{\pagestyle{empty}\origdoublepage}%
}
\let\cleardoublepage\clearemptydoublepage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%Gestione Codice in Listings (Per C++)
\definecolor{mygreen}{rgb}{0,0.4,0}
\definecolor{mygray}{rgb}{0.35,0.35,0.35}
\definecolor{mymauve}{rgb}{0.58,0,0.82}
\lstset{ %
backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}
basicstyle=\footnotesize, % the size of the fonts that are used for the code
breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace
breaklines=true, % sets automatic line breaking
captionpos=b, % sets the caption-position to bottom
commentstyle=\color{mygray}, % comment style
deletekeywords={...}, % if you want to delete keywords from the given language
escapeinside={(*@}{@*)}, % if you want to add LaTeX within your code
extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
frame=no, % adds a frame around the code
keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
keywordstyle=\color{mygreen}, % keyword style
% language=C++, % the language of the code
otherkeywords={*,...}, % if you want to add more keywords to the set
numbers=left, % where to put the line-numbers; possible values are (none, left, right)
numbersep=5pt, % how far the line-numbers are from the code
numberstyle=\tiny\color{black}, % the style that is used for the line-numbers
rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
showstringspaces=false, % underline spaces within strings only
showtabs=false, % show tabs within strings adding particular underscores
stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered
stringstyle=\color{black}, % string literal style
tabsize=2, % sets default tabsize to 2 spaces
title=\lstname, % show the filename of files included with \lstinputlisting; also try caption instead of title
literate={``}{\textquotedblleft}1,
deletestring=[b]",
}
%%%Macro per pseudocodice
\newcommand*\Let[2]{\State #1 $\gets$ #2}
%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%Gestione Headers
\newcommand{\fncyblank}{\fancyhf{}}
\pagestyle{fancy}
\fancyhead{}
\fancyhead[LE, RO]{\leftmark}
\begin{document}
\selectlanguage{english}
%%%% Il frontespizio
%Per modificare:
% 1) Modifica Frontespizio/Frontespizio.tex
% 2) Compila Tesi (questo file)
% 3) Compila Tesi-frn.tex
% 4) Ricompila Tesi (questo file)
\input{Frontespizio/Frontespizio.tex}
\cleardoublepage
\include{Sommario/Abstract}
\cleardoublepage
\include{Sommario/Sommario}
\cleardoublepage
%%%% Gli indici
\pagestyle{plain}
\pagenumbering{roman}
\tableofcontents
%
\listoffigures %Commentare se non vi sono Immagini
%
%
%
%%%% La prefazione
\include{Capitoli/Introduction}
%
\pagestyle{fancy}
\part{Preliminary Notions}\label{part:preliminary-notions}
This part of the thesis introduces the main preliminary notions and premises that are needed for the presentation of the contents of Part 2, and that provide the reader with the necessary context information.
\\\\
In Chapter~\ref{chapter:verifying-the-correctness-of-programs}, the current approaches at verifying the correctness of programs are presented. After an introduction about testing in general, the reasons behind static analysis are presented and the pros and cons are weighed.
\\\\
Chapter~\ref{chapter:shift-left-testing} will then focus on shift-left testing movement and what it actually implies.
\\\\
Moving to Chapter~\ref{chapter:eclair}, the ECLAIR static analyzer is presented, on top of which the proof-of-concept has been realized. Before talking about integrating ECLAIR static analysis in IDEs, it is important to understand how ECLAIR works and the reasoning behind it. Chapter~\ref{chapter:eclair} also includes an introduction to MISRA C and its guidelines.
\\\\
Lastly, Chapter~\ref{chapter:language-server-protocol} presents the Language Server Protocol on top of which all the communications between the IDEs and the analysis system are performed. Thanks to this protocol, we were able to decouple the IDEs extensions from the analysis tools.
\include{Capitoli/Verifying_the_Correctness_of_Programs}
\include{Capitoli/Shift_left_testing}
\include{Capitoli/ECLAIR}
\include{Capitoli/Language_Server_Protocol}
\part{The Proof of Concept}\label{part:the-proof-of-concept}
In this part of the thesis, the main results of our work are presented.
\\\\
First, in Chapter~\ref{chapter:starting-point}, the starting point is presented: current tools and ECLAIR reports fruition are analyzed.
\\\\
Chapter~\ref{chapter:the-first-experiment} briefly describes the first experiment with the Language Server Protocol and ECLAIR, detailing the issues we faced. It laid the foundations for the prototype described in Chapter~\ref{chapter:project-architecture}.
\\\\
In Chapter~\ref{chapter:project-architecture}, the architecture of the project is presented. After a first high-level view of the interactions between the components, each of them is presented and analyzed in detail.
\include{Capitoli/Starting_point}
\include{Capitoli/The_first_experiment}
\include{Capitoli/Project_architecture}
\part{Conclusion}
Finally, in Chapter~\ref{chapter:discussion-and-future-work} some conclusions are drawn.
After an overview of the challenges we faced, some reasonings about future work are presented.
\include{Capitoli/Discussion_and_future_work}
%
%%%% La bibliografia
\bibliographystyle{plain} %{apalike} -- Scegliere lo stile preferito
\nocite{*}
\bibliography{./Bibliografia}
%
\include{Capitoli/Ringraziamenti}
%
\end{document}