小编Trú*_*Lâm的帖子

我正在尝试使用Z3的HORN逻辑(set-logic HORN)对一些命令式程序进行编码,但是在定义子句时遇到了一些困难(使用SMT2).谁能告诉我在哪里可以找到Z3这个功能的良好文档来源？

我正在学习如何建立解析用C工具libtooling的叮当声。

我正在使用一个RecursiveASTVisitor-inherited 类，所以它的所有 traverse 和visitor 方法都可用。我想知道在覆盖 method 时是否可以确定语句的父函数节点VisitStmt(Stmt *s)。例如在这里，我可以FunctionDecl*从s?

谢谢。

我不太了解slevelFramaC中的选项.任何人都可以解释更多关于如何与slevel用户断言(例如//@assert ...;)或状态相关的价值,以及导致状态数量上升的因素有哪些？

例如,我有一个程序,它不包含循环,但包含if..else分支,go to语句,并且在程序的某些点上也有一些用户断言,例如:

...
a = Frama_C_unsigned_int_interval(0, 100);
//@ assert a == 0 || a == 1 || a == 2 || a == 3 || ... || a == 100;
...
b = Frama_C_unsigned_int_interval(a, 200);
//@ assert b == 0 || b == 1 || b == 2 || b == 3 || ... || b == 200;
...

在分析的输出中(我设置slevel为~100000),可能有一些像:Semantic level unrolling superposing up to …