Frama-C
 | |
| Utvecklare | Commissariat à l'Énergie Atomique ( CEA-List ) och Inria |
|---|---|
| Förvar | |
| Skrivet i | OCaml |
| Operativ system | Microsoft Windows , FreeBSD , OpenBSD , Linux , Mac OS X |
| Tillgänglig i | engelsk |
| Typ | Formell verifiering , statisk kodanalys |
| Licens | mestadels LGPL , vissa delar under BSD-licenser |
| Hemsida | |
Frama-C står för Framework for Modular Analysis of C-programs . Frama-C är en uppsättning interoperabla programanalysatorer för C-program . Frama-C har utvecklats av det franska Commissariat à l'Énergie Atomique et aux Énergies Alternatives ( CEA-List ) och Inria . Den har också fått finansiering från Core Infrastructure Initiative . Frama-C, som en statisk analysator , inspekterar program utan att köra dem. Trots sitt namn är programvaran inte relaterad till det franska projektet Framasoft .
Arkitektur
Frama-C har en modulär plugin-arkitektur som är jämförbar med Eclipse (programvara) eller GIMP .
Frama-C förlitar sig på CIL ( C Intermediate Language ) för att generera ett abstrakt syntaxträd . Det abstrakta syntaxträdet stöder kommentarer skrivna i ANSI/ISO C Specification Language (ACSL).
Flera moduler kan manipulera det abstrakta syntaxträdet för att lägga till ANSI/ISO C Specification Language ( ACSL) annoteringar. Bland ofta använda [ vaga ] plugins är:
- Värdeanalys – beräknar ett värde eller en uppsättning möjliga värden för varje variabel i ett program. Detta plugin använder abstrakta tolkningstekniker och många andra plugins använder sig av dess resultat.
- Jessie – verifierar egenskaper på ett deduktivt sätt. Jessie förlitar sig på varför eller Why3 back-end för att möjliggöra bevisförpliktelser att skickas till automatiska teoremprovare som Z3, Simplify, Alt-Ergo eller interaktiva teoremprovare som Coq eller Why. Med hjälp av Jessie en implementering av bubble-sort eller ett leksaks-e-röstningssystem bevisas uppfylla deras respektive specifikationer. Den använder en separationsminnesmodell inspirerad av separationslogik .
- WP (Weakest Precondition) – liknande Jessie , verifierar egenskaper på ett deduktivt sätt. Till skillnad från Jessie fokuserar den på parametrering med avseende på minnesmodellen. WP är designat för att samarbeta med andra Frama-C-plugins som till exempel värdeanalysplugin, till skillnad från Jessie som kompilerar C-programmet direkt till Why-språket. WP kan valfritt använda Why3-plattformen för att anropa många andra automatiserade och interaktiva provare.
- Konsekvensanalys – belyser effekterna av en ändring i C-källkoden.
- Slicing – möjliggör skivning av ett program . Det möjliggör generering av ett mindre nytt C-program som bevarar vissa givna egenskaper.
- Reservkod – tar bort värdelös kod från ett C-program.
Andra plugins är:
- Dominatorer – beräknar dominatorer och postdominatorer av uttalanden.
- Från analys – beräknar funktionella beroenden.
Funktioner
Frama-C kan användas för följande ändamål:
- För att förstå C-kod som du inte har skrivit. Frama-C gör det särskilt möjligt att observera en uppsättning värden, dela upp programmet i kortare program och navigera i programmet.
- För att bevisa formella egenskaper på koden. Genom att använda specifikationer skrivna i ANSI/ISO C Specification Language kan det säkerställa kodens egenskaper för eventuellt beteende. Frama-C hanterar flyttal.
- För att upprätthålla kodningsstandarder eller kodkonventioner på C-källkod, med hjälp av anpassade plugin(s)
- Att instrumentera C-kod mot vissa säkerhetsbrister