Celia

Library of linked lists

Input file intlist-fold2-equal.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "intlist.h" // Returns 1 if two lists are equal // Iterative version. /@ requires acyclic(x) && acyclic(y) && disjoint(x,y); / int fold2_equal(intlist x, intlist y) { intlist xi, yi, tmp; xi = yi = tmp = NULL; xi = x; yi = y; while (xi != NULL) { if (yi != NULL) { if (xi->data != yi->data) return 0; tmp = xi->next; xi = NULL; xi = tmp; tmp = NULL; tmp = yi->next; yi = NULL; yi = tmp; tmp = NULL; } else break; } if (xi == NULL) if (yi == NULL) return 1; return 0; }	/* Generated by Frama-C / struct char_P { char char_M ; }; struct void_P { }; /@ behavior default: assigns \nothing; / void free(struct char_P ptr ) ; /@ behavior default: assigns \nothing; / struct char_P malloc(unsigned int size ) ; struct intlist_; typedef struct intlist_ intlist; struct intlist_ { int data ; intlist next ; }; /@ predicate reach{L}(intlist from, intlist to) = ((from ≡ to) ∨ (\valid(from) ∧ reach(from->next, to))); / /@ predicate acyclic{L}(intlist l) = reach{L}(l, \null); / /@ predicate disjoint{L}(intlist l1, intlist l2) = ¬((∃ struct intlist_ l_0; (reach{L}(l1, l_0) ∧ reach{L}(l2, l_0)))); / /@ predicate disjoint3{L}(intlist l1_0, intlist l2_0, intlist l3) = ((disjoint{L}(l1_0, l2_0) ∧ disjoint{L}(l2_0, l3)) ∧ disjoint{L}(l1_0, l3)); / /@ logic ℤ len(intlist ptr) = ptr≡\null? 0: 1+len(ptr->next); / int fold2_equal(intlist x , intlist y ) ; /File: intlist-fold2-equal.c(9,9)//@ requires //id:67 ((acyclic{Here}(x) ∧ acyclic{Here}(y)) ∧ disjoint{Here} (x, y)); behavior default: / int fold2_equal(intlist x , intlist y ) { intlist xi ; intlist yi ; intlist tmp ; int __retres ; /File: intlist-fold2-equal.c//sid:1/ { /undefined sequence/ /File: intlist-fold2-equal.c//sid:2/ tmp = (struct intlist_ )((struct char_P )0); /effects: tmp <- / /File: intlist-fold2-equal.c//sid:3/ yi = tmp; /effects: yi <- / /File: intlist-fold2-equal.c//sid:4/ xi = yi; /effects: xi <- / } /File: intlist-fold2-equal.c//sid:5/ xi = x; /File: intlist-fold2-equal.c//sid:6/ yi = y; /File: intlist-fold2-equal.c//sid:7/ while (xi != (struct char_P )0) { /File: intlist-fold2-equal.c//sid:12/ if (yi != (struct char_P )0) { /File: intlist-fold2-equal.c//sid:14/ if (xi->data != yi->data) { /File: intlist-fold2-equal.c//sid:15/ __retres = 0; /File: intlist-fold2-equal.c//sid:34/ goto return_label; } /File: intlist-fold2-equal.c//sid:17/ tmp = xi->next; /File: intlist-fold2-equal.c//sid:18/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-equal.c//sid:19/ xi = tmp; /File: intlist-fold2-equal.c//sid:20/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-equal.c//sid:21/ tmp = yi->next; /File: intlist-fold2-equal.c//sid:22/ yi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-equal.c//sid:23/ yi = tmp; /File: intlist-fold2-equal.c//sid:24/ tmp = (struct intlist_ )((struct char_P )0); } else { /File: intlist-fold2-equal.c//sid:25/ break; } } /File: intlist-fold2-equal.c//sid:27/ if (xi == (struct char_P )0) { /File: intlist-fold2-equal.c//sid:29/ if (yi == (struct char_P )0) { /File: intlist-fold2-equal.c//sid:30/ __retres = 1; /File: intlist-fold2-equal.c//sid:35/ goto return_label; } } /File: intlist-fold2-equal.c//sid:33/ __retres = 0; /File: intlist-fold2-equal.c/return_label: / internal / /sid:36*/ return (__retres); }	Summary: intlist-fold2-equal.c:(sid:36): mset, lsum, ucons, intlist-fold2-equal.c:(sid:19): mset, lsum, ucons, intlist-fold2-equal.c:(sid:18): mset, lsum, ucons, intlist-fold2-equal.c:(sid:14_2): mset, lsum, ucons, intlist-fold2-equal.c:(sid:17): mset, lsum, ucons, intlist-fold2-equal.c:(sid:0): mset, lsum, ucons, intlist-fold2-equal.c:(sid:27): mset, lsum, ucons, intlist-fold2-equal.c:(sid:15_2): mset, lsum, ucons, intlist-fold2-equal.c:(sid:15_1): mset, lsum, ucons, intlist-fold2-equal.c:(sid:29): mset, lsum, ucons, intlist-fold2-equal.c:(sid:29_1): mset, lsum, ucons, intlist-fold2-equal.c:(sid:28_1): mset, lsum, ucons, intlist-fold2-equal.c:(sid:15): mset, lsum, ucons, intlist-fold2-equal.c:(sid:7): mset, lsum, ucons, intlist-fold2-equal.c:(sid:2): mset, lsum, ucons, intlist-fold2-equal.c:(sid:3): mset, lsum, ucons, intlist-fold2-equal.c:(sid:4): mset, lsum, ucons, intlist-fold2-equal.c:(sid:9): mset, lsum, ucons, intlist-fold2-equal.c:(sid:16_1): mset, lsum, ucons, intlist-fold2-equal.c:(sid:30): mset, lsum, ucons, intlist-fold2-equal.c:(sid:10): bottom intlist-fold2-equal.c:(sid:24): mset, lsum, ucons, intlist-fold2-equal.c:(sid:5): mset, lsum, ucons, intlist-fold2-equal.c:(sid:35): bottom intlist-fold2-equal.c:(sid:25): bottom intlist-fold2-equal.c:(sid:12): mset, lsum, ucons, intlist-fold2-equal.c:(sid:23): mset, lsum, ucons, intlist-fold2-equal.c:(sid:22): mset, lsum, ucons, intlist-fold2-equal.c:(sid:20): mset, lsum, ucons, intlist-fold2-equal.c:(sid:21): mset, lsum, ucons, intlist-fold2-equal.c:(sid:34): bottom intlist-fold2-equal.c:(sid:14): mset, lsum, ucons, intlist-fold2-equal.c:(sid:6): mset, lsum, ucons, intlist-fold2-equal.c:(sid:33): mset, lsum, ucons,

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists