问题描述
|
AVM验证程序遇到错误时，将写入闪存日志。在文档中，它说验证者将访问“所有可能的分支”，而跳转可能会通过它。但是，在尝试跟踪输出时仍然令人困惑。有什么想法如何正确解释它？整个流程似乎令人困惑。
例如，以下标记的含义是什么。
合并第一
合并电流
合并目标
合并后
此外，还有带有寄存器，作用域堆栈和操作数堆栈的机器指令和机器状态。我了解指令后又修改了状态，例如PushFalse会使布尔值出现在操作数堆栈-（Boolean [B]）上。但是有时甚至在没有指令的情况下也将状态与MERGE FirsT，MERGE CURRENT等结合起来写入。这是什么意思？
解决方法
不幸的是，这是我在那里可以找到的最全面的解释。
http://hg.mozilla.org/tamarin-redux/file/3c8d01c7b51a/doc/verifier.txt