问题标签 [program-slicing]

我从 Frama-c 得到一个后向切片，但看起来它是一个静态切片而不是动态切片。

frama-c 中是否有特定选项来获得动态后向切片？

我正在尝试在特定位置对数组元素执行反向切片。我尝试了两种不同的源代码。第一个是（first.c）：

我运行命令：

frama-c-gui -slevel 10 -val -slice-return 主文件.c

并获得以下生成的代码：

这似乎没问题，因为 x 和 y 没有定义，所以“res”可以在 out_array 中的任何位置。然后我尝试使用以下代码：

给出的结果完全相同。但是，由于我明确地在数组中寻找特定位置，并且循环是独立的（可并行化的），我希望输出是这样的：

我不确定这些例子是否清楚。我想要做的是确定，对于给定的数组位置，哪些语句会影响其最终结果。提前感谢您的任何支持。

从我读到的Indus是一个程序切片器，它识别程序的哪些部分影响或受给定程序点集的影响，而Kaveri是一个插件，它利用 Indus 程序切片库在 eclipse 中执行切片。

我从这个链接http://forge.cis.ksu.edu/frs/?group_id=12下载了一个 zip， 但我不知道如何使用它。我想知道如何使用这个插件？

我刚开始使用 Wala Java Slicer 做一些源代码分析任务。我对图书馆的正确使用有疑问。假设我有以下示例代码：

用 Wala计算语句的切片println给出以下语句：

我使用 Wala 创建切片的代码如下所示：

我希望在切片中找到许多语句但不存在：

• ut = userType即使从属方法调用ut.getInt()IS 包含在切片中，assign 语句也不包含在内
• 不包括来自实现的语句getInt()。是否有激活“程序间”切片的选项？我应该在这里提到 .class 文件包含在用于创建 .class 文件的路径中AnalysisScope。

如您所见，我使用DataDependenceOptions.NO_BASE_NO_HEAPandControlDependenceOptions.NONE作为依赖选项。但即使我同时使用FULL两者，问题仍然存在。

我究竟做错了什么？

我刚刚开始使用 Soot 以编程方式分析 .java 文件。根据我的阅读，Soot 似乎是一个非常强大的源代码分析工具，但我在网上找到的大多数材料都在谈论将它用作命令行工具。

我需要以编程方式从给定目录中的 .java 文件加载类，构建程序依赖图 (PDG) 并执行一些程序切片。我仍然不确定 Soot 是否提供切片，但我可以在拥有 PDG 后自己实现。

首先，我尝试使用以下代码：

但是，它不起作用。它在通话中卡住loadClassAndSupport了几秒钟，然后我的程序突然存在，没有给出任何异常或任何东西。

如果有人尝试以编程方式使用 Soot，我还需要设置其他选项吗？或者你能告诉我他们从头开始以编程方式设置 Soot 的教程吗？

给定一个 C 文件，我想计算某些标准的后向切片并将切片与原始代码进行比较。因为我不想从头开始实现切片程序，所以我已经尝试习惯 Frama-C，这似乎有助于完成这项任务。

但是，我的问题是，Frama-C 的切片插件更改了预处理的输入代码，因此更难识别原始的哪些行也出现在切片中。

例子：

输入文件test1.c：

预处理文件（由 产生frama-c test1.c -print -ocode test1_norm.c）：

切片（由 产生frama-c -slice-calls func1 test1.c -then-on 'Slicing export' -print）：

请注意，签名main不同，并且名称func1已更改为func1_slice_1。

有没有办法抑制这种行为，以使切片和（预处理的）原始文件更容易比较（就可计算的差异而言）？

有没有办法使用Frama-Cslicing 插件来计算特定 Cassert语句的切片？

例如，给定以下代码：

我想得到以下切片assert(b>=0);：

是否可以使用Frama-C's 切片插件来切片多个断言？

例如，给出以下代码：

我想获得两个断言的切片。

我在 Prolog 中有以下代码，问题是当我运行代码时，它为每个数据返回相同的结果。

KB 在另一个文件中并加载它，并在开始谓词中我加载了 patient3，例如它应该返回

请注意，开始谓词仅用于检查代码现在是否正常工作！当我使用跟踪运行此文件时，它显示首先尝试第一个规则。当它尝试转到另一个规则时，它在check_RTC中失败，谓词症状返回symbolNeg ..但是为什么？它应该从一开始就获取所有数据并检查下一条规则，直到找到不会失败的规则。

kb代码文件是

我正在尝试在 Prolog 中解决以下问题，并且我认为我的编码是正确的，但是我的查询只是返回 false。关于改变什么的任何建议？问题如下：

“Bagel Alley 是当地的百吉饼店，在早上上下班途中总是热闹非凡，因为人们在上班路上停下来买咖啡和百吉饼。每天早上在现场新鲜制作，百吉饼非常受欢迎，而且事实上，这家店的咖啡也很棒，简直是锦上添花！在 Bagel Alley 工作的人都很开朗友好，而且能干，所以尽管顾客数量众多，但等待的时间从不漫长或不愉快。乔和他的四个同事今天早上过来看看大家都在说什么，惊喜地发现这家店名不虚传。确定每个同事的名字，什么样的百吉饼配上馅料，味道和大小每个点的咖啡（小、中或大）。”

1. 布拉德拿到了他的百吉饼，不是小麦，上面什么都没有。沃尔特点了一杯咖啡。

2. 得到中型咖啡的两个同事一个得到了榛子味，另一个得到了他的百吉饼加花生酱。

3. 得到洋葱百吉饼但没有加黄油的人还得到了法国香草咖啡，但不是小尺寸。

4. 五个同事是乔，一个是大杯咖啡，一个是杏仁味咖啡，一个是小麦百吉饼，还有一个是在百吉饼上放鸡蛋和培根。

5. 里克没有点蓝莓百吉饼，但他点了哥伦比亚咖啡。Amaretto 咖啡是和切达面包圈一起点的，但不是 Walt 点的。

6. 奶油芝士没有配蓝莓百吉饼，但配了一大杯咖啡。芝麻百吉饼配黄油，但卡洛斯没有点。

我写的Prolog代码在这里：

我相信运行查询“百吉饼（X）”。应该给我解决问题的方法，但它返回错误。我错过了什么吗？提前谢谢了！