Celia

Library of linked lists

Input file intlist-sort-merge.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "intlist.h" // Merge sort: version creating new list #define clone fold_clone #define merge fold2_merge #define split split /@ requires acyclic(x); / intlist mergesort(intlist x) { intlist r, tmp; r = tmp = NULL; if (x != NULL) { tmp = x->next; if (tmp == NULL) r = clone(x); else { intlist l1, l2; tmp = NULL; l1 = NULL; l2 = NULL; split (x, l1, l2); tmp = mergesort (l1); l1 = NULL; l1 = tmp; tmp = NULL; tmp = mergesort (l2); l2 = NULL; l2 = tmp; tmp = NULL; tmp = merge (l1, l2); l1 = NULL; l2 = NULL; r = tmp; tmp = NULL; } } return r; } // end merge_sort function	/* 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 ) ; struct intlist_; typedef struct intlist_ intlist; struct intlist_ { int data ; intlist next ; }; typedef unsigned int size_t; /@ 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_clone(intlist x_2 ) ; intlist fold2_merge(intlist x_0 , intlist y ) ; void split(intlist x_1 , struct struct_intlist__xP l1 , struct struct_intlist__xP l2 ) ; /File: intlist-sort-merge.c//@ requires //id:268 acyclic{Here}(x); behavior default: / intlist mergesort(intlist x ) { intlist r ; intlist tmp ; struct struct_intlist__xP l1_0 ; struct struct_intlist__xP l2_0 ; /File: intlist-sort-merge.c//sid:1/ { /undefined sequence/ /File: intlist-sort-merge.c//sid:2/ tmp = (struct intlist_ )((struct char_P )0); /effects: tmp <- / /File: intlist-sort-merge.c//sid:3/ r = tmp; /effects: r <- / } /File: intlist-sort-merge.c//sid:5/ if (x != (struct char_P )0) { /File: intlist-sort-merge.c//sid:6/ tmp = x->next; /File: intlist-sort-merge.c//sid:8/ if (tmp == (struct char_P )0) { /File: intlist-sort-merge.c//sid:9/ r = fold_clone(x); } else { /File: intlist-sort-merge.c//sid:10/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:11/ l1_0->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:12/ l2_0->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:13/ split(x,l1_0,l2_0); /File: intlist-sort-merge.c//sid:14/ tmp = mergesort(l1_0->struct_intlist__xM); /File: intlist-sort-merge.c//sid:15/ l1_0->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:16/ l1_0->struct_intlist__xM = tmp; /File: intlist-sort-merge.c//sid:17/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:18/ tmp = mergesort(l2_0->struct_intlist__xM); /File: intlist-sort-merge.c//sid:19/ l2_0->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:20/ l2_0->struct_intlist__xM = tmp; /File: intlist-sort-merge.c//sid:21/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:22/ tmp = fold2_merge(l1_0->struct_intlist__xM,l2_0->struct_intlist__xM); /File: intlist-sort-merge.c//sid:23/ l1_0->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:24/ l2_0->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-sort-merge.c//sid:25/ r = tmp; /File: intlist-sort-merge.c//sid:26/ tmp = (struct intlist_ )((struct char_P )0); } } /File: intlist-sort-merge.c//sid:28/ return (r); } /@ behavior default: assigns \at(\result,Post) \from __size; / extern __attribute__((__nothrow__)) struct char_P malloc(size_t __size ) __attribute__(( __malloc__)) ; /File: intlist-fold2-merge.c//@ requires //id:201 ((acyclic{ Here}(x_0) ∧ acyclic{Here}(y)) ∧ disjoint{ Here}(x_0, y)); behavior default: / intlist fold2_merge(intlist x_0 , intlist y ) { intlist r_0 ; intlist ri ; intlist xi ; intlist yi ; intlist tmp_0 ; int v ; /File: intlist-fold2-merge.c//sid:29/ { /undefined sequence/ /File: intlist-fold2-merge.c//sid:30/ tmp_0 = (struct intlist_ )((struct char_P )0); /effects: tmp_0 <- / /File: intlist-fold2-merge.c//sid:31/ yi = tmp_0; /effects: yi <- / /File: intlist-fold2-merge.c//sid:32/ xi = yi; /effects: xi <- / /File: intlist-fold2-merge.c//sid:33/ ri = xi; /effects: ri <- / /File: intlist-fold2-merge.c//sid:34/ r_0 = ri; /effects: r_0 <- / } /File: intlist-fold2-merge.c//sid:35/ xi = x_0; /File: intlist-fold2-merge.c//sid:36/ yi = y; /File: intlist-fold2-merge.c//sid:37/ while (1) { /File: intlist-fold2-merge.c//sid:39/ if (xi != (struct char_P )0) { /File: intlist-fold2-merge.c//sid:41/ if (! (yi != (struct char_P )0)) { /File: intlist-fold2-merge.c//sid:42/ break; } } else { /File: intlist-fold2-merge.c//sid:43/ break; } /File: intlist-fold2-merge.c//sid:45/ if (xi->data < yi->data) { /File: intlist-fold2-merge.c//sid:46/ v = xi->data; /File: intlist-fold2-merge.c//sid:47/ tmp_0 = xi->next; /File: intlist-fold2-merge.c//sid:48/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:49/ xi = tmp_0; /File: intlist-fold2-merge.c//sid:50/ tmp_0 = (struct intlist_ )((struct char_P )0); } else { /File: intlist-fold2-merge.c//sid:51/ v = yi->data; /File: intlist-fold2-merge.c//sid:52/ tmp_0 = yi->next; /File: intlist-fold2-merge.c//sid:53/ yi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:54/ yi = tmp_0; /File: intlist-fold2-merge.c//sid:55/ tmp_0 = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:56/ tmp_0 = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold2-merge.c//sid:57/ tmp_0->data = v; /File: intlist-fold2-merge.c//sid:58/ tmp_0->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:60/ if (r_0 == (struct char_P )0) { /File: intlist-fold2-merge.c//sid:61/ r_0 = tmp_0; /File: intlist-fold2-merge.c//sid:62/ ri = tmp_0; } else { /File: intlist-fold2-merge.c//sid:63/ ri->next = tmp_0; /File: intlist-fold2-merge.c//sid:64/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:65/ ri = tmp_0; } /File: intlist-fold2-merge.c//sid:66/ tmp_0 = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:67/ while (xi != (struct char_P )0) { /File: intlist-fold2-merge.c//sid:71/ tmp_0 = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold2-merge.c//sid:72/ tmp_0->data = xi->data; /File: intlist-fold2-merge.c//sid:73/ tmp_0->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:75/ if (r_0 == (struct char_P )0) { /File: intlist-fold2-merge.c//sid:76/ r_0 = tmp_0; /File: intlist-fold2-merge.c//sid:77/ ri = tmp_0; } else { /File: intlist-fold2-merge.c//sid:78/ ri->next = tmp_0; /File: intlist-fold2-merge.c//sid:79/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:80/ ri = tmp_0; } /File: intlist-fold2-merge.c//sid:81/ tmp_0 = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:82/ tmp_0 = xi->next; /File: intlist-fold2-merge.c//sid:83/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:84/ xi = tmp_0; /File: intlist-fold2-merge.c//sid:85/ tmp_0 = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:86/ while (yi != (struct char_P )0) { /File: intlist-fold2-merge.c//sid:90/ tmp_0 = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold2-merge.c//sid:91/ tmp_0->data = yi->data; /File: intlist-fold2-merge.c//sid:92/ tmp_0->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:94/ if (r_0 == (struct char_P )0) { /File: intlist-fold2-merge.c//sid:95/ r_0 = tmp_0; /File: intlist-fold2-merge.c//sid:96/ ri = tmp_0; } else { /File: intlist-fold2-merge.c//sid:97/ ri->next = tmp_0; /File: intlist-fold2-merge.c//sid:98/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:99/ ri = tmp_0; } /File: intlist-fold2-merge.c//sid:100/ tmp_0 = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:101/ tmp_0 = yi->next; /File: intlist-fold2-merge.c//sid:102/ yi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:103/ yi = tmp_0; /File: intlist-fold2-merge.c//sid:104/ tmp_0 = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:105/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:106/ return (r_0); } /File: intlist-fold-split_rec.c//@ requires //id:134 acyclic{ Here}(x_1); behavior default: / void split(intlist x_1 , struct struct_intlist__xP l1 , struct struct_intlist__xP l2 ) { intlist tmp_1 ; intlist nxt ; intlist ll1 ; intlist ll2 ; /File: intlist-fold-split_rec.c//sid:108/ if (x_1 == (struct char_P )0) { /File: intlist-fold-split_rec.c//sid:109/ l1->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:110/ l2->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:169/ goto return_label; } /File: intlist-fold-split_rec.c//sid:113/ nxt = x_1->next; /File: intlist-fold-split_rec.c//sid:114/ ll1 = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold-split_rec.c//sid:115/ ll1->data = x_1->data; /File: intlist-fold-split_rec.c//sid:116/ ll1->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:118/ if (nxt == (struct char_P )0) { /File: intlist-fold-split_rec.c//sid:119/ l1->struct_intlist__xM = ll1; /File: intlist-fold-split_rec.c//sid:120/ l2->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:121/ { /undefined sequence/ /File: intlist-fold-split_rec.c//sid:122/ ll1 = (struct intlist_ )((struct char_P )0); /effects: ll1 <- / /File: intlist-fold-split_rec.c//sid:123/ nxt = ll1; /effects: nxt <- / } /File: intlist-fold-split_rec.c//sid:170/ goto return_label; } /File: intlist-fold-split_rec.c//sid:126/ ll2 = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold-split_rec.c//sid:127/ ll2->data = nxt->data; /File: intlist-fold-split_rec.c//sid:128/ ll2->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:129/ tmp_1 = nxt->next; /File: intlist-fold-split_rec.c//sid:130/ split(tmp_1,l1,l2); /File: intlist-fold-split_rec.c//sid:131/ ll1->next = l1->struct_intlist__xM; /File: intlist-fold-split_rec.c//sid:132/ ll2->next = l2->struct_intlist__xM; /File: intlist-fold-split_rec.c//sid:133/ l1->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:134/ l1->struct_intlist__xM = ll1; /File: intlist-fold-split_rec.c//sid:135/ l2->struct_intlist__xM = (struct intlist_ )((struct char_P )0); /File: intlist-fold-split_rec.c//sid:136/ l2->struct_intlist__xM = ll2; /File: intlist-fold-split_rec.c//sid:137/ { /undefined sequence/ /File: intlist-fold-split_rec.c//sid:138/ nxt = (struct intlist_ )((struct char_P )0); /effects: nxt <- / /File: intlist-fold-split_rec.c//sid:139/ tmp_1 = nxt; /effects: tmp_1 <- / /File: intlist-fold-split_rec.c//sid:140/ ll2 = tmp_1; /effects: ll2 <- / /File: intlist-fold-split_rec.c//sid:141/ ll1 = ll2; /effects: ll1 <- / } /File: intlist-fold-split_rec.c/return_label: / internal / /sid:171/ return; } /File: intlist-fold-clone.c//@ requires //id:67 acyclic{Here}(x_2); behavior default: / intlist fold_clone(intlist x_2 ) { intlist xi_0 ; intlist y_0 ; intlist yi_0 ; intlist z ; /File: intlist-fold-clone.c//sid:143/ { /undefined sequence/ /File: intlist-fold-clone.c//sid:144/ z = (struct intlist_ )((struct char_P )0); /effects: z <- / /File: intlist-fold-clone.c//sid:145/ yi_0 = z; /effects: yi_0 <- / /File: intlist-fold-clone.c//sid:146/ y_0 = yi_0; /effects: y_0 <- / /File: intlist-fold-clone.c//sid:147/ xi_0 = y_0; /effects: xi_0 <- / } /File: intlist-fold-clone.c//sid:148/ xi_0 = x_2; /File: intlist-fold-clone.c//sid:149/ while (xi_0 != (struct char_P )0) { /File: intlist-fold-clone.c//sid:153/ z = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold-clone.c//sid:154/ z->data = xi_0->data; /File: intlist-fold-clone.c//sid:155/ z->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold-clone.c//sid:157/ if (y_0 == (struct char_P )0) { /File: intlist-fold-clone.c//sid:158/ y_0 = z; } else { /File: intlist-fold-clone.c//sid:159/ yi_0->next = z; } /File: intlist-fold-clone.c//sid:160/ yi_0 = (struct intlist_ )((struct char_P )0); /File: intlist-fold-clone.c//sid:161/ yi_0 = z; /File: intlist-fold-clone.c//sid:162/ z = (struct intlist_ )((struct char_P )0); /File: intlist-fold-clone.c//sid:163/ z = xi_0->next; /File: intlist-fold-clone.c//sid:164/ xi_0 = (struct intlist_ )((struct char_P )0); /File: intlist-fold-clone.c//sid:165/ xi_0 = z; /File: intlist-fold-clone.c//sid:166/ z = (struct intlist_ )((struct char_P )0); } /File: intlist-fold-clone.c//sid:167/ yi_0 = (struct intlist_ )((struct char_P )0); /File: intlist-fold-clone.c//sid:168*/ return (y_0); }	Summary: intlist-sort-merge.c:(sid:28): mset, lsum, ucons, Summary: intlist-fold2-merge.c:(sid:106): mset, lsum, ucons, Summary: intlist-fold-split_rec.c:(sid:171): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:115): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:132): mset, lsum, ucons, intlist-sort-merge.c:(sid:17): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:110): mset, lsum, ucons, intlist-fold2-merge.c:(sid:37): mset, lsum, ucons, intlist-fold-clone.c:(sid:157): mset, lsum, ucons, intlist-fold2-merge.c:(sid:62): mset, lsum, ucons, intlist-fold2-merge.c:(sid:39): mset, lsum, ucons, intlist-fold-clone.c:(sid:167): mset, lsum, ucons, intlist-fold2-merge.c:(sid:66): mset, lsum, ucons, intlist-fold2-merge.c:(sid:41): mset, lsum, ucons, intlist-sort-merge.c:(sid:12): mset, lsum, ucons, intlist-fold2-merge.c:(sid:47): mset, lsum, ucons, intlist-fold2-merge.c:(sid:42): bottom intlist-fold2-merge.c:(sid:43): bottom intlist-fold2-merge.c:(sid:94): mset, lsum, ucons, intlist-fold2-merge.c:(sid:84): mset, lsum, ucons, intlist-fold2-merge.c:(sid:98): mset, lsum, ucons, intlist-fold2-merge.c:(sid:34_2): mset, lsum, ucons, intlist-sort-merge.c:(sid:9): mset, lsum, ucons, intlist-fold-clone.c:(sid:162): mset, lsum, ucons, intlist-fold-clone.c:(sid:153): mset, lsum, ucons, intlist-fold2-merge.c:(sid:90): mset, lsum, ucons, intlist-fold2-merge.c:(sid:34_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:51): mset, lsum, ucons, intlist-fold2-merge.c:(sid:57): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:122): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:123): mset, lsum, ucons, intlist-fold2-merge.c:(sid:17_2): mset, lsum, ucons, intlist-sort-merge.c:(sid:2): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:133): mset, lsum, ucons, intlist-fold2-merge.c:(sid:17_1): mset, lsum, ucons, intlist-sort-merge.c:(sid:3): mset, lsum, ucons, intlist-fold2-merge.c:(sid:103): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:116): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:128): mset, lsum, ucons, intlist-sort-merge.c:(sid:18): mset, lsum, ucons, intlist-fold2-merge.c:(sid:80): mset, lsum, ucons, intlist-fold2-merge.c:(sid:85): mset, lsum, ucons, intlist-fold-clone.c:(sid:168): mset, lsum, ucons, intlist-sort-merge.c:(sid:23): mset, lsum, ucons, intlist-fold2-merge.c:(sid:76): bottom intlist-sort-merge.c:(sid:13): mset, lsum, ucons, intlist-fold2-merge.c:(sid:67): mset, lsum, ucons, intlist-fold2-merge.c:(sid:48): mset, lsum, ucons, intlist-fold-clone.c:(sid:163): mset, lsum, ucons, intlist-fold2-merge.c:(sid:58): mset, lsum, ucons, intlist-fold-clone.c:(sid:158): mset, lsum, ucons, intlist-fold2-merge.c:(sid:69): mset, lsum, ucons, intlist-fold2-merge.c:(sid:70): bottom intlist-fold2-merge.c:(sid:52): mset, lsum, ucons, intlist-fold2-merge.c:(sid:67_2): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:134): mset, lsum, ucons, intlist-fold2-merge.c:(sid:99): mset, lsum, ucons, intlist-fold2-merge.c:(sid:67_1): bottom intlist-fold2-merge.c:(sid:104): mset, lsum, ucons, intlist-fold2-merge.c:(sid:63): mset, lsum, ucons, intlist-sort-merge.c:(sid:15_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:49_2): mset, lsum, ucons, intlist-fold-clone.c:(sid:144): mset, lsum, ucons, intlist-fold2-merge.c:(sid:95): bottom intlist-fold2-merge.c:(sid:49_1): bottom intlist-fold-clone.c:(sid:145): mset, lsum, ucons, intlist-fold-clone.c:(sid:146): mset, lsum, ucons, intlist-fold-clone.c:(sid:147): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:113): mset, lsum, ucons, intlist-sort-merge.c:(sid:5): mset, lsum, ucons, intlist-sort-merge.c:(sid:24): mset, lsum, ucons, intlist-fold2-merge.c:(sid:77): bottom intlist-fold-split_rec.c:(sid:129): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:118): mset, lsum, ucons, intlist-fold2-merge.c:(sid:81): mset, lsum, ucons, intlist-fold2-merge.c:(sid:72): mset, lsum, ucons, intlist-fold2-merge.c:(sid:30): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:135): mset, lsum, ucons, intlist-fold2-merge.c:(sid:31): mset, lsum, ucons, intlist-fold2-merge.c:(sid:86): mset, lsum, ucons, intlist-fold2-merge.c:(sid:32): mset, lsum, ucons, intlist-sort-merge.c:(sid:19): mset, lsum, ucons, intlist-fold2-merge.c:(sid:33): mset, lsum, ucons, intlist-fold-clone.c:(sid:164): mset, lsum, ucons, intlist-fold2-merge.c:(sid:88): mset, lsum, ucons, intlist-fold2-merge.c:(sid:34): mset, lsum, ucons, intlist-fold2-merge.c:(sid:89): bottom intlist-sort-merge.c:(sid:14): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:27_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:49): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:108): mset, lsum, ucons, intlist-fold2-merge.c:(sid:45): mset, lsum, ucons, intlist-fold-clone.c:(sid:154): mset, lsum, ucons, intlist-fold2-merge.c:(sid:96): bottom intlist-fold2-merge.c:(sid:53): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:126): mset, lsum, ucons, intlist-fold2-merge.c:(sid:100): mset, lsum, ucons, intlist-fold2-merge.c:(sid:91): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:114): mset, lsum, ucons, intlist-fold2-merge.c:(sid:0): mset, lsum, ucons, intlist-fold-clone.c:(sid:159): bottom intlist-fold2-merge.c:(sid:105): mset, lsum, ucons, intlist-fold2-merge.c:(sid:60): mset, lsum, ucons, intlist-fold2-merge.c:(sid:64): mset, lsum, ucons, intlist-fold-clone.c:(sid:13_2): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:136): mset, lsum, ucons, intlist-sort-merge.c:(sid:10): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:130): mset, lsum, ucons, intlist-sort-merge.c:(sid:25): mset, lsum, ucons, intlist-sort-merge.c:(sid:20): mset, lsum, ucons, intlist-fold2-merge.c:(sid:56): mset, lsum, ucons, intlist-sort-merge.c:(sid:6): mset, lsum, ucons, intlist-fold2-merge.c:(sid:82): mset, lsum, ucons, intlist-fold-clone.c:(sid:148): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:16_1): mset, lsum, ucons, intlist-fold-clone.c:(sid:165): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:169): bottom intlist-fold2-merge.c:(sid:73): mset, lsum, ucons, intlist-sort-merge.c:(sid:26): mset, lsum, ucons, intlist-fold2-merge.c:(sid:50): mset, lsum, ucons, intlist-fold2-merge.c:(sid:16_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:16_1): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:119): mset, lsum, ucons, intlist-sort-merge.c:(sid:21): mset, lsum, ucons, intlist-fold-clone.c:(sid:160): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:170): bottom intlist-fold2-merge.c:(sid:78): mset, lsum, ucons, intlist-fold2-merge.c:(sid:44_2): mset, lsum, ucons, intlist-sort-merge.c:(sid:15): mset, lsum, ucons, intlist-sort-merge.c:(sid:17_2): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:138): mset, lsum, ucons, intlist-sort-merge.c:(sid:17_1): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:139): mset, lsum, ucons, intlist-fold-clone.c:(sid:155): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:140): mset, lsum, ucons, intlist-fold2-merge.c:(sid:63_2): mset, lsum, ucons, intlist-fold-clone.c:(sid:17_2): bottom intlist-fold-clone.c:(sid:149): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:141): mset, lsum, ucons, intlist-fold2-merge.c:(sid:101): mset, lsum, ucons, intlist-sort-merge.c:(sid:0): mset, lsum, ucons, intlist-fold-clone.c:(sid:17_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:54): mset, lsum, ucons, intlist-fold-clone.c:(sid:151): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:109): mset, lsum, ucons, intlist-fold-clone.c:(sid:152): bottom intlist-fold2-merge.c:(sid:92): mset, lsum, ucons, intlist-fold-clone.c:(sid:0): mset, lsum, ucons, intlist-fold2-merge.c:(sid:35): mset, lsum, ucons, intlist-fold-clone.c:(sid:166): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:131): mset, lsum, ucons, intlist-fold2-merge.c:(sid:65): mset, lsum, ucons, intlist-sort-merge.c:(sid:8): mset, lsum, ucons, intlist-sort-merge.c:(sid:11): mset, lsum, ucons, intlist-fold2-merge.c:(sid:46): mset, lsum, ucons, intlist-fold2-merge.c:(sid:97): mset, lsum, ucons, intlist-fold2-merge.c:(sid:83): mset, lsum, ucons, intlist-fold2-merge.c:(sid:61): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:120): mset, lsum, ucons, intlist-sort-merge.c:(sid:16): mset, lsum, ucons, intlist-fold2-merge.c:(sid:36): mset, lsum, ucons, intlist-sort-merge.c:(sid:22): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:0): mset, lsum, ucons, intlist-fold-clone.c:(sid:161): mset, lsum, ucons, intlist-fold2-merge.c:(sid:75): mset, lsum, ucons, intlist-fold2-merge.c:(sid:55): mset, lsum, ucons, intlist-fold2-merge.c:(sid:102): mset, lsum, ucons, intlist-fold2-merge.c:(sid:79): mset, lsum, ucons, intlist-fold-split_rec.c:(sid:127): mset, lsum, ucons, intlist-fold2-merge.c:(sid:71): mset, lsum, ucons,

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists