frama-c.byte - Online în cloud

PROGRAM:

NUME

frama-c[.byte] - un analizor static pentru programele C

frama-c-gui[.byte] - interfața grafică a frama-c

REZUMAT

frama-c [ Opțiuni ] fișiere

DESCRIERE

frama-c este o suită de instrumente dedicate analizei codului sursă scris în C. It
reunește mai multe tehnici de analiză statică într-un singur cadru de colaborare. Acest
framework-ul poate fi extins prin pluginuri suplimentare plasate în $FRAMAC_PLUGIN director.
Comanda

frama-c -help

va furniza lista completă a pluginurilor care sunt instalate în prezent.

frama-c-gui este interfața grafică cu utilizatorul a frama-c. Dispune de aceleași opțiuni ca și
versiunea de linie de comandă.

frama-c.byte și frama-c-gui.byte sunt versiunile ocaml bytecode ale liniei de comandă și
respectiv interfață grafică cu utilizatorul.

În mod implicit, Frama-C recunoaște .c fișiere ca fișiere C care necesită preprocesare și .i fişiere ca
Fișierele C au fost deja preprocesate. Unele plugin-uri pot extinde lista de recunoscute
fișiere. Preprocesarea poate fi personalizată prin intermediul -cpp-comandă și -cpp-extra-args
opțiuni.

OPŢIUNI

Sintaxă

Opțiunile care iau un parametru suplimentar pot fi, de asemenea, scrise sub formular

-opțiune=PARAM

Această opțiune este obligatorie când PARAM începe cu liniuță ('-')

Majoritatea opțiunilor care nu acceptă niciun parametru au o corespondență

-Nu-opțiune

opțiune care are efectul opus.

Ajutor Opțiuni

-Ajutor oferă o scurtă notificare de utilizare și lista de pluginuri instalate.

-kernel-help
tipărește lista de opțiuni recunoscute de nucleul Frama-C

-verbos n
Setează nivelul de verbozitate (implicit este 1). Setarea lui la 0 va genera mai puțin progres
mesaje. Acest nivel poate fi setat și pe per conecteaza baza, cu optiune -conecteaza-
prolix n. Nivelul de verbositate al nucleului poate fi controlat cu opțiune
-kernel-verbose n.

- depanare n
Setează nivelul de depanare (implicit este 0, adică nu există mesaje de depanare). Această opțiune
are aceleași specializări pentru plugin (și nucleu) ca -verbos.

-Liniște Setează nivelul de nivel de depanare și nivel de depanare la 0.

Opţiuni controlul Frama-C nucleu

-interval-valid-absolut
consideră că toate adresele numerice din interval minim maxim sunt valabile. Limitele sunt
analizate ca constante întregi ocaml. În mod implicit, toate adresele numerice sunt
considerat invalid.

-add-path p1[,p2[...,pn]]
adaugă directoare prin la lista directoarelor în care se află pluginurile
cautat

[-nu]-permite-duplicare
permite duplicarea blocurilor mici în timpul normalizării testelor și buclelor.
În caz contrar, normalizarea folosește etichete și gotos. Blocuri mai mari și blocuri cu non-
fluxul de control trivial nu sunt niciodată duplicate. Setarea implicită este da.

[-nu]-nu
citește adnotarea ACSL. Aceasta este valoarea implicită. Adnotările nu sunt preprocesate de
Mod implicit. Utilizare -pp-nu pentru asta.

-big-ints-hex max
numere întregi mai mari decât max sunt afișate în hexazecimal (în mod implicit, toate numerele întregi sunt
afișat în zecimală)

-Verifica efectuează verificări de integritate pe AST-ul intern (numai pentru dezvoltatori).

[-nu]-restrânge-apel-cast
permite turnarea implicită între valoarea returnată de o funcție și valoarea l este
atribuit. În caz contrar, este utilizată o variabilă temporară și distribuția este explicită.
Setarea implicită este da.

[-nu]-constfold
pliază toate expresiile constante din punct de vedere sintactic din cod înainte de analize. Valori implicite
la nr.

[-no]-continue-anot-error
Când se analizează o adnotare, comportamentul implicit ( -Nu versiunea acestei opțiuni)
atunci când apare o eroare de verificare a tipului este de a respinge fișierul sursă, așa cum este cazul
erori de verificare de tip în codul C. Cu această opțiune activată, verificatorul de tip va
emite doar un avertisment și eliminați adnotarea, dar verificarea tipului va continua
(Erorile în codul C sunt încă fatale, totuși).

-cpp-comandă cmd
Utilizeaza cmd ca comandă pentru a preprocesa fișierele C. Implicit la CPP mediu inconjurator
variabilă sau către

gcc -C -E -I.

dacă nu este setat. Pentru a păstra adnotările ACSL, preprocesorul trebuie să păstreze
comentarii ( -C opțiune pentru gcc). %1 și %2 poate fi utilizat în cmd pentru a desemna
fișierul sursă original și, respectiv, fișierul preprocesat

-cpp-extra-args args
Oferă argumente suplimentare pre-procesorului. Acest lucru este util doar atunci când
-preprocesare-nu este setat. Preprocesarea adnotărilor se face în două pre-procesare separate.
etapele de prelucrare. Prima este o trecere normală a codului C care reține macro
definiții. Acestea sunt apoi utilizate în a doua trecere în care sunt adnotările
preprocesate. args sunt folosite numai pentru prima trecere, astfel încât argumentează că
nu ar trebui folosit de două ori (cum ar fi directive suplimentare de includere sau macro
definiţii) trebuie astfel să meargă acolo în loc de -cpp-comandă.

[-nu]-dynlink
Când este activat, încărcați toate pluginurile dinamice găsite în calea de căutare (vezi -print-plugin-
cale pentru mai multe informații despre calea de căutare implicită). În rest, doar pluginuri
solicitat de -module-încărcare va fi încărcat. Comportamentul implicit este activat.

-enumerii Repr
Alegeți modul în care este determinată reprezentarea tipurilor enumerate. frama-c
-enumerii ajutor oferă lista de opțiuni disponibile. Implicit este gcc-enums

-cifre-float n
Când scoateți numere în virgulă mobilă, afișați n cifre. Implicit la 12.

-float-flush-la-zero
Operațiunile cu virgulă mobilă ajung la zero

-float-hex
afișarea plutește ca hexazecimal

-float-normal
afișajul plutește cu rutina standard Ocaml

-float-relativ
Afișează intervalul flotant ca [ limita inferioară++lățime ]

[-nu]-force-rl-arg-eval
forțează ordinea de evaluare de la dreapta la stânga pentru argumentele apelurilor de funcție. In caz contrar
ordinea de evaluare este lăsată nespecificată, ca în standardul C. Implicit la nr.

-jurnal-dezactivare
Nu scoateți un jurnal al sesiunii curente. Vedea -jurnal-activare.

-jurnal-activare
Activat în mod implicit, aruncă un jurnal cu toate acțiunile efectuate în timpul curentului
Sesiune Frama-C sub forma unui script ocaml cu care se poate reda -sarcină-
scenariu. Numele scriptului poate fi setat cu -nume-revista opțiune.

-nume-revista nume
Setați numele fișierului jurnal (fără .ml extensie). Implicit la
frama_c_journal.

-initializate-padding-locals
Inițializarea implicită a localurilor setează biții de umplutură la 0. Dacă este fals, biții de umplutură
sunt lăsate neinițializate (implicit la da).

[-nu]-pastreaza-comentarii
Încearcă să păstreze comentariile când imprimă destul de mult codul sursă (implicit nu).

[-nu]-menține-comutator
Cand -simplificare-cfg este setat, păstrează instrucțiunile switch. Implicit la nr.

-păstrarea-funcții-specificate-neutilizate
Vedea -elimină-funcțiile-specificate-neutilizate

[-nu]-lib-entry
Indică faptul că punctul de intrare este apelat în timpul execuției programului. Aceasta implică în
în special că nu se poate presupune că variabilele globale au valorile lor inițiale.
Valoarea implicită este -no-lib-entry: punctul de intrare este, de asemenea, punctul de plecare al
programul și globalurile au valoarea lor inițială.

-sarcină fişier
încărcați starea (salvată anterior) conținută în fişier.

-modul-încărcare m1[,m2[...,mn]]
încarcă modulele ocaml prin . Aceste module trebuie să fie .cmxsfișiere pentru
versiunea de cod nativă a Frama-c și .cmoor.cmafișiere pentru versiunea bytecode (vezi
secțiunea Dynlink a manualului Ocaml pentru mai multe informații). Toate modulele care sunt
prezente în căile de căutare plugin sunt încărcate automat.

-încărcare-script s1[,s2,[...,sn]]
încarcă scripturile ocaml prin . Scripturile trebuie să fie .mlfișiere. ei
trebuie să fie compilabil bazându-se numai pe biblioteca standard Ocaml și API-ul Frama-C. Dacă
este nevoie de un pas de compilare personalizat, compilați-le în afara Frama-C și utilizați
-modul-încărcare in schimb.

-machdep maşină
utilizări maşină ca configurația curentă dependentă de mașină (dimensiunea diferitelor
tipuri întregi, finalitate, ...). Lista mașinilor acceptate în prezent este
disponibil prin -machdep ajutor opțiune. Implicit este x86_32

-principal f
Seturi f ca punct de intrare al analizei. Implicit la „principal”. În mod implicit, este
considerat ca punct de plecare al programului analizat. Utilizare -lib-intrare if f
ar trebui să fie numit în mijlocul unei execuții.

-eclipsa
tipărește o versiune ofuscată a codului (unde identificatorii originali sunt înlocuiți
prin unul lipsit de sens) și iese. Tabelul de corespondență dintre original și nou
simbolurile se păstrează la începutul rezultatului.

-ocode fişier
redirecționează codul destul de tipărit către fişier în loc de ieșire standard.

[-nu]-nume-orig
În timpul fazei de normalizare, unele variabile pot fi redenumite atunci când sunt diferite
variabilă cu același nume poate coexista (de exemplu, o variabilă globală și o variabilă formală
parametru). Când această opțiune este activată, de fiecare dată când se întâmplă acest lucru este tipărit un mesaj.
Implicit la nr.

[-nu]-warn-semnat-downcast
generarea de alarme atunci când downcast-urile semnate pot depăși intervalul de destinație (implicit la
nu).

[-nu]-warn-signed-overflow
generați alarme pentru operațiunile semnate care depășesc (implicit la da).

[-nu]-warn-unsigned-downcast
generați alarme atunci când downcast-urile nesemnate pot depăși intervalul de destinație (implicit
la nu).

[-nu]-warn-unsigned-overflow
generați alarme pentru operațiuni nesemnate care depășesc (implicit nu).

[-nu]-pp-nu
adnotări pre-proces. În prezent, acest lucru este posibil numai atunci când utilizați gcc (sau GNU
cpp) pre-procesor. Valoarea implicită este să nu preproceseze adnotările.

[-nu]-tipărește
pretty-tipărește codul sursă așa cum este normalizat de CIL (implicit la nu).

-print-libpath
scoate directorul în care este instalată biblioteca kernel Frama-C

-print-path
alias de -print-share-path

-print-plugin-path
afișează directorul în care Frama-C își caută pluginurile (poate fi suprascris de
FRAMAC_PLUGIN variabila si cea -add-path opțiune)

-print-share-path
scoate directorul în care Frama-C își stochează datele (poate fi suprascris de
FRAMAC_SHARE variabil)

-elimină-funcțiile-specificate-neutilizate
păstrează prototipurile de funcții care au o specificație ACSL, dar nu sunt utilizate în
cod. Aceasta este valoarea implicită. Funcții având atributul FRAMAC_BUILTIN sunt întotdeauna
ținut.

-safe-arrays
Pentru matrice multidimensionale sau matrice care sunt câmpuri în interiorul structs , se presupune că
toate accesele trebuie să fie în legătură (setate implicit). Opțiunea opusă este -nesigur-
matrice

-Salvați fişier
Salvează starea lui Frama-C în fişier după ce au avut loc analizele.

[-nu]-simplificare-cfg
elimină declarația break, continue și switch înainte de analize. Implicit la nr.

-atunci permite să se compună analize: o primă rulare a Frama-C va avea loc cu opțiunile
înainte -atunci iar oa doua rulare se va face cu opțiunile după -atunci pe
proiect curent de la prima rulare.

-apoi PRJ
similar -atunci cu excepția faptului că a doua rulare este efectuată în proiect PRJ Daca nu asa
proiectul există, Frama-C iese cu o eroare.

-timp fişier
adaugă ora și data utilizatorului în date fişier când iese Frama-C.

-verificare de tip
forțează verificarea de tip a fișierelor sursă. Această opțiune este relevantă numai dacă nu mai departe
se solicită analiza (deoarece verificarea tipului va avea loc implicit înaintea analizei
este lansat).

-nivelul n
derulează sintactic buclele n ori înainte de analiză. Acest lucru poate fi destul de costisitor
iar unele plugin-uri (de exemplu, analiza valorii) oferă modalități mai eficiente de a performa
același lucru. Consultați manualele respective pentru mai multe informații. Acest lucru poate, de asemenea
fi activat pe o buclă prin intermediul buclă pragma derula directivă. A
valoare negativă pentru n va inhiba astfel de pragmate.

[-nu]-unicode
scoate formule ACSL cu caractere utf8. Aceasta este valoarea implicită. Când i se dă
-fără-unicode opțiunea, Frama-C va folosi în schimb versiunea ASCII. Consultați manualul ACSL
pentru corespondență.

-matrice-nesigure
vedea -safe-arrays

[-nu]-acces-nespecificat
verifică dacă accesările de citire/scriere au loc în ordine nespecificată (conform C
noțiunea standard de punct de secvență) sunt efectuate pe locații separate. Cu
-fără-acces-nespecificat, presupune că este întotdeauna cazul (acesta este implicit).

-versiune
scoate șirul de versiune a lui Frama-C

-warn-zecimal-float
avertizează când o constantă în virgulă mobilă nu poate fi reprezentată exact (de ex. 0.1).
poate fi unul dintre nici unul, dată, Sau toate

[-nu]-warn-undeclared-callee
avertizează când o funcție este apelată înainte de a fi declarată (setată implicit).
Frama-C

Plugin-uri specific Opțiuni

Pentru fiecare conecteaza, comanda

frama-c -conecteaza-Ajutor

va oferi lista de opțiuni care sunt specifice pluginului.

EXIT STAREA

0 Executarea cu succes

1 Intrare nevalidă de utilizator

2 Întreruperea utilizatorului (ucidere sau echivalent)

3 Caracteristica neimplementată

4 5 6 Eroare internă

125 Eroare necunoscută

Starea de ieșire mai mare de 2 poate fi considerată o eroare (sau o solicitare de caracteristică pentru caz
de statutul de ieșire 3) și poate fi raportat pe BTS-ul Frama-C (vezi mai jos).

MEDIUL VARIABILE

Este posibil să controlați locurile în care Frama-C își caută fișierele prin intermediul
urmatoarele variabile.

FRAMAC_LIB
Directorul în care sunt instalate interfețele compilate ale nucleului

FRAMAC_PLUGIN
Directorul în care Frama-C poate găsi pluginuri standard. Dacă doriți să aveți pluginuri
în mai multe locuri, folosiți -add-path in schimb.

FRAMAC_SHARE
Directorul în care sunt instalate datele Frama-C.

Utilizați frama-c.byte online folosind serviciile onworks.net