frama-c-gui - Online in de cloud

PROGRAMMA:

NAAM

frama-c[.byte] - een statische analysator voor C-programma's

frama-c-gui[.byte] - de grafische interface van frama-c

KORTE INHOUD

frame-c [ opties ] bestanden

PRODUCTBESCHRIJVING

frame-c is een reeks tools gewijd aan de analyse van broncode geschreven in C. It
verzamelt verschillende statische analysetechnieken in één samenwerkingskader. Dit
framework kan worden uitgebreid door extra plug-ins geplaatst in de $FRAMAC_PLUGIN directory.
Het bevel

frame-c -help

geeft de volledige lijst van de plug-ins die momenteel zijn geïnstalleerd.

frame-c-gui is de grafische gebruikersinterface van frame-c. Het beschikt over dezelfde opties als:
de opdrachtregelversie.

frame-c.byte en frame-c-gui.byte zijn de ocaml bytecode-versies van de opdrachtregel en
grafische gebruikersinterface respectievelijk.

Standaard herkent Frama-C .c bestanden als C-bestanden die voorbewerking nodig hebben en .i bestanden als
C-bestanden zijn al voorbewerkt. Sommige plug-ins kunnen de lijst met herkende
bestanden. Pre-processing kan worden aangepast via de -cpp-opdracht en -cpp-extra-args
opties.

OPTIES

Syntaxis

Opties met een extra parameter kunnen ook onder het formulier worden geschreven

-optie=param

Deze optie is verplicht wanneer: param begint met een streepje ('-')

De meeste opties waarvoor geen parameter nodig is, hebben een overeenkomstige

-Nee-Keuze

optie die het tegenovergestelde effect heeft.

Help opties

-Help geeft een korte gebruiksmelding en de lijst met geïnstalleerde plug-ins.

-kernel-help
drukt de lijst met opties af die worden herkend door de kernel van Frama-C

-uitgebreid n
Stelt breedsprakigheidsniveau in (standaard is 1). Als je het op 0 zet, wordt er minder vooruitgang geboekt
berichten. Dit niveau kan ook per inpluggen basis, met optie -inpluggen-
breedsprakig n. Breedsprakigheidsniveau van de kernel kan worden geregeld met optie
-kernel-uitgebreid n.

-debuggen n
Stelt het foutopsporingsniveau in (standaard is 0, wat betekent dat er geen foutopsporingsberichten zijn). Deze optie
heeft dezelfde specialisaties per plug-in (en kernel) als -uitgebreid.

-rustig Stelt breedsprakigheid en foutopsporingsniveau in op 0.

Opties het regelen van Frame-C's pit

-absoluut-geldig-bereik
is van mening dat alle numerieke adressen in het bereik min-max zijn toegestaan. Grenzen zijn
ontleed als ocaml integer-constanten. Standaard zijn alle numerieke adressen:
als ongeldig beschouwd.

-add-pad p1[,p2[...,pn]]
voegt mappen toe door naar de lijst met mappen waarin plug-ins zich bevinden
doorzocht

[-no]-duplicatie toestaan
maakt duplicatie van kleine blokken mogelijk tijdens normalisatie van tests en lussen.
Anders gebruikt normalisatie labels en gotos. Grotere blokken en blokken met niet-
triviale controlestroom worden nooit gedupliceerd. Staat standaard op ja.

[-nee]-annot
leest ACSL-annotatie. Dit is de standaardinstelling. Annotaties zijn niet voorbewerkt door
standaard. Gebruik maken van -pp-annot daarom.

-grote-ints-hex max
gehele getallen groter dan max worden weergegeven in hexadecimaal (standaard zijn alle gehele getallen
weergegeven in decimalen)

-controleren voert integriteitscontroles uit op de interne AST (alleen voor ontwikkelaars).

[-no]-collapse-call-cast
staat impliciete cast toe tussen de waarde die wordt geretourneerd door een functie en de lwaarde die het is
toegewezen aan. Anders wordt een tijdelijke variabele gebruikt en wordt de cast expliciet gemaakt.
Staat standaard op ja.

[-nee]-constfold
vouwt alle syntactisch constante expressies in de code vóór analyses. Standaardinstellingen
naar nee.

[-no]-doorgaan-annot-fout
Bij het analyseren van een annotatie wordt het standaardgedrag (de -Nee versie van deze optie)
wanneer er een typecontrolefout optreedt, is het afwijzen van het bronbestand zoals het geval is voor
typecontrole fouten binnen de C-code. Met deze optie aan, zal de typechecker
voer alleen een waarschuwing uit en verwijder de annotatie, maar de typecontrole gaat door
(fouten in de C-code zijn echter nog steeds fataal).

-cpp-opdracht cmd
u gebruikt cmd als de opdracht om C-bestanden vooraf te verwerken. Standaard ingesteld op de CPP milieu
variabel of to

gcc-C-E-I.

als het niet is ingesteld. Om ACSL-annotaties te behouden, moet de preprocessor:
opmerkingen (de -C optie voor gcc). %1 en %2 kan worden gebruikt in cmd om de aan te duiden
originele bronbestand en het voorverwerkte bestand respectievelijk

-cpp-extra-args betoogt
Geeft aanvullende argumenten aan de pre-processor. Dit is alleen nuttig wanneer:
-voorbewerken-annot is ingesteld. Het voorbewerken van annotaties gebeurt in twee aparte pre-
verwerkingsfasen. De eerste is een normale doorgave van de C-code die macro behoudt
definities. Deze worden vervolgens gebruikt in de tweede doorgang waarin annotaties worden
voorbewerkt. betoogt worden alleen gebruikt voor de eerste doorgang, zodat argumenten die
mag niet twee keer worden gebruikt (zoals aanvullende include-richtlijnen of macro
definities) moet daar dus heen in plaats van -cpp-opdracht.

[-nee]-dynlink
Laad, indien ingeschakeld, alle dynamische plug-ins die in het zoekpad zijn gevonden (zie -print-plug-in-
pad voor meer informatie over het standaard zoekpad). Anders alleen plug-ins
aangevraagd door -laad-modules zal worden geladen. Standaardgedrag is ingeschakeld.

-opsommingen repr
Kies de manier waarop de weergave van opgesomde typen wordt bepaald. frame-c
-opsommingen hulp geeft de lijst met beschikbare opties. Standaard is gcc-opsommingen

-zwevende cijfers n
Wanneer u getallen met drijvende komma uitvoert, geeft u weer: n cijfers. Staat standaard op 12.

-float-flush-naar-nul
Bewerkingen met drijvende komma gelijk naar nul

-float-hex
display zweeft als hexadecimaal

-float-normaal
display floats met standaard Ocaml-routine

-float-relatief
float-interval weergeven als [ ondergrens++Breedte ]

[-no]-force-rl-arg-eval
dwingt de evaluatievolgorde van rechts naar links af voor argumenten van functieaanroepen. Anders
de evaluatievolgorde wordt niet gespecificeerd, zoals in de C-standaard. Staat standaard op nr.

-journaal-uitschakelen
Voer geen journaal van de huidige sessie uit. Zien -journaal inschakelen.

-journaal inschakelen
Standaard aan, dumpt een journaal van alle acties die zijn uitgevoerd tijdens de huidige
Frama-C-sessie in de vorm van een ocaml-script dat kan worden afgespeeld met -laden-
script. De naam van het script kan worden ingesteld met de -journaalnaam optie.

-journaalnaam naam
Stel de naam van het journaalbestand in (zonder de .ml verlenging). Standaard ingesteld op
frame_c_journal.

-geïnitialiseerde-padding-locals
Impliciete initialisatie van locals stelt opvulbits in op 0. Indien onwaar, opvulbits
worden niet geïnitialiseerd (standaard ingesteld op ja).

[-nee]-commentaar behouden
Probeert opmerkingen te behouden bij het mooi afdrukken van de broncode (standaard ingesteld op nee).

[-nee]-houd-schakelaar
. -vereenvoudigen-cfg is ingesteld, houdt switch-statements bij. Staat standaard op nr.

-keep-ongebruikte-gespecificeerde-functies
Bekijk -verwijder-ongebruikte-gespecificeerde-functies

[-no]-lib-invoer
Geeft aan dat het ingangspunt wordt aangeroepen tijdens de uitvoering van het programma. Dit houdt in
met name dat van globale variabelen niet kan worden aangenomen dat ze hun oorspronkelijke waarden hebben.
De standaard is -geen-lib-invoer: het startpunt is ook het startpunt van de
programma en globals hebben hun initiële waarde.

-laden filet
laad de (eerder opgeslagen) status in filet.

-laad-module m1[,m2[...,mn]]
laadt de ocaml-modules door . Deze modules moeten .cmxsbestanden voor de
native codeversie van Frama-c en .cmoor.cmabestanden voor de bytecode-versie (zie
het Dynlink-gedeelte van de Ocaml-handleiding voor meer informatie). Alle modules die zijn
aanwezig in de plug-in zoekpaden worden automatisch geladen.

-load-script s1[,s2,[...,sn]]
laadt de ocaml-scripts door . De scripts moeten zijn .mlbestanden. Zij
moet compileerbaar zijn, alleen vertrouwend op de standaardbibliotheek van Ocaml en de API van Frama-C. Indien
er is een aangepaste compilatiestap nodig, compileer ze buiten Frama-C en gebruik
-laad-module gebruiken.

-machdep machine
toepassingen machine als de huidige machine-afhankelijke configuratie (grootte van de verschillende
integer-types, endianness, ...). De lijst met momenteel ondersteunde machines is:
beschikbaar via -machdep hulp optie. Standaard is x86_32

-hoofd f
Sets f als startpunt van de analyse. Staat standaard op 'hoofd'. Standaard is het
beschouwd als het startpunt van het te analyseren programma. Gebruik maken van -lib-invoer if f
wordt verondersteld te worden genoemd in het midden van een executie.

-verduisteren
drukt een versluierde versie van de code af (waar de originele identifiers zijn vervangen)
door een zinloze) en exits. De correspondentietabel tussen origineel en nieuw
symbolen worden aan het begin van het resultaat bewaard.

-ocode filet
stuurt mooie gedrukte code om naar filet in plaats van standaarduitvoer.

[-no]-oorspronkelijke-naam
Tijdens de normalisatiefase kunnen sommige variabelen een nieuwe naam krijgen als ze anders zijn
variabele met dezelfde naam kunnen naast elkaar bestaan ​​(bijv. een globale variabele en een formele
parameter). Als deze optie is ingeschakeld, wordt er elke keer dat dit gebeurt een bericht afgedrukt.
Staat standaard op nr.

[-no]-waarschuwing-ondertekend-neergeslagen
alarmen genereren wanneer ondertekende downcasts het bestemmingsbereik kunnen overschrijden (standaard tot
niet).

[-no]-waarschuwing-ondertekende-overflow
alarmen genereren voor ondertekende bewerkingen die overlopen (standaard ingesteld op ja).

[-no]-warn-unsigned-downcast
alarmen genereren wanneer niet-ondertekende downcasts het bestemmingsbereik kunnen overschrijden (standaard
naar nee).

[-no]-warn-unsigned-overflow
alarmen genereren voor niet-ondertekende bewerkingen die overlopen (standaard op nee).

[-nee]-pp-annot
annotaties vooraf verwerken. Dit is momenteel alleen mogelijk bij gebruik van gcc (of GNU
cpp) preprocessor. De standaardinstelling is om annotaties niet vooraf te verwerken.

[-geen]-afdruk
pretty-print de broncode zoals genormaliseerd door CIL (standaard op nee).

-print-libpath
voert de map uit waarin de Frama-C-kernelbibliotheek is geïnstalleerd

-afdrukpad
alias van -print-share-pad

-print-plugin-pad
voert de map uit waar Frama-C zijn plug-ins doorzoekt (kan worden overschreven door de
FRAMAC_PLUGIN variabele en de -add-pad optioneel)

-print-share-pad
voert de map uit waar Frama-C zijn gegevens opslaat (kan worden overschreven door de
FRAMAC_SHARE variabel)

-verwijder-ongebruikte-gespecificeerde-functies
houdt functie-prototypes bij die een ACSL-specificatie hebben maar niet worden gebruikt in de
code. Dit is de standaardinstelling. Functies met het attribuut FRAMAC_BUILTIN zijn altijd
bewaard.

-veilige-arrays
Voor multidimensionale arrays of arrays die velden binnen structs zijn, wordt ervan uitgegaan dat:
alle toegangen moeten gebonden zijn (standaard ingesteld). De tegenovergestelde optie is -onveilig-
arrays

-opslaan filet
Slaat de staat van Frama-C op in filet nadat analyses hebben plaatsgevonden.

[-nee]-vereenvoudigen-cfg
verwijdert break, continue en switch statement voor analyses. Staat standaard op nr.

-dan maakt het mogelijk om analyses samen te stellen: een eerste run van Frama-C zal plaatsvinden met de opties
vaardigheden -dan en een tweede run zal worden gedaan met de opties na -dan op de
huidige project vanaf de eerste run.

-dan-op PRJ
Soortgelijke -dan behalve dat de tweede run wordt uitgevoerd in project PRJ Als dat niet zo is
project bestaat, wordt Frama-C afgesloten met een fout.

-tijd filet
voegt de tijd en datum van de gebruiker toe aan de gegeven filet wanneer Frama-C wordt afgesloten.

-typecontrole
dwingt typecontrole van de bronbestanden af. Deze optie is alleen relevant indien niet verder
analyse wordt gevraagd (omdat typecontrole impliciet vóór de analyse plaatsvindt)
wordt gelanceerd).

-univeau n
syntactisch uitrollen van loops n keer voor de analyse. Dit kan behoorlijk duur zijn
en sommige plug-ins (bijv. de waardeanalyse) bieden efficiëntere manieren om te presteren
hetzelfde. Zie hun respectievelijke handleidingen voor meer informatie. Dit kan ook
worden geactiveerd per lus via de lus pragma uitrollen richtlijn. EEN
negatieve waarde voor n zal dergelijke pragma's remmen.

[-geen]-unicode
voert ACSL-formules uit met utf8-tekens. Dit is de standaardinstelling. wanneer gegeven de
-geen-unicode optie, zal Frama-C in plaats daarvan de ASCII-versie gebruiken. Zie de ACSL-handleiding
voor de correspondentie.

-onveilige-arrays
zien -veilige-arrays

[-no]-niet-gespecificeerde-toegang
controleert of lees-/schrijftoegangen plaatsvinden in niet-gespecificeerde volgorde (volgens de C
standaardbegrip van sequentiepunt) worden uitgevoerd op afzonderlijke locaties. Met
-geen-niet-gespecificeerde-toegang, gaat ervan uit dat dit altijd het geval is (dit is de standaardinstelling).

-versie
geeft de versiereeks van Frama-C . weer

-waarschuwen-decimaal-zweven
waarschuwt wanneer een drijvende-kommaconstante niet exact kan worden weergegeven (bijv. 0.1).
kan een van zijn geen, eensof allen

[-no]-waarschuwen-niet-aangegeven-calle
waarschuwt wanneer een functie wordt aangeroepen voordat deze is gedeclareerd (standaard ingesteld).
Frama-C

Plugins specifiek opties

Voor elk inpluggen, het bevel

frame-c -inpluggen-Help

geeft de lijst met opties die specifiek zijn voor de plug-in.

EXIT STATUS

0 Succesvolle uitvoering

1 Ongeldige gebruikersinvoer

2 Gebruikersonderbreking (kill of equivalent)

3 Niet-geïmplementeerde functie

4 5 6 Interne fout

125 Onbekende fout

Uitgangsstatus groter dan 2 kan worden beschouwd als een bug (of een functieverzoek voor de case
van exit-status 3) en kan worden gerapporteerd op Frama-C's BTS (zie hieronder).

MILIEU VARIABELEN

Het is mogelijk om de plaatsen te controleren waar Frama-C naar zijn bestanden zoekt via de
volgende variabelen.

FRAMAC_LIB
De map waarin de gecompileerde interfaces van de kernel zijn geïnstalleerd

FRAMAC_PLUGIN
De directory waar Frama-C standaard plug-ins kan vinden. Als je plug-ins wilt hebben
op verschillende plaatsen, gebruik -add-pad gebruiken.

FRAMAC_SHARE
De map waarin Frama-C-gegevens zijn geïnstalleerd.

Gebruik frama-c-gui online met behulp van onworks.net-services