Celia

Library of linked lists

Input file intlist-lib-del_tail.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "intlist.h" // Deletes the last element of head. // Iterative version. /@ requires acyclic(head); @ / intlist del_tail(intlist head) { intlist h, hp, tmp; h = hp = tmp = NULL; if (head == NULL) return NULL; h = head; tmp = h->next; if (tmp == NULL) { free(head); return NULL; } while (tmp != NULL) { hp = NULL; hp = h; h = NULL; h = tmp; tmp = NULL; tmp = h->next; } free(h); hp->next = NULL; hp = NULL; /* no more used */ return head; }	/* Generated by Frama-C / struct char_P { char char_M ; }; struct void_P { }; /@ behavior default: assigns \nothing; / struct char_P malloc(unsigned int size ) ; struct intlist_; typedef struct intlist_ intlist; struct intlist_ { int data ; intlist next ; }; /@ behavior default: assigns \nothing; / extern __attribute__((__nothrow__)) void free(struct char_P __ptr ) ; /@ 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); / intlist del_tail(intlist head ) ; /File: intlist-lib-del_tail.c//@ requires //id:67 acyclic{Here} (head); behavior default: / intlist del_tail(intlist head ) { intlist h ; intlist hp ; intlist tmp ; intlist __retres ; /File: intlist-lib-del_tail.c//sid:1/ { /undefined sequence/ /File: intlist-lib-del_tail.c//sid:2/ tmp = (struct intlist_ )((struct char_P )0); /effects: tmp <- / /File: intlist-lib-del_tail.c//sid:3/ hp = tmp; /effects: hp <- / /File: intlist-lib-del_tail.c//sid:4/ h = hp; /effects: h <- / } /File: intlist-lib-del_tail.c//sid:6/ if (head == (struct char_P )0) { /File: intlist-lib-del_tail.c//sid:7/ __retres = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:30/ goto return_label; } /File: intlist-lib-del_tail.c//sid:9/ h = head; /File: intlist-lib-del_tail.c//sid:10/ tmp = h->next; /File: intlist-lib-del_tail.c//sid:12/ if (tmp == (struct char_P )0) { /File: intlist-lib-del_tail.c//sid:13/ free((struct char_P )head); /File: intlist-lib-del_tail.c//sid:14/ __retres = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:31/ goto return_label; } /File: intlist-lib-del_tail.c//sid:16/ while (tmp != (struct char_P )0) { /File: intlist-lib-del_tail.c//sid:20/ hp = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:21/ hp = h; /File: intlist-lib-del_tail.c//sid:22/ h = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:23/ h = tmp; /File: intlist-lib-del_tail.c//sid:24/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:25/ tmp = h->next; } /File: intlist-lib-del_tail.c//sid:26/ free((struct char_P )h); /File: intlist-lib-del_tail.c//sid:27/ hp->next = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:28/ hp = (struct intlist_ )((struct char_P )0); /File: intlist-lib-del_tail.c//sid:29/ __retres = head; /File: intlist-lib-del_tail.c/return_label: /* internal / /sid:32*/ return (__retres); }	Summary: intlist-lib-del_tail.c:(sid:32): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:31): bottom intlist-lib-del_tail.c:(sid:27): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:23): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:16_1): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:29): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:12_1): bottom intlist-lib-del_tail.c:(sid:22): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:2): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:30): bottom intlist-lib-del_tail.c:(sid:3): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:4): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:14): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:16): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:9): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:18): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:6): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:19): bottom intlist-lib-del_tail.c:(sid:26): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:0): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:12): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:7): bottom intlist-lib-del_tail.c:(sid:25): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:21): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:13): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:24): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:20): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:20_2): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:28): mset, lsum, ucons, intlist-lib-del_tail.c:(sid:10): mset, lsum, ucons,

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists