frama-c.byte - Online sa Cloud

PROGRAMA:

NAME

frama-c[.byte] - isang static na analyzer para sa mga C program

frama-c-gui[.byte] - ang graphical na interface ng frama-c

SINOPSIS

frama-c [ pagpipilian ] file

DESCRIPTION

frama-c ay isang hanay ng mga tool na nakatuon sa pagsusuri ng source code na nakasulat sa C. Ito
nangangalap ng ilang static na diskarte sa pagsusuri sa iisang collaborative na balangkas. Ito
framework ay maaaring palawigin ng mga karagdagang plugin na inilagay sa $FRAMAC_PLUGIN direktoryo.
Ang utos

frama-c -tulong

ay magbibigay ng buong listahan ng mga plugin na kasalukuyang naka-install.

frama-c-gui ay ang graphical na user interface ng frama-c. Nagtatampok ito ng parehong mga pagpipilian bilang
ang bersyon ng command-line.

frama-c.byte at frama-c-gui.byte ay ang mga bersyon ng ocaml bytecode ng command-line at
graphical na user interface ayon sa pagkakabanggit.

Bilang default, kinikilala ng Frama-C .c mga file bilang C file na nangangailangan ng pre-processing at .i mga file bilang
C file na na-pre-process na. Maaaring pahabain ng ilang plugin ang listahan ng mga kinikilala
mga file. Maaaring i-customize ang pre-processing sa pamamagitan ng -cpp-utos at -cpp-extra-args
mga pagpipilian.

Opsyon

palaugnayan

Ang mga opsyon na kumukuha ng karagdagang parameter ay maaari ding isulat sa ilalim ng form

-opsyon=ang pera ko

Ang pagpipiliang ito ay sapilitan kapag ang pera ko nagsisimula sa gitling ('-')

Karamihan sa mga opsyon na walang parameter ay may katumbas

-hindi-pagpipilian

opsyon na may kabaligtaran na epekto.

Tulong pagpipilian

-tulong nagbibigay ng maikling paunawa sa paggamit at ang listahan ng mga naka-install na plugin.

-kernel-tulong
nagpi-print ng listahan ng mga opsyon na kinikilala ng kernel ng Frama-C

-salita n
Itinatakda ang antas ng verbosity (default ay 1). Ang pagtatakda nito sa 0 ay maglalabas ng mas kaunting pag-unlad
mga mensahe. Ang antas na ito ay maaari ding itakda sa isang per isaksak batayan, na may opsyon -isaksak-
pandiwang n. Ang antas ng verbosity ng kernel ay maaaring kontrolin gamit ang opsyon
-kernel-verbose n.

-debug n
Nagtatakda ng antas ng pag-debug (ang default ay 0, ibig sabihin ay walang mga mensahe sa pag-debug). Ang pagpipiliang ito
ay may parehong espesyalisasyon sa bawat plugin (at kernel) gaya ng -salita.

-tahimik Itinatakda ang verbosity at antas ng pag-debug sa 0.

Options pagkontrol Mga Frama-C pinakabuod

-absolute-valid-range
Isinasaalang-alang na ang lahat ng mga numerical na address sa hanay min-max ay may bisa. Ang mga hangganan ay
na-parse bilang ocaml integer constants. Bilang default, ang lahat ng mga numerical na address ay
itinuturing na hindi wasto.

-add-path p1[,p2[...,pn]]
nagdadagdag ng mga direktoryo sa pamamagitan ng sa listahan ng mga direktoryo kung nasaan ang mga plugin
hinanap

[-no]-allow-duplication
nagbibigay-daan sa pagdoble ng mga maliliit na bloke sa panahon ng normalisasyon ng mga pagsubok at mga loop.
Kung hindi, ang normalisasyon ay gumagamit ng mga label at gotos. Mas malalaking bloke at bloke na may hindi
Ang walang kabuluhang daloy ng kontrol ay hindi kailanman nadoble. Default sa yes.

[-no]-annot
nagbabasa ng ACSL annotation. Ito ang default. Ang anotasyon ay hindi paunang pinoproseso ni
default. Gamitin -pp-annot para sa na.

-big-ints-hex max
mga integer na mas malaki kaysa sa max ay ipinapakita sa hexadecimal (bilang default, lahat ng integer ay
ipinapakita sa decimal)

-suriin nagsasagawa ng mga pagsusuri sa integridad sa panloob na AST (para sa mga developer lamang).

[-no]-collapse-call-cast
nagbibigay-daan sa implicit cast sa pagitan ng value na ibinalik ng isang function at ang lvalue nito
nakatalaga sa. Kung hindi, isang pansamantalang variable ang ginagamit at ang cast ay gagawing tahasan.
Default sa yes.

[-no]-constfold
tiklop ang lahat ng syntactically pare-pareho ang mga expression sa code bago pag-aralan. Mga Default
sa no.

[-no]-continue-annot-error
Kapag sinusuri ang isang anotasyon, ang default na gawi (ang -hindi bersyon ng opsyong ito)
kapag naganap ang isang error sa pag-typecheck ay ang pagtanggi sa source file gaya ng kaso para sa
mga error sa pag-typecheck sa loob ng C code. Kapag naka-on ang opsyong ito, gagawin ng typechecker
maglabas lamang ng babala at itapon ang anotasyon ngunit magpapatuloy ang pag-typecheck
(Ang mga error sa C code ay nakamamatay pa rin, bagaman).

-cpp-utos cmd
Gumagamit cmd bilang utos sa paunang proseso ng mga C file. Default sa CPP kapaligiran
variable o sa

gcc -C -E -I.

kung hindi ito nakatakda. Upang mapanatili ang mga ACSL annotation, dapat panatilihin ng preprocessor
komento (ang -C opsyon para sa gcc). %1 at %2 maaaring magamit sa cmd upang tukuyin ang
orihinal na source file at ang paunang naprosesong file ayon sa pagkakabanggit

-cpp-extra-args mga pagtatalo
Nagbibigay ng mga karagdagang argumento sa pre-processor. Ito ay kapaki-pakinabang lamang kapag
-preprocess-annot ay nakatakda. Ginagawa ang mga anotasyon bago ang pagproseso sa dalawang magkahiwalay na pre-
mga yugto ng pagproseso. Ang una ay isang normal na pass sa C code na nagpapanatili ng macro
mga kahulugan. Pagkatapos ay gagamitin ang mga ito sa pangalawang pass kung saan ang mga anotasyon ay
pre-processed. mga pagtatalo ay ginagamit lamang para sa unang pass, upang ang mga argumento na
hindi dapat gamitin nang dalawang beses (tulad ng karagdagang isama ang mga direktiba o macro
mga kahulugan) ay dapat pumunta doon sa halip na -cpp-utos.

[-no]-dynlink
Kapag naka-on, i-load ang lahat ng mga dynamic na plug-in na makikita sa path ng paghahanap (tingnan -print-plugin-
landas para sa higit pang impormasyon sa default na landas sa paghahanap). Kung hindi, mga plugin lamang
hiniling ng -load-modules ilo-load. Naka-on ang default na gawi.

-enums repr
Piliin kung paano tinutukoy ang representasyon ng mga enumerated na uri. frama-c
-enums Tulungan nagbibigay ng listahan ng mga magagamit na opsyon. Default ay gcc-enums

-float-digit n
Kapag nag-output ng mga floating-point na numero, ipakita n mga digit. Default sa 12.

-float-flush-to-zero
Ang mga pagpapatakbo ng floating point ay nag-flush sa zero

-float-hex
display floats bilang hexadecimal

-lutang-normal
display floats na may karaniwang Ocaml routine

-float-relative
ipakita ang float interval bilang [ lower_bound++lapad ]

[-no]-force-rl-arg-eval
pinipilit ang kanan pakaliwa na pagkakasunud-sunod ng pagsusuri para sa mga argumento ng mga function na tawag. Kung hindi
ang pagkakasunud-sunod ng pagsusuri ay naiwang hindi tinukoy, tulad ng sa pamantayan ng C. Default sa no.

-journal-disable
Huwag mag-output ng journal ng kasalukuyang session. Tingnan mo -journal-enable.

-journal-enable
Naka-on bilang default, ibina-dump ang isang journal ng lahat ng mga pagkilos na ginawa sa panahon ng kasalukuyang
Frama-C session sa anyo ng isang ocaml script na maaaring i-replay -load-
script. Ang pangalan ng script ay maaaring itakda sa -journal-pangalan pagpipilian.

-journal-pangalan pangalan
Itakda ang pangalan ng journal file (nang walang .ml extension). Default sa
frama_c_journal.

-initialized-padding-locals
Itinatakda ng implicit initialization ng mga lokal ang padding bits sa 0. Kung false, padding bits
ay naiwang hindi nasimulan (default sa oo).

[-no]-keep-comments
Sinusubukang panatilihin ang mga komento kapag medyo nagpi-print ng source code (default sa no).

[-no]-keep-switch
Kailan -pasimplehin-cfg ay nakatakda, pinapanatili ang mga pahayag ng switch. Default sa no.

-keep-unused-specified-functions
Tingnan -remove-unused-specified-functions

