frama-c.byte - 云端在线

程序：

您的姓名

frama-c[.byte] - C 程序的静态分析器

frama-c-gui[.byte] - frama-c 的图形界面

概要

框架-c [ 选项 ] 档

商品描述

框架-c 是一套专门用于分析用 C 编写的源代码的工具。
在单个协作框架中收集多种静态分析技术。 这个
框架可以通过放置在框架中的附加插件进行扩展 $FRMAC_PLUGIN 目录。
命令

框架-c-帮助

将提供当前安装的插件的完整列表。

框架-c-gui 是图形用户界面 框架-c. 它具有与以下相同的选项
命令行版本。

帧-c.byte 和 frame-c-gui.byte 是命令行的 ocaml 字节码版本和
分别为图形用户界面。

默认情况下，Frama-C 识别 .c 文件作为 C 文件需要预处理和 .i 文件为
C 文件已经过预处理。 某些插件可能会扩展已识别的列表
文件。 预处理可以通过定制 -cpp-命令 和 -cpp-额外参数
选项​​。

配置

句法

带附加参数的选项也可以写在形式下

-选项=停止

这个选项是强制性的，当 停止 以破折号 ('-') 开头

大多数不带参数的选项都有相应的

-没有-选项

具有相反效果的选项。

政策和帮助 选项

-救命 给出简短的使用通知和已安装插件的列表。

-内核帮助
打印 Frama-C 内核识别的选项列表

-冗长 n
设置详细级别（默认为 1）。 将其设置为 0 将输出较少的进度
消息。 这个级别也可以设置在每个 插入 基础，带选项 -插入-
详细 n. 内核的详细级别可以通过选项控制
-内核详细 n.

-调试 n
设置调试级别（默认为 0，表示没有调试消息）。 这个选项
具有与每个插件（和内核）相同的专业化 -冗长.

-安静的 将详细程度和调试级别设置为 0。

附加选项 控制 Frame-C 的 核心

-绝对有效范围
认为范围内的所有数字地址 最小-最大 是有效的。 界限是
解析为 ocaml 整数常量。 默认情况下，所有数字地址都是
视为无效。

-添加路径 p1[,p2[...,pn]]
添加目录 通过 到插件所在的目录列表
搜索

[-no]-允许重复
允许在测试和循环的规范化期间复制小块。
否则，规范化使用标签和 goto。 更大的块和带有非
琐碎的控制流永远不会重复。 默认为是。

[-no]-注释
读取 ACSL 注释。 这是默认设置。 注释不被预处理
默认。 用 -pp-注释 对于这一点。

-大整数十六进制 最大
大于的整数 最大 以十六进制显示（默认情况下，所有整数都是
以十进制显示）

-检查 对内部 AST 执行完整性检查（仅限开发人员）。

[-no]-折叠-呼叫-投射
允许在函数返回的值和它的左值之间进行隐式转换
分配给。 否则，将使用临时变量并显式进行强制转换。
默认为是。

[-no]-constfold
在分析之前折叠代码中的所有语法常量表达式。 默认值
没有。

[-no]-继续注释错误
分析注释时，默认行为（ -没有 此选项的版本）
当发生类型检查错误时拒绝源文件，就像
C 代码中的类型检查错误。 启用此选项后，类型检查器将
只输出警告并丢弃注释但类型检查将继续
（不过，C 代码中的错误仍然是致命的）。

-cpp-命令 CMD
使用 CMD 作为预处理 C 文件的命令。 默认为 CPP 环境
变量或

gcc -C -E -I。

如果没有设置。 为了保留 ACSL 注释，预处理器必须保留
评论（ -C gcc 的选项）。 %1 和 %2 可用于 CMD 表示
分别为原始源文件和预处理文件

-cpp-额外参数 ARGS
为预处理器提供额外的参数。 这仅在以下情况下有用
-预处理注释 设置。 预处理注释在两个单独的预处理中完成
处理阶段。 第一个是对保留宏的 C 代码的正常传递
定义。 然后在第二遍中使用它们，在此期间注释被
预处理。 ARGS 仅用于第一遍，因此参数
不应使用两次（例如附加的包含指令或宏
定义）因此必须去那里而不是 -cpp-命令.

[-no]-动态链接
启用时，加载在搜索路径中找到的所有动态插件（请参阅 -打印插件-
径 有关默认搜索路径的更多信息）。 否则，只有插件
被要求 -加载模块 将被加载。 默认行为已开启。

-枚举 代表
选择确定枚举类型表示的方式。 框架-c
-枚举 帮助 给出可用选项的列表。 默认是 gcc 枚举

-浮点数 n
输出浮点数时，显示 n 数字。 默认为 12。

-float-flush-to-XNUMX
浮点运算清零

-浮动十六进制
以十六进制显示浮点数

-浮动正常
使用标准 Ocaml 例程显示浮动

-浮动相对
将浮点间隔显示为 [ 下界++宽度 ]

[-no]-force-rl-arg-eval
强制函数调用的参数从右到左求值顺序。 除此以外
评估顺序未指定，就像在 C 标准中一样。 默认为否。

- 日志禁用
不输出当前会话的日志。 看 -期刊启用.

-期刊启用
默认情况下，转储当前执行的所有操作的日志
可以重播的 ocaml 脚本形式的 Frama-C 会话 -加载-
脚本. 脚本的名称可以用 -期刊名称 选项。

-期刊名称 姓名
设置日志文件的名称（不带 .ml 延期）。 默认为
frama_c_journal。

-初始化填充本地
局部变量的隐式初始化将填充位设置为 0。如果为 false，则填充位
未初始化（默认为是）。

[-no]-保留评论
在漂亮地打印源代码时尝试保留注释（默认为 no）。

[-no]-保持开关
什么时候 -简化-cfg 已设置，保留 switch 语句。 默认为否。

-保留未使用的指定功能
我们 -删除未使用的指定功能

[-no]-lib 入口
表示在程序执行期间调用入口点。 这意味着在
特别是不能假设全局变量有它们的初始值。
默认是 -无库条目: 入口点也是起点
program 和 globals 有它们的初始值。

-加载 文件
加载（以前保存的）状态包含在 文件.

-加载模块 m1[,m2[...,mn]]
加载 ocaml 模块 通过 . 这些模块必须 .cmxs的文件
Frama-c 的本机代码版本和 .cmoor.cma字节码版本的文件（见
有关更多信息，请参阅 Ocaml 手册的 Dynlink 部分）。 所有模块
出现在插件搜索路径中会自动加载。

-加载脚本 s1[,s2,[...,sn]]
加载 ocaml 脚本 通过 . 脚本必须是 .ml文件。 他们
必须仅依赖 Ocaml 标准库和 Frama-C 的 API 即可编译。 如果
需要一些自定义编译步骤，在 Frama-C 之外编译它们并使用
-加载模块 代替。

-马赫德普 机
使用 机 作为当前依赖于机器的配置（各种大小
整数类型，字节序，...）。 当前支持的机器列表是
通过 -马赫德普 帮助 选项。 默认是 x86_32

-主要 f
套数 f 作为分析的切入点。 默认为“主要”。 默认情况下，它是
被视为正在分析的程序的起点。 用 -lib 入口 if f
应该在执行过程中调用。

-混淆
打印代码的混淆版本（其中原始标识符被替换
通过无意义的一个）并退出。 原厂与新厂对应表
符号保留在结果的开头。

-o代码 文件
将漂亮打印的代码重定向到 文件 而不是标准输出。

[-no]-原名
在规范化阶段，某些变量可能会在不同时重命名
同名变量可以共存（例如全局变量和形式变量）
范围）。 当此选项打开时，每次发生这种情况时都会打印一条消息。
默认为否。

[-no]-警告-签名-沮丧
当签名向下转换可能超出目标范围时生成警报（默认为
不是）。

[-no]-警告签名溢出
为溢出的签名操作生成警报（默认为是）。

[-no]-警告-未签名-向下转型
当无符号向下转换可能超出目标范围时生成警报（默认
不）。

[-no]-警告无符号溢出
为溢出的未签名操作生成警报（默认为 no）。

[-no]-pp-注释
预处理注释。 目前只有在使用 gcc（或 GNU
cpp) 预处理器。 默认是不预处理注释。

[-no]-打印
漂亮地打印由 CIL 规范化的源代码（默认为 no）。

-打印libpath
输出安装Frama-C内核库的目录

-打印路径
别名 -打印共享路径

-打印插件路径
输出 Frama-C 搜索其插件的目录（可以被覆盖
FRAMAC_插件 变量和 -添加路径 选项​​）

-打印共享路径
输出 Frama-C 存储其数据的目录（可以被覆盖
FRAMAC_分享 多变的）

-删除未使用的指定功能
保留具有 ACSL 规范但未在
代码。 这是默认设置。 具有属性的函数 FRAMAC_内置 总是
保留。

-安全数组
对于多维数组或结构中字段的数组，假设
所有访问都必须绑定（默认设置）。 相反的选择是 -不安全-
数组

-节省 文件
将 Frama-C 的状态保存到 文件 分析完成后。

[-no]-简化-cfg
在分析之前删除 break、continue 和 switch 语句。 默认为否。

-然后 允许一个人进行分析：第一次运行 Frama-C 将与选项一起发生
before -然后 之后将使用选项进行第二次运行 -然后 在
第一次运行的当前项目。

-然后-打开 PRJ
像 -然后 除了第二次运行是在项目中进行的 PRJ 如果没有这样的
项目存在，Frama-C 退出并出现错误。

-时间 文件
在给定的内容中附加用户时间和日期 文件 当 Frama-C 退出时。

-类型检查
强制对源文件进行类型检查。 此选项仅在没有进一步的情况下才相关
请求分析（因为类型检查将在分析之前隐式发生
启动）。

-ulevel n
从句法上展开循环 n 分析之前的时间。 这可能非常昂贵
和一些插件（例如价值分析）提供了更有效的方式来执行
同样的事情。 有关更多信息，请参阅它们各自的手册。 这也可以
通过在每个循环的基础上激活 循环 编译 展开 指示。 一种
负值 n 将抑制此类编译指示。

[-no]-unicode
输出带有 utf8 字符的 ACSL 公式。 这是默认设置。 当给出
-无unicode 选项，Frama-C 将使用 ASCII 版本代替。 请参阅 ACSL 手册
为对应。

-不安全数组
看到 -安全数组

[-no]-未指定访问
检查以未指定顺序发生的读/写访问（根据 C
标准的序列点概念）在不同的位置执行。 和
-没有未指定的访问权限, 假定情况始终如此（这是默认设置）。

-版
输出 Frama-C 的版本字符串

-警告十进制浮点数
当浮点常量无法准确表示时发出警告（例如 0.1）。
可以是其中之一 没有, 一旦或 所有

[-no]-警告未声明的被调用者
在声明之前调用函数时发出警告（默认设置）。
框架-C

插件 具体的 选项

对于每一个 插入， 命令

框架-c -插入-救命

将给出特定于插件的选项列表。

退出 状态

0 成功执行

1 无效的用户输入

2 用户中断（杀死或等效）

3 未实现的功能

4 5 6 内部错误

125 未知错误

大于 2 的退出状态可以被认为是一个错误（或案例的功能请求
退出状态 3) 并且可能会在 Frama-C 的 BTS 上报告（见下文）。

环境 变数

可以通过以下方式控制 Frama-C 查找其文件的位置
以下变量。

FRMAC_LIB
内核编译接口的安装目录

FRAMAC_插件
Frama-C 可以找到标准插件的目录。 如果你想要插件
在几个地方，使用 -添加路径 代替。

FRAMAC_分享
Frama-C 数据的安装目录。

使用 onworks.net 服务在线使用 frama-c.byte