Celia

Library of linked lists

Input file intlist-lib-empty.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "intlist.h" // Returns non zero if the list is not empty. /@ requires acyclic(head); @ / int empty(intlist head) { if (head == NULL) return 0; return 1; }	/* 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 empty(intlist head ) ; /File: intlist-lib-empty.c//@ requires //id:67 acyclic{Here}(head); behavior default: / int empty(intlist head ) { int __retres ; /File: intlist-lib-empty.c//sid:2/ if (head == (struct char_P )0) { /File: intlist-lib-empty.c//sid:3/ __retres = 0; /File: intlist-lib-empty.c//sid:6/ goto return_label; } /File: intlist-lib-empty.c//sid:5/ __retres = 1; /File: intlist-lib-empty.c/return_label: /* internal / /sid:7*/ return (__retres); }	Summary: intlist-lib-empty.c:(sid:7): mset, lsum, ucons, intlist-lib-empty.c:(sid:3): bottom intlist-lib-empty.c:(sid:0): mset, lsum, ucons, intlist-lib-empty.c:(sid:2): mset, lsum, ucons, intlist-lib-empty.c:(sid:5): mset, lsum, ucons, intlist-lib-empty.c:(sid:6): bottom intlist-lib-empty.c:(sid:8_1): bottom

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists