回答情况：
提问时间：
问题标签：
我正在用alt-ergo测试程序在frama-c上运行一个测试文件。然而，我得到了下面的alt-ergo错误。所有其他的夫人-c检查都很好。我知道问题不在测试文件中。----------------------------------------------------------------------------我使用了以下说明来安装alt-ergo ()最简单的方法是获取alt-ergo的二进制文件。$ wh
浏览 11修改于2014-09-18得票数 3
回答已采纳
在本例中，使用alt-ergo组合键。
我想知道是否有任何特定的方法可以“转储”给alt-ergo的输入(假设alt-ergo是从frama-c调用的；即不是interop)？我想看看C程序属性的证明义务是如何用alt-ergo的“本机”输入语言编码的。任何帮助都将不胜感激。
浏览 15提问于2019-11-16得票数 1
[wp] [Alt-Ergo 2.3.1] Goal typed_swap_ensures_A : Failed[rte] annotating function swap[wp] [Alt-Ergo2.0.0] Goal typed_swap_assert_rte_mem_access : Failed
Unknown err
浏览 4修改于2020-12-13得票数 1
我正在尝试用Alt-Ergo在一个相当复杂的函数上测试WP插件。不幸的是，我不能弄清楚下面给出的“基本”行为有什么问题。奇怪的是，如果我随意注释一些行，我总是会从Alt-ergo得到“有效”。[wp] Collecting axiomatic usage[wp] 1 goal scheduled
[wp] [Alt-Ergo
浏览 0修改于2014-01-10得票数 0
下面的SMT-LIB代码在Z3，MathSat和CVC4中运行没有问题，但它不能在Alt-Ergo中运行，请让我知道发生了什么，非常感谢：(set-option :
浏览 2修改于2020-04-01得票数 1
回答已采纳
[wp] Collecting axiomatic usage[wp] 4 goals scheduled[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (154ms)[wp]
浏览 4修改于2015-09-04得票数 3
回答已采纳
Cast with incompatible pointers types (source: sint8*) (target: uint8*)[wp] [Alt-Ergo2.2.0] Goal typed_real_main_call_stringCompare_requires_validLengthS1 : Timeout (Qed:2ms) (20s)
[wp] [Alt-Ergo] Goal typed_real_main_call_stringCompare_4_requires_validLeng
浏览 2提问于2020-12-09得票数 6
回答已采纳
2.3.3] Goal typed_array_loop_invariant_2_preserved : Timeout (Qed:43ms) (10s) (cached)<----[wp] [Alt-Ergo2.3.3] Goal typed_array_ensures : Valid (Qed:35ms) (50ms) (52) (cached
浏览 16修改于2020-11-10得票数 1
回答已采纳
1回答
] Goal typed_swap_assign_part2 : Valid (39ms) (21)[wp] [Alt-Ergo] Goal typed_swap_assign_part3 : Valid (30ms) (21) Qed: 2 (0ms-1ms)
Alt-Ergo: 3
浏览 4修改于2014-06-06得票数 4
回答已采纳
: Valid (17ms) (21)[wp]] Goal typed_main_call_search_pre_3 : Valid (383ms) (93)[wp] [Qed] Goal typed_search_loop_assign : Valid
[
浏览 5修改于2016-01-06得票数 4
回答已采纳
Goal typed_f_loop_term_decrease : Valid (4ms)[wp] [Alt-Ergo] Goal typed_f_loop_inv_preserved : Failed当使用键wp-print执行Prover Alt-Ergo returns Failed
Error: Alt-Ergo exit
浏览 2提问于2015-10-17得票数 2
回答已采纳
22:[wp] warning: Missing assigns clause (assigns 'everything' instead)[wp] [Alt-Ergo_2 : Unknown (Qed:2ms) (128ms)[wp] [Alt-Ergo] Goal typed_array_eq
浏览 5修改于2017-07-20得票数 3
回答已采纳
= 0u);这是运行代码后得到的wp输出：[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_ensures :Timeout (Qed:11ms) (10s)rved: Timeout (Qed:9ms) (10s)
[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_assi
浏览 12提问于2022-08-22得票数 1
回答已采纳
都不能证明final_a和post条件，Z3也不能证明循环不变量；# ~/queue $ frama-c -wp -wp-prover alt-ergo test2.c [wp] [Qed] Goal typed_main_loop_assign_part1 : Valid[wp] [Alt-Er
浏览 5提问于2015-07-16得票数 1
回答已采纳
loop.c:20: Warning: Missing assigns clause (assigns 'everything' instead)[wp] [Alt-Ergo2.4.1] Goal typed_f_loop_assigns_part2 : Timeout (Qed:6ms) (10s) (cached)
[wp] [Alt-Ergo 2.4.1] Goaltyped_f_loop_variant_decrease : Timeout (Qed:16ms) (10s) (cac
浏览 12修改于2022-01-14得票数 0
回答已采纳
Parsing test.c (with preprocessing)[wp] 10 goals scheduled[wp] [Alt-Ergo] Goal typed_foo_assign_exit_part3: Unknown (Qed:4ms) (102ms) Qed:
浏览 0修改于2018-11-04得票数 1
回答已采纳
n; i++) { p++; return res;然而，在运行frama-c -wp -wp-prover alt-ergosamenum.c:8: Warning: Missing assigns clause (assigns 'everything' instead)[wp] [Alt-Ergo] Goal typed_max_seq_ensures_2 : Timeout (Qed:1m
浏览 3提问于2020-05-07得票数 0
回答已采纳
*q = tmp;
q++;
}编辑[wp] [Cvc3] Goal store_memswap_loop_inv_6_preserved : Unknown[wp] [Alt-Ergo] Goal store_memswap_loo
浏览 11修改于2013-10-04得票数 2
回答已采纳
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号