Celia

Library of linked lists

Input file intlist-fold2-merge.c:	Normalized code, input of the analysis (with statement identifiers - sid):	Computed invariants (indexed by statement identifier):
#include "intlist.h" // Merge two lists in the result. // If the two lists are sorted, the result is sorted. // Iterative version. /@ requires acyclic(x) && acyclic(y) && disjoint(x,y); / intlist fold2_merge(intlist x, intlist y) { intlist r, ri, xi, yi, tmp; int v; r = ri = xi = yi = tmp = NULL; xi = x; yi = y; while (xi != NULL && yi != NULL) { if (xi->data < yi->data) { v = xi->data; tmp = xi->next; xi = NULL; xi = tmp; tmp = NULL; } else { v = yi->data; tmp = yi->next; yi = NULL; yi = tmp; tmp = NULL; } // add v at the end of r, pointed by ri tmp = (intlist) malloc(sizeof (struct intlist_)); tmp->data = v; tmp->next = NULL; if (r == NULL) { r = tmp; ri = tmp; } else { ri->next = tmp; ri = NULL; ri = tmp; } tmp = NULL; } while (xi != NULL) { // add v at the end of r, pointed by ri tmp = (intlist) malloc(sizeof (struct intlist_)); tmp->data = xi->data; tmp->next = NULL; if (r == NULL) { r = tmp; ri = tmp; } else { ri->next = tmp; ri = NULL; ri = tmp; } tmp = NULL; tmp = xi->next; xi = NULL; xi = tmp; tmp = NULL; } while (yi != NULL) { // add v at the end of r, pointed by ri tmp = (intlist) malloc(sizeof (struct intlist_)); tmp->data = yi->data; tmp->next = NULL; if (r == NULL) { r = tmp; ri = tmp; } else { ri->next = tmp; ri = NULL; ri = tmp; } tmp = NULL; tmp = yi->next; yi = NULL; yi = tmp; tmp = NULL; } ri = NULL; /* no more used */ return r; }	/* Generated by Frama-C / 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 fold2_merge(intlist x , intlist y ) ; /File: intlist-fold2-merge.c(10,10)//@ requires //id:67 ((acyclic{ Here}(x) ∧ acyclic{Here}(y)) ∧ disjoint{ Here}(x, y)); behavior default: / intlist fold2_merge(intlist x , intlist y ) { intlist r ; intlist ri ; intlist xi ; intlist yi ; intlist tmp ; int v ; /File: intlist-fold2-merge.c//sid:1/ { /undefined sequence/ /File: intlist-fold2-merge.c//sid:2/ tmp = (struct intlist_ )((struct char_P )0); /effects: tmp <- / /File: intlist-fold2-merge.c//sid:3/ yi = tmp; /effects: yi <- / /File: intlist-fold2-merge.c//sid:4/ xi = yi; /effects: xi <- / /File: intlist-fold2-merge.c//sid:5/ ri = xi; /effects: ri <- / /File: intlist-fold2-merge.c//sid:6/ r = ri; /effects: r <- / } /File: intlist-fold2-merge.c//sid:7/ xi = x; /File: intlist-fold2-merge.c//sid:8/ yi = y; /File: intlist-fold2-merge.c//sid:9/ while (1) { /File: intlist-fold2-merge.c//sid:11/ if (xi != (struct char_P )0) { /File: intlist-fold2-merge.c//sid:13/ if (! (yi != (struct char_P )0)) { /File: intlist-fold2-merge.c//sid:14/ break; } } else { /File: intlist-fold2-merge.c//sid:15/ break; } /File: intlist-fold2-merge.c//sid:17/ if (xi->data < yi->data) { /File: intlist-fold2-merge.c//sid:18/ v = xi->data; /File: intlist-fold2-merge.c//sid:19/ tmp = xi->next; /File: intlist-fold2-merge.c//sid:20/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:21/ xi = tmp; /File: intlist-fold2-merge.c//sid:22/ tmp = (struct intlist_ )((struct char_P )0); } else { /File: intlist-fold2-merge.c//sid:23/ v = yi->data; /File: intlist-fold2-merge.c//sid:24/ tmp = yi->next; /File: intlist-fold2-merge.c//sid:25/ yi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:26/ yi = tmp; /File: intlist-fold2-merge.c//sid:27/ tmp = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:28/ tmp = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold2-merge.c//sid:29/ tmp->data = v; /File: intlist-fold2-merge.c//sid:30/ tmp->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:32/ if (r == (struct char_P )0) { /File: intlist-fold2-merge.c//sid:33/ r = tmp; /File: intlist-fold2-merge.c//sid:34/ ri = tmp; } else { /File: intlist-fold2-merge.c//sid:35/ ri->next = tmp; /File: intlist-fold2-merge.c//sid:36/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:37/ ri = tmp; } /File: intlist-fold2-merge.c//sid:38/ tmp = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:39/ while (xi != (struct char_P )0) { /File: intlist-fold2-merge.c//sid:43/ tmp = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold2-merge.c//sid:44/ tmp->data = xi->data; /File: intlist-fold2-merge.c//sid:45/ tmp->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:47/ if (r == (struct char_P )0) { /File: intlist-fold2-merge.c//sid:48/ r = tmp; /File: intlist-fold2-merge.c//sid:49/ ri = tmp; } else { /File: intlist-fold2-merge.c//sid:50/ ri->next = tmp; /File: intlist-fold2-merge.c//sid:51/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:52/ ri = tmp; } /File: intlist-fold2-merge.c//sid:53/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:54/ tmp = xi->next; /File: intlist-fold2-merge.c//sid:55/ xi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:56/ xi = tmp; /File: intlist-fold2-merge.c//sid:57/ tmp = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:58/ while (yi != (struct char_P )0) { /File: intlist-fold2-merge.c//sid:62/ tmp = (intlist )malloc(sizeof(struct intlist_ )); /File: intlist-fold2-merge.c//sid:63/ tmp->data = yi->data; /File: intlist-fold2-merge.c//sid:64/ tmp->next = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:66/ if (r == (struct char_P )0) { /File: intlist-fold2-merge.c//sid:67/ r = tmp; /File: intlist-fold2-merge.c//sid:68/ ri = tmp; } else { /File: intlist-fold2-merge.c//sid:69/ ri->next = tmp; /File: intlist-fold2-merge.c//sid:70/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:71/ ri = tmp; } /File: intlist-fold2-merge.c//sid:72/ tmp = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:73/ tmp = yi->next; /File: intlist-fold2-merge.c//sid:74/ yi = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:75/ yi = tmp; /File: intlist-fold2-merge.c//sid:76/ tmp = (struct intlist_ )((struct char_P )0); } /File: intlist-fold2-merge.c//sid:77/ ri = (struct intlist_ )((struct char_P )0); /File: intlist-fold2-merge.c//sid:78/ return (r); }	Summary: intlist-fold2-merge.c:(sid:78): mset, lsum, ucons, intlist-fold2-merge.c:(sid:69): mset, lsum, ucons, intlist-fold2-merge.c:(sid:4): mset, lsum, ucons, intlist-fold2-merge.c:(sid:67): bottom intlist-fold2-merge.c:(sid:5): mset, lsum, ucons, intlist-fold2-merge.c:(sid:6): mset, lsum, ucons, intlist-fold2-merge.c:(sid:27): mset, lsum, ucons, intlist-fold2-merge.c:(sid:49): bottom intlist-fold2-merge.c:(sid:44): mset, lsum, ucons, intlist-fold2-merge.c:(sid:44_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:53): mset, lsum, ucons, intlist-fold2-merge.c:(sid:9): mset, lsum, ucons, intlist-fold2-merge.c:(sid:47): mset, lsum, ucons, intlist-fold2-merge.c:(sid:43): mset, lsum, ucons, intlist-fold2-merge.c:(sid:17): mset, lsum, ucons, intlist-fold2-merge.c:(sid:11): mset, lsum, ucons, intlist-fold2-merge.c:(sid:58): mset, lsum, ucons, intlist-fold2-merge.c:(sid:51): mset, lsum, ucons, intlist-fold2-merge.c:(sid:21): mset, lsum, ucons, intlist-fold2-merge.c:(sid:13): mset, lsum, ucons, intlist-fold2-merge.c:(sid:60): mset, lsum, ucons, intlist-fold2-merge.c:(sid:25): mset, lsum, ucons, intlist-fold2-merge.c:(sid:14): bottom intlist-fold2-merge.c:(sid:61): bottom intlist-fold2-merge.c:(sid:63_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:19): mset, lsum, ucons, intlist-fold2-merge.c:(sid:15): bottom intlist-fold2-merge.c:(sid:34): mset, lsum, ucons, intlist-fold2-merge.c:(sid:74): mset, lsum, ucons, intlist-fold2-merge.c:(sid:38): mset, lsum, ucons, intlist-fold2-merge.c:(sid:32): mset, lsum, ucons, intlist-fold2-merge.c:(sid:23): mset, lsum, ucons, intlist-fold2-merge.c:(sid:36): mset, lsum, ucons, intlist-fold2-merge.c:(sid:67_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:68): bottom intlist-fold2-merge.c:(sid:67_1): bottom intlist-fold2-merge.c:(sid:29): mset, lsum, ucons, intlist-fold2-merge.c:(sid:49_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:63): mset, lsum, ucons, intlist-fold2-merge.c:(sid:49_1): bottom intlist-fold2-merge.c:(sid:56): mset, lsum, ucons, intlist-fold2-merge.c:(sid:72): mset, lsum, ucons, intlist-fold2-merge.c:(sid:66): mset, lsum, ucons, intlist-fold2-merge.c:(sid:28): mset, lsum, ucons, intlist-fold2-merge.c:(sid:62): mset, lsum, ucons, intlist-fold2-merge.c:(sid:77): mset, lsum, ucons, intlist-fold2-merge.c:(sid:70): mset, lsum, ucons, intlist-fold2-merge.c:(sid:22): mset, lsum, ucons, intlist-fold2-merge.c:(sid:54): mset, lsum, ucons, intlist-fold2-merge.c:(sid:45): mset, lsum, ucons, intlist-fold2-merge.c:(sid:0): mset, lsum, ucons, intlist-fold2-merge.c:(sid:52): mset, lsum, ucons, intlist-fold2-merge.c:(sid:75): mset, lsum, ucons, intlist-fold2-merge.c:(sid:20): mset, lsum, ucons, intlist-fold2-merge.c:(sid:57): mset, lsum, ucons, intlist-fold2-merge.c:(sid:26): mset, lsum, ucons, intlist-fold2-merge.c:(sid:50): mset, lsum, ucons, intlist-fold2-merge.c:(sid:7): mset, lsum, ucons, intlist-fold2-merge.c:(sid:48): bottom intlist-fold2-merge.c:(sid:30): mset, lsum, ucons, intlist-fold2-merge.c:(sid:24): mset, lsum, ucons, intlist-fold2-merge.c:(sid:39): mset, lsum, ucons, intlist-fold2-merge.c:(sid:34_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:34_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:41): mset, lsum, ucons, intlist-fold2-merge.c:(sid:18): mset, lsum, ucons, intlist-fold2-merge.c:(sid:42): bottom intlist-fold2-merge.c:(sid:37): mset, lsum, ucons, intlist-fold2-merge.c:(sid:73): mset, lsum, ucons, intlist-fold2-merge.c:(sid:17_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:64): mset, lsum, ucons, intlist-fold2-merge.c:(sid:35): mset, lsum, ucons, intlist-fold2-merge.c:(sid:17_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:33): mset, lsum, ucons, intlist-fold2-merge.c:(sid:8): mset, lsum, ucons, intlist-fold2-merge.c:(sid:71): mset, lsum, ucons, intlist-fold2-merge.c:(sid:16_2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:16_1): mset, lsum, ucons, intlist-fold2-merge.c:(sid:2): mset, lsum, ucons, intlist-fold2-merge.c:(sid:55): mset, lsum, ucons, intlist-fold2-merge.c:(sid:76): mset, lsum, ucons, intlist-fold2-merge.c:(sid:3): mset, lsum, ucons,

Plugin for Static Analysis of C Programs with Dynamic Lists

Library of linked lists