Celia

Library of linked lists

Input file intlist-sort-insert.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "intlist.h" // Insertion sort. // Version moving data like in arrays. /@ requires acyclic(x); / intlist insertsort(intlist x) { intlist xi; intlist y; intlist yi; int m; int n; xi = NULL; y = NULL; yi = NULL; xi = x->next; while (xi != NULL) { y = x; while (y != xi) { if (y->data <= xi->data) { yi = y->next; y = NULL; y = yi; yi = NULL; } else break; } m = xi->data; while (y != xi) { n = y->data; y->data = m; m = n; yi = y->next; y = NULL; y = yi; yi = NULL; } y = NULL; xi->data = m; yi = xi->next; xi = NULL; xi = yi; yi = NULL; } }	/* 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); / /File: intlist-sort-insert.c//@ requires //id:67 acyclic{Here}(x); behavior default: / intlist insertsort(intlist x ) { intlist xi ; intlist y ; intlist yi ; int m ; int n ; intlist __retres ; /File: intlist-sort-insert.c//sid:1/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:2/ y = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:3/ yi = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:4/ xi = x->next; /File: intlist-sort-insert.c//sid:5/ while (xi != (struct char_P )0) { /File: intlist-sort-insert.c//sid:9/ y = x; /File: intlist-sort-insert.c//sid:10/ while (y != xi) { /File: intlist-sort-insert.c//sid:15/ if (y->data <= xi->data) { /File: intlist-sort-insert.c//sid:16/ yi = y->next; /File: intlist-sort-insert.c//sid:17/ y = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:18/ y = yi; /File: intlist-sort-insert.c//sid:19/ yi = (struct intlist_ )((struct char_P )0); } else { /File: intlist-sort-insert.c//sid:20/ break; } } /File: intlist-sort-insert.c//sid:21/ m = xi->data; /File: intlist-sort-insert.c//sid:22/ while (y != xi) { /File: intlist-sort-insert.c//sid:26/ n = y->data; /File: intlist-sort-insert.c//sid:27/ y->data = m; /File: intlist-sort-insert.c//sid:28/ m = n; /File: intlist-sort-insert.c//sid:29/ yi = y->next; /File: intlist-sort-insert.c//sid:30/ y = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:31/ y = yi; /File: intlist-sort-insert.c//sid:32/ yi = (struct intlist_ )((struct char_P )0); } /File: intlist-sort-insert.c//sid:33/ y = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:34/ xi->data = m; /File: intlist-sort-insert.c//sid:35/ yi = xi->next; /File: intlist-sort-insert.c//sid:36/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-sort-insert.c//sid:37/ xi = yi; /File: intlist-sort-insert.c//sid:38/ yi = (struct intlist_ )((struct char_P )0); } /File: intlist-sort-insert.c//sid:39/ __retres = (struct intlist_ )0; /File: intlist-sort-insert.c//sid:40*/ return (__retres); }	Summary: intlist-sort-insert.c:(sid:40): mset, lsum, ucons, intlist-sort-insert.c:(sid:9): mset, lsum, ucons, intlist-sort-insert.c:(sid:27): mset, lsum, ucons, intlist-sort-insert.c:(sid:17): mset, lsum, ucons, intlist-sort-insert.c:(sid:25_2): mset, lsum, ucons, intlist-sort-insert.c:(sid:4): mset, lsum, ucons, intlist-sort-insert.c:(sid:1): mset, lsum, ucons, intlist-sort-insert.c:(sid:19): mset, lsum, ucons, intlist-sort-insert.c:(sid:31): mset, lsum, ucons, intlist-sort-insert.c:(sid:34): mset, lsum, ucons, intlist-sort-insert.c:(sid:0): mset, lsum, ucons, intlist-sort-insert.c:(sid:20): bottom intlist-sort-insert.c:(sid:22_2): mset, lsum, ucons, intlist-sort-insert.c:(sid:3): mset, lsum, ucons, intlist-sort-insert.c:(sid:37): mset, lsum, ucons, intlist-sort-insert.c:(sid:15): mset, lsum, ucons, intlist-sort-insert.c:(sid:10): mset, lsum, ucons, intlist-sort-insert.c:(sid:33): mset, lsum, ucons, intlist-sort-insert.c:(sid:26): mset, lsum, ucons, intlist-sort-insert.c:(sid:16): mset, lsum, ucons, intlist-sort-insert.c:(sid:30): mset, lsum, ucons, intlist-sort-insert.c:(sid:12): mset, lsum, ucons, intlist-sort-insert.c:(sid:13): bottom intlist-sort-insert.c:(sid:32): mset, lsum, ucons, intlist-sort-insert.c:(sid:28): mset, lsum, ucons, intlist-sort-insert.c:(sid:36): mset, lsum, ucons, intlist-sort-insert.c:(sid:5): mset, lsum, ucons, intlist-sort-insert.c:(sid:22): mset, lsum, ucons, intlist-sort-insert.c:(sid:7): mset, lsum, ucons, intlist-sort-insert.c:(sid:24): mset, lsum, ucons, intlist-sort-insert.c:(sid:8): bottom intlist-sort-insert.c:(sid:25): bottom intlist-sort-insert.c:(sid:18): mset, lsum, ucons, intlist-sort-insert.c:(sid:39): mset, lsum, ucons, intlist-sort-insert.c:(sid:2): mset, lsum, ucons, intlist-sort-insert.c:(sid:36_2): mset, lsum, ucons, intlist-sort-insert.c:(sid:26_2): mset, lsum, ucons, intlist-sort-insert.c:(sid:35): mset, lsum, ucons, intlist-sort-insert.c:(sid:29): mset, lsum, ucons, intlist-sort-insert.c:(sid:26_1): mset, lsum, ucons, intlist-sort-insert.c:(sid:38): mset, lsum, ucons, intlist-sort-insert.c:(sid:21): mset, lsum, ucons,

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists