这是可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行的命令 spark,例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序:
您的姓名
spark - 检查 SPARK 程序并生成验证条件
概要
火花 [选项] [ FILE_LIST 或 @METAFILE ]
商品描述
SPARK的考官, 火花, 分析给定的源文件中的错误和违规
SPARK 子集和(可选)生成验证条件和死路
证明不存在运行时异常和部分正确性所必需的猜想。
本手册页仅总结了 火花 命令行标志,请参阅完整
考官手册以获取更多信息。
配置
这些选项并不完全遵循通常的 GNU 命令行语法。 所有选项开始
用一个破折号代替通常的两个破折号,它们也可以缩写,只要
缩写是唯一的。 例如 -救命 可以缩写为 -他 但不 -h 这样
与发生冲突 -html.
-源扩展名=文件类型
指定源文件扩展名(默认'ada')
-无索引文件, -索引文件=文件规格
指定索引文件。 默认情况下不使用索引文件。
-nowarning_file, -警告文件=文件规格
指定警告控制文件。 默认情况下不使用警告控制文件。
-无配置文件, -配置文件=文件规格
指定 Examiner 配置文件。 默认没有配置文件
用过的。
-无开关
忽略 spark.sw 文件(如果存在)。
-不上榜, -列表扩展名=文件类型
默认情况下,所有列表文件都具有“lst”扩展名。 这些选项可用于
禁用列表文件生成或更改默认扩展名。
-noreport_file, -报告文件=文件规格
默认情况下,报告将命名为“SPARK.REP”。 这些选项可用于
更改默认名称或禁用报告生成。
-html, -html=目录规格
生成 HTML 列表和报告文件。
-输出目录=目录规格
在指定目录中生成报告、清单和证明文件。
-plain_output
输出文件中不会出现日期、行号或错误号。
-语言=L
这可以是 83、95(默认值)或 2005 之一。
-个人资料=P
在顺序(默认)或 ravenscar 语言配置文件之间进行选择。
-结节
不要预定义 Standard.Duration。
-语法检查
仅执行语法检查。 没有语义检查。
-流分析=型
在信息或数据之间进行选择。
-政策=型
为流分析选择安全或安全策略。
-VCG 生成 VC。
-dpc 生成 DPC。
-规则=选择
选择生成复合常数证明规则的策略。 可以是其中之一
(默认)、懒惰、敏锐或全部。
-注释字符=CHAR
选择替代注释字符。 默认值为“#”。
-诺回声
抑制屏幕输出。
-诺斯利 不要生成 SLI 文件。
-sparklib
使用标准的 SPARK 库。
-统计, -统计
将 Examiner 表使用统计信息附加到报告文件中。 默认情况下我们不做
本。
-fdl_标识符=OPTION
在 SPARK 源中发现 FDL 标识符时控制处理。 可以是其中之一
“拒绝”(默认)或“接受”或.
-版
打印 Examiner 横幅和统计数据,然后退出。
-救命 打印命令行摘要和选项。
-原始流程错误
以原始的、不太紧凑的格式打印信息流错误。
-错误解释=设置
在错误消息后打印说明。 设置可以关闭(默认),
first_occurrence 或 every_occurrence。
-理由选项=型
选择政策来证明错误。 值可以是完整的(默认)、简短的
或忽略。
-套管, -套管=选择
检查外壳以获取标识符参考并检查包装标准的外壳
身份标识。 也可以指定 i 或 s 以仅检查其中之一。
使用 onworks.net 服务在线使用 spark