Hulktahukate (teegi APRON) kasutamine Goblint analüsaatoris
Organization
Programming Languages
Abstract
Goblint on staatiline programmianalüsaator C keele jaoks, mis keskendub
andmejooksude tuvastamise ja andmejooksu-vabaduse tõestamisele. Lihtsustatult
tähendab see seda, et Goblint saab kasutajalt sisendiks mitmelõimelise
programmi lähtekoodi ja otsustab, kas kõik globaalsed muutujad on korrektselt
lukkudega kaitstud.
Mida täpsemalt Goblint teab, milliseid väärtusi võivad (näiteks täisarvulised)
muutujad omada, seda täpsem on kogu analüüsi tulemus ning seda vähem on
ekslikke andmejooksude hoiatusi. Samas, liigne täpsus tähendab ka enamasti
seda, et analüüs võtab ebamõistlikult kaua aega.
Üks huvitav viis arvulite muutujate väärtuste hulkade hoidmiseks on kumerad
hulktahukad. Intuitiivselt tähendab see seda, et programmi seisundit mingis
kohas kirjeldab teatav võrratuste süsteem. Näiteks, x>10, x
Graduation Theses defence year
2015-2016
Supervisor
Kalmer Apinis
Spoken language (s)
Estonian, English
Requirements for candidates
Level
Masters
Application of contact
Name
Kalmer Apinis
Phone
+372 737 5443
E-mail
Full Document