Frama C snapshot

Frama-C é uma plataforma dedicada à análise do código-fonte escrito em C.

NOTA: O repositório oficial do Frama-C está agora em nosso Gitlab!

A Frama-C mudou seu repositório oficial para nossa instância do Gitlab auto-hospedado.

Os lançamentos oficiais (a partir do Frama-C 21) não serão mais atualizados aqui.

Instantâneos noturnos também estão disponíveis em nosso Gitlab! Agora você pode ter acesso à versão mais recente de desenvolvimento em: https://git.frama-c.com/pub/frama-c/-/tree/master

O rastreador oficial de edição do Frama-C está agora em nosso gitlab: https://git.frama-c.com/pub/frama-c/-/isissues

Você pode enviar questões e obter solicitações usando seu login do GitHub (escolha "Faça login com o GitHub" quando solicitado).

Vejo você lá!

Uma plataforma colaborativa

O Frama-C reúne várias técnicas de análise em uma única plataforma colaborativa, consistindo em um kernel que fornece um conjunto principal de recursos (por exemplo, um AST normalizado para programas C) mais um conjunto de analisadores, chamados plug-ins . Os plug-ins podem criar resultados calculados por outros plug-ins na plataforma.

Graças a essa abordagem, o Frama-C fornece ferramentas sofisticadas, incluindo:

• um analisador baseado na interpretação abstrata, destinada a verificar a ausência de erros de tempo de execução ( EVA );
• uma estrutura de prova de programa com base no cálculo da pré -condição mais fraco ( WP );
• um slicer de programa ( fatiamento );
• uma ferramenta para verificação das propriedades temporal (LTL) ( AORAï );
• uma ferramenta de verificação de tempo de execução ( e-ACSL );
• Várias ferramentas para análise de exploração e dependência da base de código ( de , impacto , métricas , ocorrência , escopo , etc.).

Esses plug-ins compartilham um idioma comum e podem trocar informações por meio de propriedades ACSL ( ANSI/ISO C Specification Language ). Os plug-ins também podem colaborar por meio de suas APIs.

Instalação

Para obter informações mais detalhadas sobre a instalação do OPAM/FRAMA-C, consulte o Install.md.

O Frama-C está disponível através do Opam, o gerente de pacotes da OCAML. Este é o método de instalação preferido. Certifique -se de instalar Opam v2.0 ou superior. Em seguida, a seguinte sequência de comandos deve instalar o Frama-C e sua GUI:

 opam init
opam install depext
opam depext frama-c
opam install frama-c

O Frama-C é desenvolvido principalmente no Linux, geralmente testado no macOS (via homebrew) e, ocasionalmente, testado no Windows (através do subsistema do Windows para Linux).

Uso

O Frama-C pode ser executado a partir da linha de comando ou através de sua interface gráfica.

Uso simples

O uso recomendado para arquivos simples é uma das seguintes linhas:

 frama-c file.c -<plugin> [options]
frama-c-gui file.c

Onde -<plugin> é um dos vários plug -ins Frama -C, por exemplo, -eva , ou -wp , ou -metrics , etc. Os plug -ins também podem ser executados diretamente da GUI.

Para listar todos os plug-ins, execute:

 frama-c -plugins

Cada plug-in possui um comando de ajuda ( -<plugin>-help ou- -<plugin>-h ) que descreve suas várias opções.

Finalmente, a lista de opções que regem o comportamento do próprio kernel de Frama-C está disponível

 frama-c -kernel-help

Cenários complexos

Para cenários de uso mais complexos (muitos arquivos e diretórios, com várias diretivas de pré-processamento), recomendamos dividir o uso do Frama-C em duas partes:

1. Analisar os arquivos de entrada e salvar o resultado em um arquivo;
2. Carregando os resultados da análise e depois executando as análises ou a GUI.

A análise geralmente envolve dar argumentos extras ao pré-processador C; portanto, a opção -cpp-extra-args geralmente é útil, como no exemplo abaixo:

 frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

Os resultados são então carregados no Frama-C para análises posteriores ou para inspeção via GUI:

 frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

Referência adicional

• Links para manuais de usuários e desenvolvedores, arquivos Frama-C e manuais de plug-in estão disponíveis em
  http://frama-c.com/download.html

• O Stackoverflow tem várias perguntas com a etiqueta frama-c , que é monitorada por vários membros da comunidade Frama-C.

• A lista de discussão Frama-C-Discuss é usada para anúncios e discussões em geral.

• O sistema oficial de rastreamento de bugs pode ser usado para relatórios de bugs.

• O Wiki Frama-C tem algumas informações úteis, embora não esteja totalmente atualizado.

• O blog Frama-C tem várias postagens sobre novos desenvolvimentos do Frama-C, bem como discussões gerais sobre o idioma C, comportamento indefinido, cálculos de ponto flutuante etc.

• O repositório de instantâneos do github contém os arquivos .tar.gz de lançamentos estáveis ​​de Frama-C, prontos para serem clonados. Também pode ser usado para relatar problemas e enviar solicitações de puxar.