如何在另一个插件中使用WP的结果? [英] How do I use the results of WP in another plug-in?

问题描述

我正在编写一个Frama-C插件，我想知道是否有可能从我的插件中使用WP获得最弱的先决条件，如果可以，那么到底是什么?过去，例如，我曾使用Db.Value在自己的插件中使用EVA插件的结果.是否有类似于WP的Db.Value的东西?

I am working on writing a Frama-C plug-in and I would like to know if it is possible to get the weakest precondition of something using WP from within my plug-in, and if so, how exactly? In the past I've used Db.Value, for example, to use the results of the EVA plug-in in my own plug-in. Is there something similar to Db.Value for WP?

推荐答案

WP插件在WP.mli文件中公开其API，该文件是通过收集组成Wp的更高级别模块的接口而生成的.您可以在src/plugins/wp/Wp.mli中找到它.

The WP plugin exposes its API in the WP.mli file, that is generated by collecting the interfaces of the higher-level modules composing Wp. you can find it in src/plugins/wp/Wp.mli.

但是，您应该意识到，此API不应被认为是稳定的，并且在较新的Frama-C版本中可能会引入非向后兼容的更改.

However, you should be aware that this API should not be considered stable, and non-backward compatible changes may be introduced in newer Frama-C versions.

这篇关于如何在另一个插件中使用WP的结果?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！