[-no]-lib-entry
Ipinapahiwatig na ang entry point ay tinatawag sa panahon ng pagpapatupad ng programa. Ito ay nagpapahiwatig sa
partikular na ang mga pandaigdigang variable ay hindi maaaring ipagpalagay na mayroong kanilang mga paunang halaga.
Ang default ay -walang-lib-entry: ang entry point ay din ang panimulang punto ng
programa at mga global ay may kanilang paunang halaga.

-load file
i-load ang (naunang na-save) na estado na nakapaloob sa file.

-load-module m1[,m2[...,mn]]
naglo-load ng ocaml modules sa pamamagitan ng . Ang mga module na ito ay dapat na .cmxsmga file para sa
katutubong code na bersyon ng Frama-c at .cmoor.cmamga file para sa bersyon ng bytecode (tingnan
ang seksyong Dynlink ng manwal ng Ocaml para sa higit pang impormasyon). Lahat ng mga module na
na naroroon sa mga landas sa paghahanap ng plugin ay awtomatikong na-load.

-load-script s1[,s2,[...,sn]]
nilo-load ang mga script ng ocaml sa pamamagitan ng . Ang mga script ay dapat na .mlmga file. sila
Dapat ay compilable umaasa lamang sa Ocaml standard library at Frama-C's API. Kung
kailangan ang ilang custom na hakbang sa pag-compile, i-compile ang mga ito sa labas ng Frama-C at gamitin
-load-module sa halip.

-machdep makina
Gumagamit makina bilang kasalukuyang configuration na umaasa sa makina (laki ng iba't ibang
mga uri ng integer, endiandness, ...). Ang listahan ng mga kasalukuyang sinusuportahang makina ay
magagamit sa pamamagitan ng -machdep Tulungan opsyon. Default ay x86_32

-pangunahin f
Sets f bilang entry point ng pagsusuri. Default sa 'pangunahing'. Bilang default, ito ay
itinuturing na panimulang punto ng programang sinusuri. Gamitin -lib-entry if f
ay dapat na tinatawag sa gitna ng isang execution.

-kalabuan
nagpi-print ng obfuscated na bersyon ng code (kung saan pinapalitan ang mga orihinal na identifier
sa pamamagitan ng walang kahulugan) at paglabas. Ang talahanayan ng pagsusulatan sa pagitan ng orihinal at bago
ang mga simbolo ay pinananatili sa simula ng resulta.

-ocode file
nire-redirect ang medyo naka-print na code sa file sa halip na karaniwang output.

[-no]-orig-pangalan
Sa yugto ng normalisasyon, maaaring mapalitan ang pangalan ng ilang variable kapag naiiba
variable na may parehong pangalan ay maaaring magkakasamang umiral (hal. isang global variable at isang pormal
parameter). Kapag naka-on ang opsyong ito, may ipi-print na mensahe sa tuwing nangyayari ito.
Default sa no.

[-no]-warn-signed-downcast
bumuo ng mga alarm kapag ang mga naka-sign downcast ay maaaring lumampas sa hanay ng patutunguhan (default sa
hindi).

[-no]-warn-signed-overflow
bumuo ng mga alarma para sa mga nilagdaang operasyon na umaapaw (default sa oo).

[-no]-warn-unsigned-downcast
bumuo ng mga alarma kapag ang mga unsigned downcast ay maaaring lumampas sa hanay ng patutunguhan (default
sa hindi).

[-no]-warn-unsigned-overflow
bumuo ng mga alarma para sa mga hindi napirmahang operasyon na umaapaw (default sa hindi).

[-no]-pp-annot
mga anotasyon bago ang proseso. Ito ay kasalukuyang posible lamang kapag gumagamit ng gcc (o GNU
cpp) pre-processor. Ang default ay hindi paunang iproseso ang mga anotasyon.

[-no]-print
pretty-print ang source code bilang normalized sa pamamagitan ng CIL (defaults sa no).

-print-libpath
output ang direktoryo kung saan naka-install ang Frama-C kernel library

-print-path
alyas ng -print-share-path

-print-plugin-path
output ang direktoryo kung saan hinahanap ng Frama-C ang mga plugin nito (maaaring ma-overidden ng
FRAMAC_PLUGIN variable at ang -add-path option)

-print-share-path
output ang direktoryo kung saan iniimbak ng Frama-C ang data nito (maaaring ma-overidden ng
FRAMAC_SHARE variable)

-remove-unused-specified-functions
nagpapanatili ng mga prototype ng function na may detalye ng ACSL ngunit hindi ginagamit sa
code. Ito ang default. Mga function na may katangian FRAMAC_BUILTIN Palagi
iningatan

-safe-arrays
Para sa mga multidimensional na array o array na mga field sa loob ng structs , ipinapalagay iyon
lahat ng mga pag-access ay dapat na nakatali (nakatakda bilang default). Ang kabaligtaran na opsyon ay -hindi ligtas-
mga dumadating

-iligtas file
Sine-save ang estado ng Frama-C sa file pagkatapos maganap ang mga pagsusuri.

[-no]-simplify-cfg
inaalis ang break, continue at switch statement bago mag-analyze. Default sa no.

-tapos nagbibigay-daan sa isa na bumuo ng mga pagsusuri: isang unang run ng Frama-C ang magaganap kasama ang mga opsyon
bago -tapos at ang pangalawang pagtakbo ay gagawin sa mga opsyon pagkatapos -tapos sa
kasalukuyang proyekto mula sa unang pagtakbo.

-pagkatapos prj
Kapareho ng -tapos maliban na ang pangalawang pagtakbo ay ginanap sa proyekto prj Kung walang ganyan
umiiral ang proyekto, lalabas ang Frama-C nang may error.

-panahon file
idinaragdag ang oras at petsa ng user sa ibinigay file kapag lumabas ang Frama-C.

-typecheck
pinipilit ang pag-typecheck ng mga source file. Ang pagpipiliang ito ay may kaugnayan lamang kung wala nang higit pa
ang pagsusuri ay hinihiling (dahil ang pag-typecheck ay tuwirang magaganap bago ang pagsusuri
ay inilunsad).

-ulevel n
syntactically unroll loops n beses bago ang pagsusuri. Ito ay maaaring medyo magastos
at ilang mga plugin (hal. ang pagsusuri ng halaga) ay nagbibigay ng mas mahusay na mga paraan upang gumanap
ang parehong bagay. Tingnan ang kani-kanilang mga manwal para sa higit pang impormasyon. Maaari din ito
ma-activate sa isang per-loop na batayan sa pamamagitan ng silo pragma hubarin direktiba A
negatibong halaga para sa n ay hahadlang sa gayong mga pragma.

[-no]-unicode
naglalabas ng mga formula ng ACSL na may mga utf8 na character. Ito ang default. Kapag ibinigay ang
-walang-unicode opsyon, gagamitin ng Frama-C ang bersyon ng ASCII sa halip. Tingnan ang manwal ng ACSL
para sa pagsusulatan.

-unsafe-arrays
makita -safe-arrays

[-no]-unspecified-access
mga pagsusuri na nagbabasa/nagsusulat ng mga access na nagaganap sa hindi tinukoy na pagkakasunud-sunod (ayon sa C
standard's notion of sequence point) ay ginaganap sa magkakahiwalay na lokasyon. Sa
-no-unspecified-access, ipinapalagay na ito ay palaging ang kaso (ito ang default).

-version
naglalabas ng string ng bersyon ng Frama-C

-babalaan-decimal-float
nagbabala kapag ang isang floating-point constant ay hindi maaaring eksaktong kinakatawan (hal 0.1).
maaaring isa sa wala, minsan, O lahat

[-no]-warn-undeclared-callee
nagbabala kapag tinawag ang isang function bago ito ideklara (itinakda bilang default).
Frama-C

Plugins tiyak pagpipilian

Para sa bawat isaksak, ang utos

frama-c -isaksak-tulong

ay magbibigay ng listahan ng mga opsyon na partikular sa plugin.

EXIT STATUS

0 Ang matagumpay na pagpapatupad

1 Di-wastong input ng user

2 Pagkagambala ng user (pumatay o katumbas)

3 Hindi naipatupad na tampok

4 5 6 Panloob na error

125 Hindi kilalang error

Ang exit status na mas mataas sa 2 ay maaaring ituring bilang isang bug (o isang feature request para sa case
ng exit status 3) at maaaring iulat sa BTS ng Frama-C (tingnan sa ibaba).

Kapaligiran MGA VARIABLE

Posibleng kontrolin ang mga lugar kung saan hinahanap ng Frama-C ang mga file nito sa pamamagitan ng
sumusunod na mga variable.

FRAMAC_LIB
Ang direktoryo kung saan naka-install ang mga pinagsama-samang interface ng kernel

FRAMAC_PLUGIN
Ang direktoryo kung saan mahahanap ng Frama-C ang mga karaniwang plug-in. Kung nais mong magkaroon ng mga plugin
sa ilang lugar, gamitin -add-path sa halip.

FRAMAC_SHARE
Ang direktoryo kung saan naka-install ang mga data ng Frama-C.

Gumamit ng frama-c.byte online gamit ang mga serbisyo ng onworks.net