小编BHM*_*BHM的帖子

我想用 Frama-c 和 WP 插件来表示，下面编写的 stringCompare 函数充当“它应该”的作用 - 即：给定相同的输入字符串，该函数返回 0 并且结果不同于 0如果字符串不相同。我已经注释了如下所示的相关函数，并希望能够证明 WP 生成的未经证实的目标，这怎么做？

我通过尝试运行带有注释的插件获得的输出可以在代码下方看到

#include <string.h>
#include <stdio.h>

/*@  
    requires validPointers: \valid_read(s1) && \valid_read(s2) ;
    requires validLengthS1: 100 >= strlen(s1) >= 0;
    requires validLengthS2: 100 >= strlen(s2) >= 0;
    assigns \nothing ;
    allocates \nothing ;  
    frees \nothing ;
    behavior allEqual:
        assumes \forall integer k; 0 <= k < n ==> s1[k] == s2[k];
        ensures \result == 0;
    behavior SomeDifferent:
        assumes \exists integer k; 0 <= k < n ==> …