I am trying to verify the above with Frama-C. From the manuals, it seems like Frama-C isn't well suited for malloc, and function pointers. I was wondering if I am missing something in my verification conditions, or Frama-C isn't well suited to handle lists? The output is for Alt-Ergo solver.
#include <stdlib.h>
typedef struct _list {
int key;
struct _list *next;
} list; //defined list
/*@
inductive reachable{L} (list* root, list* node) {
case root_reachable{L}: \forall list* root; reachable(root,root);
case next_reachable{L}: \forall list* root, *node; \valid(root) && reachable(root->next,node) ==> reachable(root,node) ;
} */
/*@inductive samelist{L} (list* l1, list* l2) {
case base_same{L}: \forall list* l1, *l2; l1 == \null && l2 == \null;
case next_same{L}: \forall list* l1, *l2; \valid(l1) && \valid(l2) && \separated(l1, l2)
&& l1->key == l2->key && samelist(l1->next,l2->next) ==> samelist(l1,l2) ;
} */
/*@ predicate finite{L}(list* root) = reachable(root,\null); */
/*@
axiomatic Length {
logic integer length{L}(list* l);
axiom length_nil{L}: length(\null) == 0;
axiom length_cons{L}:
\forall list* l, integer n; finite(l) && \valid(l) ==> length(l) == length(l->next) + 1;
} */
/*@
terminates finite(h);
assigns \result \from h;
ensures \separated(\result,h);
ensures finite(\result);
ensures samelist(\result,h);
*/
list *copyListRec(list *h)
{
if(h == NULL)
{
return NULL;
}
else
{
list *c = (list *) malloc (sizeof *c);
c->key = h->key;
c->next = copyListRec(h->next);
return c;
}
}
This the output with wp (Alt-Ergo):
[kernel] Parsing framac-copyList.c (with preprocessing)
[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:436: Warning:
Neither code nor explicit exits and terminates for function malloc,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
[wp] Warning: No definition for 'length' interpreted as reads nothing
[wp] framac-copyList.c:47: Warning:
Missing decreases clause on recursive function copyListRec, call must be unreachable
[wp] FRAMAC_SHARE/libc/stdlib.h:427: Warning:
Allocation, initialization and danglingness not yet implemented
(allocation: \fresh{Old, Here}(\at(\result,wp:post),\at(size,wp:pre)))
[wp] framac-copyList.c:45: Warning:
Cast with incompatible pointers types (source: sint8*) (target: _list*)
[wp] 18 goals scheduled
[wp] [Failure] typed_copyListRec_ensures (Qed 5ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_terminates_part3 (Qed 0.73ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_terminates_part2 (Qed 1ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_ensures_2 (Qed 6ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_ensures_3 (Qed 8ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_assigns_normal_part3 (Qed 3ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_assigns_normal_part6 (Qed 4ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_assigns_normal_part5 (Qed 5ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] Proved goals: 10 / 18
Qed: 10 (0.73ms-2ms-8ms)
Failed: 8
Handling linked lists with Frama-C and WP is like, super hard. Furthermore, currently WP does not handle dynamic allocation (this is a known limitation that is listed in the WP manual).
Here, the Failure is due to your inductive definition samelist: the first case does not use samelist, which leads to a typing error in Why3. WP should say this, so I'd suggest creating an issue on the public GitLab of Frama-C.
Furthermore, your definition of length does not give the memory footprint on which it depends, it should be done using the reads clause.
If you are interested in seeing exiting verification of linked lists with Frama-C, you may have a look to this paper: https://link.springer.com/chapter/10.1007/978-3-319-77935-5_3 and cited articles in this paper.