Celia

Library of linked lists

Input file intlist-sort-quick.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "stdlib.h" #include "stdio.h" typedef struct intlist_ intlist; struct intlist_ { int data; intlist next; }; / =================================================================== / / Predicates and functions used to specify intlist / / =================================================================== / // - reachability predicate /@ predicate reach(intlist from, intlist to) = @ (from == to) \|\| (\valid(from) && reach(from->next,to)) ; / // - acyclic predicate /@ predicate acyclic(intlist l) = @ reach(l,\null) ; / // - disjoint predicate /@ predicate disjoint(intlist l1, intlist l2) = @ ! (\exists intlist l ; reach(l1,l) && reach(l2,l)) ; @ @ predicate disjoint3(intlist l1, intlist l2, intlist l3) = @ disjoint(l1,l2) && disjoint(l2,l3) && disjoint(l1,l3) ; @ / //- length function /@ logic integer len(intlist ptr) = @ (ptr == \null) ? 0 : 1 + len(ptr->next) @ ; / // Quick sort: version creating new list /@ requires acyclic (a) ; / intlist quicksort(intlist a) { intlist left, right; intlist pivot, res, start, tmp; int d, l; intlist xis, ys, tmps; if (a == NULL) res = NULL; else { start = a->next; if (start == NULL){ //res = fold_clone(a);a res = NULL; res = (intlist) malloc(sizeof (struct intlist_)); res->data = a->data; res->next = NULL; } else { d = a->data; l = 1; pivot = NULL; pivot = (intlist) malloc(sizeof (struct intlist_)); pivot->next = NULL; pivot->data = d; xis = ys = tmps = NULL; xis = start; left = NULL; right = NULL; while (xis != NULL) { ys = (intlist) malloc(sizeof (struct intlist_)); ys->data = xis->data; ys->next = NULL; tmps = xis->next; xis = NULL; xis = tmps; tmps = NULL; if (ys->data <= d) { ys->next = left; left = NULL; left = ys; } else { ys->next = right; right = NULL; right = ys; } ys = NULL; } start = NULL; / no more used / l = 1 ; tmp = quicksort(left); left = NULL; left = tmp; tmp = NULL; tmp = quicksort(right); right = NULL; right = tmp; tmp = NULL; res = fold_concat3(left, pivot, right); left = right = pivot = NULL; } } return res; } /@ requires acyclic(x) && acyclic(y) && acyclic(h) && disjoint(x,y) && disjoint(y,h) && disjoint(x,h); / intlist fold_concat3(intlist x, intlist y, intlist h) { intlist r, z, zi, tmp, li; r = z = zi = tmp = li = NULL; // Copy X li = x; while (li != NULL) { zi = (intlist) malloc(sizeof (struct intlist_)); zi->data = li->data; zi->next = NULL; if (r == NULL) { r = zi; z = zi; } else { z->next = zi; z = NULL; z = zi; } zi = NULL; zi = li->next; li = NULL; li = zi; zi = NULL; } // Copy y after z li = y; while (li != NULL) { zi = (intlist) malloc(sizeof (struct intlist_)); zi->data = li->data; zi->next = NULL; if (r == NULL) { r = zi; z = zi; } else { z->next = zi; z = NULL; z = zi; } zi = NULL; zi = li->next; li = NULL; li = zi; zi = NULL; } // Copy h after z li = h; while (li != NULL) { zi = (intlist) malloc(sizeof (struct intlist_)); zi->data = li->data; zi->next = NULL; if (r == NULL) { r = zi; z = zi; } else { z->next = zi; z = NULL; z = zi; } zi = NULL; zi = li->next; li = NULL; li = zi; zi = NULL; } z = NULL; return r; } /@ requires len ==1 ; */ void amain(int len) { intlist curr, head; int i; head = NULL; curr = NULL; for (i = 1; i <= len; i++) { curr = NULL; curr = (intlist) malloc(sizeof (struct intlist_)); curr->data = len - i; curr->next = NULL; curr->next = head; head = NULL; head = curr; } curr = NULL; curr = quicksort(head); head = NULL; }	/* Generated by Frama-C / struct struct_intlist__xP { struct intlist_ struct_intlist__xM ; }; struct char_P { char char_M ; }; struct void_P { }; /@ behavior default: assigns \nothing; / void free(struct char_P ptr ) ; typedef unsigned int size_t; struct intlist_; typedef struct intlist_ intlist; struct intlist_ { int data ; intlist next ; }; /@ behavior default: assigns \at(\result,Post) \from __size; / extern __attribute__((__nothrow__)) struct char_P malloc(size_t __size ) __attribute__(( __malloc__)) ; /@ 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 fold_concat3(intlist x , intlist y , intlist h ) ; /File:intlist-sort-quick.c//@ requires //id:1 acyclic{ Here}(a); behavior default: / intlist quicksort( intlist a ) { struct struct_intlist__xP left ; struct struct_intlist__xP right ; intlist pivot ; intlist res ; intlist start ; intlist tmp ; int d ; int l ; intlist xis ; intlist ys ; intlist tmps ; intlist tmp_3 ; /File:intlist-sort-quick.c//sid:2/ if (a == (struct char_P )0) { /File:intlist-sort-quick.c//sid:3/ res = (struct intlist_ )((struct char_P )0); } else { /File:intlist-sort-quick.c//sid:4/ start = a->next; /File:intlist-sort-quick.c//sid:6/ if (start == (struct char_P )0) { /File:intlist-sort-quick.c//sid:7/ res = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:8/ res = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:9/ res->data = a->data; /File:intlist-sort-quick.c//sid:10/ res->next = (struct intlist_ )((struct char_P )0); } else { /File:intlist-sort-quick.c//sid:11/ d = a->data; /File:intlist-sort-quick.c//sid:12/ l = 1; /File:intlist-sort-quick.c//sid:13/ pivot = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:14/ pivot = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:15/ pivot->next = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:16/ pivot->data = d; /File:intlist-sort-quick.c//sid:17/ { /undefined sequence/ /File:intlist-sort-quick.c//sid:18/ tmps = (struct intlist_ )((struct char_P )0); /effects: tmps <- / /File:intlist-sort-quick.c//sid:19/ ys = tmps; /effects: ys <- / /File:intlist-sort-quick.c//sid:20/ xis = ys; /effects: xis <- / } /File:intlist-sort-quick.c//sid:21/ xis = start; /File:intlist-sort-quick.c//sid:22/ left->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:23/ right->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:24/ while (xis != (struct char_P )0) { /File:intlist-sort-quick.c//sid:28/ ys = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:29/ ys->data = xis->data; /File:intlist-sort-quick.c//sid:30/ ys->next = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:31/ tmps = xis->next; /File:intlist-sort-quick.c//sid:32/ xis = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:33/ xis = tmps; /File:intlist-sort-quick.c//sid:34/ tmps = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:36/ if (ys->data <= d) { /File:intlist-sort-quick.c//sid:37/ ys->next = left->struct_intlist__xM; /File:intlist-sort-quick.c//sid:38/ left->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:39/ left->struct_intlist__xM = ys; } else { /File:intlist-sort-quick.c//sid:40/ ys->next = right->struct_intlist__xM; /File:intlist-sort-quick.c//sid:41/ right->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:42/ right->struct_intlist__xM = ys; } /File:intlist-sort-quick.c//sid:43/ ys = (struct intlist_ )((struct char_P )0); } /File:intlist-sort-quick.c//sid:44/ start = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:45/ l = 1; /File:intlist-sort-quick.c//sid:46/ tmp = quicksort(left->struct_intlist__xM); /File:intlist-sort-quick.c//sid:47/ left->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:48/ left->struct_intlist__xM = tmp; /File:intlist-sort-quick.c//sid:49/ tmp = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:50/ tmp = quicksort(right->struct_intlist__xM); /File:intlist-sort-quick.c//sid:51/ right->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:52/ right->struct_intlist__xM = tmp; /File:intlist-sort-quick.c//sid:53/ tmp = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:54/ res = fold_concat3(left->struct_intlist__xM,pivot, right->struct_intlist__xM); /File:intlist-sort-quick.c//sid:55/ { /undefined sequence/ /File:intlist-sort-quick.c//sid:56/ pivot = (struct intlist_ )((struct char_P )0); /effects: pivot <- / /File:intlist-sort-quick.c//sid:57/ tmp_3 = pivot; /effects: <- / /File:intlist-sort-quick.c//sid:58/ right->struct_intlist__xM = tmp_3; /effects: right->struct_intlist__xM <- tmp_3, right/ /File:intlist-sort-quick.c//sid:59/ left->struct_intlist__xM = tmp_3; /effects: left->struct_intlist__xM <- left/ } } } /File:intlist-sort-quick.c//sid:60/ return (res); } /File:intlist-sort-quick.c//@ requires //id:2 ((((( acyclic{ Here} (x) ∧ acyclic{ Here} (y)) ∧ acyclic{ Here} (h)) ∧ disjoint{ Here} (x, y)) ∧ disjoint{ Here} (y, h)) ∧ disjoint{ Here} (x, h)); behavior default: / intlist fold_concat3( intlist x , intlist y , intlist h ) { intlist r ; intlist z ; intlist zi ; intlist tmp_0 ; intlist li ; /File:intlist-sort-quick.c//sid:61/ { /undefined sequence/ /File:intlist-sort-quick.c//sid:62/ li = (struct intlist_ )((struct char_P )0); /effects: li <- / /File:intlist-sort-quick.c//sid:63/ tmp_0 = li; /effects: tmp_0 <- / /File:intlist-sort-quick.c//sid:64/ zi = tmp_0; /effects: zi <- / /File:intlist-sort-quick.c//sid:65/ z = zi; /effects: z <- / /File:intlist-sort-quick.c//sid:66/ r = z; /effects: r <- / } /File:intlist-sort-quick.c//sid:67/ li = x; /File:intlist-sort-quick.c//sid:68/ while (li != (struct char_P )0) { /File:intlist-sort-quick.c//sid:72/ zi = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:73/ zi->data = li->data; /File:intlist-sort-quick.c//sid:74/ zi->next = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:76/ if (r == (struct char_P )0) { /File:intlist-sort-quick.c//sid:77/ r = zi; /File:intlist-sort-quick.c//sid:78/ z = zi; } else { /File:intlist-sort-quick.c//sid:79/ z->next = zi; /File:intlist-sort-quick.c//sid:80/ z = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:81/ z = zi; } /File:intlist-sort-quick.c//sid:82/ zi = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:83/ zi = li->next; /File:intlist-sort-quick.c//sid:84/ li = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:85/ li = zi; /File:intlist-sort-quick.c//sid:86/ zi = (struct intlist_ )((struct char_P )0); } /File:intlist-sort-quick.c//sid:87/ li = y; /File:intlist-sort-quick.c//sid:88/ while (li != (struct char_P )0) { /File:intlist-sort-quick.c//sid:92/ zi = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:93/ zi->data = li->data; /File:intlist-sort-quick.c//sid:94/ zi->next = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:96/ if (r == (struct char_P )0) { /File:intlist-sort-quick.c//sid:97/ r = zi; /File:intlist-sort-quick.c//sid:98/ z = zi; } else { /File:intlist-sort-quick.c//sid:99/ z->next = zi; /File:intlist-sort-quick.c//sid:100/ z = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:101/ z = zi; } /File:intlist-sort-quick.c//sid:102/ zi = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:103/ zi = li->next; /File:intlist-sort-quick.c//sid:104/ li = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:105/ li = zi; /File:intlist-sort-quick.c//sid:106/ zi = (struct intlist_ )((struct char_P )0); } /File:intlist-sort-quick.c//sid:107/ li = h; /File:intlist-sort-quick.c//sid:108/ while (li != (struct char_P )0) { /File:intlist-sort-quick.c//sid:112/ zi = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:113/ zi->data = li->data; /File:intlist-sort-quick.c//sid:114/ zi->next = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:116/ if (r == (struct char_P )0) { /File:intlist-sort-quick.c//sid:117/ r = zi; /File:intlist-sort-quick.c//sid:118/ z = zi; } else { /File:intlist-sort-quick.c//sid:119/ z->next = zi; /File:intlist-sort-quick.c//sid:120/ z = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:121/ z = zi; } /File:intlist-sort-quick.c//sid:122/ zi = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:123/ zi = li->next; /File:intlist-sort-quick.c//sid:124/ li = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:125/ li = zi; /File:intlist-sort-quick.c//sid:126/ zi = (struct intlist_ )((struct char_P )0); } /File:intlist-sort-quick.c//sid:127/ z = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:128/ return (r); } /File:intlist-sort-quick.c//@ requires //id:3 (len ≡ 1); behavior default: / void amain( int len ) { intlist curr ; intlist head ; int i ; /File:intlist-sort-quick.c//sid:129/ head = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:130/ curr = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:131/ i = 1; /File:intlist-sort-quick.c//sid:132/ while (i <= len) { /File:intlist-sort-quick.c//sid:136/ curr = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:137/ curr = (intlist )malloc(sizeof(struct intlist_ )); /File:intlist-sort-quick.c//sid:138/ curr->data = len - i; /File:intlist-sort-quick.c//sid:139/ curr->next = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:140/ curr->next = head; /File:intlist-sort-quick.c//sid:141/ head = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:142/ head = curr; /File:intlist-sort-quick.c//sid:143/ i ++; } /File:intlist-sort-quick.c//sid:144/ curr = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:145/ curr = quicksort(head); /File:intlist-sort-quick.c//sid:146/ head = (struct intlist_ )((struct char_P )0); /File:intlist-sort-quick.c//sid:148*/ return; }	Summary: intlist-sort-quick.c:(sid:60): mset, lsum, ucons, Summary: intlist-sort-quick.c:(sid:128): mset, lsum, ucons, intlist-sort-quick.c:(sid:121): mset, lsum, ucons, intlist-sort-quick.c:(sid:58_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:12): mset, lsum, ucons, intlist-sort-quick.c:(sid:58_1): mset, lsum, ucons, intlist-sort-quick.c:(sid:145): bottom intlist-sort-quick.c:(sid:2): mset, lsum, ucons, intlist-sort-quick.c:(sid:106): mset, lsum, ucons, intlist-sort-quick.c:(sid:101): mset, lsum, ucons, intlist-sort-quick.c:(sid:62): mset, lsum, ucons, intlist-sort-quick.c:(sid:38): mset, lsum, ucons, intlist-sort-quick.c:(sid:117): bottom intlist-sort-quick.c:(sid:63): mset, lsum, ucons, intlist-sort-quick.c:(sid:9): mset, lsum, ucons, intlist-sort-quick.c:(sid:150_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:64): mset, lsum, ucons, intlist-sort-quick.c:(sid:150_1): mset, lsum, ucons, intlist-sort-quick.c:(sid:86): mset, lsum, ucons, intlist-sort-quick.c:(sid:125_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:65): mset, lsum, ucons, intlist-sort-quick.c:(sid:66): mset, lsum, ucons, intlist-sort-quick.c:(sid:81): mset, lsum, ucons, intlist-sort-quick.c:(sid:33): mset, lsum, ucons, intlist-sort-quick.c:(sid:49): mset, lsum, ucons, intlist-sort-quick.c:(sid:23): mset, lsum, ucons, intlist-sort-quick.c:(sid:97): mset, lsum, ucons, intlist-sort-quick.c:(sid:140): bottom intlist-sort-quick.c:(sid:29): mset, lsum, ucons, intlist-sort-quick.c:(sid:81_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:13): mset, lsum, ucons, intlist-sort-quick.c:(sid:137): bottom intlist-sort-quick.c:(sid:53): mset, lsum, ucons, intlist-sort-quick.c:(sid:127): mset, lsum, ucons, intlist-sort-quick.c:(sid:16): mset, lsum, ucons, intlist-sort-quick.c:(sid:129): bottom intlist-sort-quick.c:(sid:122): mset, lsum, ucons, intlist-sort-quick.c:(sid:77): mset, lsum, ucons, intlist-sort-quick.c:(sid:42): mset, lsum, ucons, intlist-sort-quick.c:(sid:146): bottom intlist-sort-quick.c:(sid:89_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:118): bottom intlist-sort-quick.c:(sid:89_1): mset, lsum, ucons, intlist-sort-quick.c:(sid:45): mset, lsum, ucons, intlist-sort-quick.c:(sid:3): mset, lsum, ucons, intlist-sort-quick.c:(sid:102): mset, lsum, ucons, intlist-sort-quick.c:(sid:113): mset, lsum, ucons, intlist-sort-quick.c:(sid:34): mset, lsum, ucons, intlist-sort-quick.c:(sid:129_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:98): mset, lsum, ucons, intlist-sort-quick.c:(sid:129_1): mset, lsum, ucons, intlist-sort-quick.c:(sid:82): mset, lsum, ucons, intlist-sort-quick.c:(sid:39): mset, lsum, ucons, intlist-sort-quick.c:(sid:10): mset, lsum, ucons, intlist-sort-quick.c:(sid:93): mset, lsum, ucons, intlist-sort-quick.c:(sid:24): mset, lsum, ucons, intlist-sort-quick.c:(sid:46): mset, lsum, ucons, intlist-sort-quick.c:(sid:14): mset, lsum, ucons, intlist-sort-quick.c:(sid:141): bottom intlist-sort-quick.c:(sid:78): mset, lsum, ucons, intlist-sort-quick.c:(sid:26): mset, lsum, ucons, intlist-sort-quick.c:(sid:50): mset, lsum, ucons, intlist-sort-quick.c:(sid:27): bottom intlist-sort-quick.c:(sid:7): mset, lsum, ucons, intlist-sort-quick.c:(sid:130): bottom intlist-sort-quick.c:(sid:107): mset, lsum, ucons, intlist-sort-quick.c:(sid:30): mset, lsum, ucons, intlist-sort-quick.c:(sid:123): mset, lsum, ucons, intlist-sort-quick.c:(sid:73): mset, lsum, ucons, intlist-sort-quick.c:(sid:18): mset, lsum, ucons, intlist-sort-quick.c:(sid:148): bottom intlist-sort-quick.c:(sid:54): mset, lsum, ucons, intlist-sort-quick.c:(sid:19): mset, lsum, ucons, intlist-sort-quick.c:(sid:20): mset, lsum, ucons, intlist-sort-quick.c:(sid:87): mset, lsum, ucons, intlist-sort-quick.c:(sid:103): mset, lsum, ucons, intlist-sort-quick.c:(sid:43): mset, lsum, ucons, intlist-sort-quick.c:(sid:108): mset, lsum, ucons, intlist-sort-quick.c:(sid:114): mset, lsum, ucons, intlist-sort-quick.c:(sid:110): mset, lsum, ucons, intlist-sort-quick.c:(sid:111): bottom intlist-sort-quick.c:(sid:119): mset, lsum, ucons, intlist-sort-quick.c:(sid:67): mset, lsum, ucons, intlist-sort-quick.c:(sid:36): mset, lsum, ucons, intlist-sort-quick.c:(sid:83): mset, lsum, ucons, intlist-sort-quick.c:(sid:202_2): bottom intlist-sort-quick.c:(sid:4): mset, lsum, ucons, intlist-sort-quick.c:(sid:88): mset, lsum, ucons, intlist-sort-quick.c:(sid:8): mset, lsum, ucons, intlist-sort-quick.c:(sid:94): mset, lsum, ucons, intlist-sort-quick.c:(sid:90): mset, lsum, ucons, intlist-sort-quick.c:(sid:142): bottom intlist-sort-quick.c:(sid:131): bottom intlist-sort-quick.c:(sid:124): mset, lsum, ucons, intlist-sort-quick.c:(sid:91): bottom intlist-sort-quick.c:(sid:132): bottom intlist-sort-quick.c:(sid:99): mset, lsum, ucons, intlist-sort-quick.c:(sid:134): bottom intlist-sort-quick.c:(sid:138): bottom intlist-sort-quick.c:(sid:135): bottom intlist-sort-quick.c:(sid:68): mset, lsum, ucons, intlist-sort-quick.c:(sid:167_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:74): mset, lsum, ucons, intlist-sort-quick.c:(sid:70): mset, lsum, ucons, intlist-sort-quick.c:(sid:47): mset, lsum, ucons, intlist-sort-quick.c:(sid:71): bottom intlist-sort-quick.c:(sid:31): mset, lsum, ucons, intlist-sort-quick.c:(sid:104): mset, lsum, ucons, intlist-sort-quick.c:(sid:79): mset, lsum, ucons, intlist-sort-quick.c:(sid:51): mset, lsum, ucons, intlist-sort-quick.c:(sid:40): mset, lsum, ucons, intlist-sort-quick.c:(sid:28): mset, lsum, ucons, intlist-sort-quick.c:(sid:143): bottom intlist-sort-quick.c:(sid:62_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:0): bottom intlist-sort-quick.c:(sid:62_1): mset, lsum, ucons, intlist-sort-quick.c:(sid:84): mset, lsum, ucons, intlist-sort-quick.c:(sid:120): mset, lsum, ucons, intlist-sort-quick.c:(sid:21): mset, lsum, ucons, intlist-sort-quick.c:(sid:6): mset, lsum, ucons, intlist-sort-quick.c:(sid:116): mset, lsum, ucons, intlist-sort-quick.c:(sid:11): mset, lsum, ucons, intlist-sort-quick.c:(sid:144): bottom intlist-sort-quick.c:(sid:125): mset, lsum, ucons, intlist-sort-quick.c:(sid:37): mset, lsum, ucons, intlist-sort-quick.c:(sid:112): mset, lsum, ucons, intlist-sort-quick.c:(sid:100): mset, lsum, ucons, intlist-sort-quick.c:(sid:44): mset, lsum, ucons, intlist-sort-quick.c:(sid:171_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:96): mset, lsum, ucons, intlist-sort-quick.c:(sid:171_1): bottom intlist-sort-quick.c:(sid:56): mset, lsum, ucons, intlist-sort-quick.c:(sid:146_2): mset, lsum, ucons, intlist-sort-quick.c:(sid:57): mset, lsum, ucons, intlist-sort-quick.c:(sid:139): bottom intlist-sort-quick.c:(sid:58): mset, lsum, ucons, intlist-sort-quick.c:(sid:15): mset, lsum, ucons, intlist-sort-quick.c:(sid:105): mset, lsum, ucons, intlist-sort-quick.c:(sid:80): mset, lsum, ucons, intlist-sort-quick.c:(sid:59): mset, lsum, ucons, intlist-sort-quick.c:(sid:92): mset, lsum, ucons, intlist-sort-quick.c:(sid:32): mset, lsum, ucons, intlist-sort-quick.c:(sid:76): mset, lsum, ucons, intlist-sort-quick.c:(sid:0): mset, lsum, ucons, intlist-sort-quick.c:(sid:48): mset, lsum, ucons, intlist-sort-quick.c:(sid:22): mset, lsum, ucons, intlist-sort-quick.c:(sid:136): bottom intlist-sort-quick.c:(sid:85): mset, lsum, ucons, intlist-sort-quick.c:(sid:41): mset, lsum, ucons, intlist-sort-quick.c:(sid:0): mset, lsum, ucons, intlist-sort-quick.c:(sid:126): mset, lsum, ucons, intlist-sort-quick.c:(sid:72): mset, lsum, ucons, intlist-sort-quick.c:(sid:52): mset, lsum, ucons,

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists