在 frama-c.21.1 中找不到一些标志
Can't find some flags in frama-c.21.1
我想使用 frama-c 作为分析器来检查 C 源代码是否有未定义的行为。我在 here 找到了 C-Reduce 提供的代码。但是，这个脚本中的一些标志我在新版本的frama-c中找不到。
我找不到的标志列表如下：
- -第一次报警时停止
- -精确并集
我可以在 github
上的 frama-c 更新日志中找到其他内容
但无论如何，我找不到一些标志，甚至是一点描述。
我担心标志“-precise-unions”，因为它似乎要检查并集。虽然“-stop-at-first-alarm”似乎可以节省时间。
我找到了一个代码 here，该代码没有使用任何已更改的标志。但它是正确的吗？
我真的不知道。
谢谢你的好意。
选项 -stop-at-first-alarm 已替换为更通用的 -eva-stop-at-nth-alarm 1。如果您愿意，可以用更大的数字替换 1。它所做的是在发出 nth 警报后停止分析。如果您的目标是设置 0 个警报并仔细检查每个警报，则此选项可能会节省时间。但是，总的来说，它并没有提高分析的效率。
-precise-unions 是一个非常古老的选项，已在 Frama-C Fluorine (2013) 中废弃。它不再需要。不影响分析的正确性。
您提到的Csmith驱动脚本确实使用了旧选项，但不影响正确性。默认情况下，没有任何选项，Frama-C/Eva 将警告代码中未定义的行为。如果你想比 C 标准更严格（例如禁止无符号溢出），那么你可能需要添加额外的选项，例如 -warn-unsigned-overflow.
我想使用 frama-c 作为分析器来检查 C 源代码是否有未定义的行为。我在 here 找到了 C-Reduce 提供的代码。但是，这个脚本中的一些标志我在新版本的frama-c中找不到。
我找不到的标志列表如下：
- -第一次报警时停止
- -精确并集
我可以在 github
上的 frama-c 更新日志中找到其他内容但无论如何，我找不到一些标志，甚至是一点描述。
我担心标志“-precise-unions”，因为它似乎要检查并集。虽然“-stop-at-first-alarm”似乎可以节省时间。
我找到了一个代码 here，该代码没有使用任何已更改的标志。但它是正确的吗？
我真的不知道。
谢谢你的好意。
选项 -stop-at-first-alarm 已替换为更通用的 -eva-stop-at-nth-alarm 1。如果您愿意，可以用更大的数字替换 1。它所做的是在发出 nth 警报后停止分析。如果您的目标是设置 0 个警报并仔细检查每个警报，则此选项可能会节省时间。但是，总的来说，它并没有提高分析的效率。
-precise-unions 是一个非常古老的选项，已在 Frama-C Fluorine (2013) 中废弃。它不再需要。不影响分析的正确性。
您提到的Csmith驱动脚本确实使用了旧选项，但不影响正确性。默认情况下，没有任何选项，Frama-C/Eva 将警告代码中未定义的行为。如果你想比 C 标准更严格（例如禁止无符号溢出），那么你可能需要添加额外的选项，例如 -warn-unsigned-overflow.