From patchwork Fri Jun 22 13:41:27 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Tomas_H=C3=A4rdin?= X-Patchwork-Id: 9479 Delivered-To: ffmpegpatchwork@gmail.com Received: by 2002:a02:141:0:0:0:0:0 with SMTP id c62-v6csp952031jad; Fri, 22 Jun 2018 06:41:39 -0700 (PDT) X-Google-Smtp-Source: AAOMgpfRuNgu0PU0pzaZ39QTcGqNOFfA8HlUT5K5dekAkJgy3SI7faGXcRB6o61OuuvZFImmuOvd X-Received: by 2002:adf:be81:: with SMTP id i1-v6mr1668688wrh.86.1529674899775; Fri, 22 Jun 2018 06:41:39 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1529674899; cv=none; d=google.com; s=arc-20160816; b=ehGhTHD3ezdHXOtuY+4I580TFzsyYhgx58aESTdohxLg3c+Iq3wPEypW1rrYXfSJRI dA6pMye3BIrTtOrpp8kLekyszkk7KmBb3C9arNBpeLqZVAvLiL6fxEnkGAiLl6dEn+Vn K725gvEqmCcr1fhG6X5ysHf5xSraEj3kELW7URddZxErHkd1gHanXJ/xv45rH24dNvGd 5LG3OWW09X3CRIY0Pb/1omEoausXB7CWy6DRTl3t7N/1zaZC9jH8x/HGETifRyQkIIz9 S1fAnJfTyAjGkKhClkx8+RBkXnixGcbTXerOKH8PPc6erRya+TZsceaHS2KYl++MFDv9 9QJA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence:subject :mime-version:date:to:from:message-id:dkim-signature:dkim-signature :delivered-to:arc-authentication-results; bh=LarUHOt1Abx9YowA1+C29FEJThOK72GM2Tval9Qsluc=; b=FhpMozBR+dH9mjoZ+CGvGcyHWbYwNb8uLs7T5fN9X7cwkJsfgUC3KorqOubxEKpw0O QjukjuvsFzHqU133VQFa1yxE6vQM/J/tEr9wbtdwiUuPojsMGrF11QPwg5FkN4/1uDzj RaQUjYQSQvtEanUoo7MmMFeNxSN6pJA7JViCinLBgNHUNrN6TsY1o9gTnI0uWuXLfamA itiprUVw/ec9Docb83xRKgHvNkNGrqB4Uv/jTfhZwVietpTJZ3NZ8HE+i7FNARdQTktc 4axMncUObzGavf4rweDlLYfupZ/ssFKU1X37hEda0y7s6f0WjwDpK3ms/S3QhKxC3MLM a8FQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=HaDlRUQx; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=odnrolYC; spf=pass (google.com: domain of ffmpeg-devel-bounces@ffmpeg.org designates 79.124.17.100 as permitted sender) smtp.mailfrom=ffmpeg-devel-bounces@ffmpeg.org Return-Path: Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org. [79.124.17.100]) by mx.google.com with ESMTP id e9-v6si7938859wrg.249.2018.06.22.06.41.38; Fri, 22 Jun 2018 06:41:39 -0700 (PDT) Received-SPF: pass (google.com: domain of ffmpeg-devel-bounces@ffmpeg.org designates 79.124.17.100 as permitted sender) client-ip=79.124.17.100; Authentication-Results: mx.google.com; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=HaDlRUQx; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=odnrolYC; spf=pass (google.com: domain of ffmpeg-devel-bounces@ffmpeg.org designates 79.124.17.100 as permitted sender) smtp.mailfrom=ffmpeg-devel-bounces@ffmpeg.org Received: from [127.0.1.1] (localhost [127.0.0.1]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id E3480689DCA; Fri, 22 Jun 2018 16:40:42 +0300 (EEST) X-Original-To: ffmpeg-devel@ffmpeg.org Delivered-To: ffmpeg-devel@ffmpeg.org Received: from mail.acc.umu.se (mail.acc.umu.se [130.239.18.156]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTPS id C9807689D45 for ; Fri, 22 Jun 2018 16:40:36 +0300 (EEST) Received: from localhost (localhost.localdomain [127.0.0.1]) by amavisd-new (Postfix) with ESMTP id F30B144BA6 for ; Fri, 22 Jun 2018 15:41:29 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=acc.umu.se; s=mail1; t=1529674890; bh=SkWaJMreOQSTl+VnJFYxym/dQ0Qa5/3VmT0rBv1++Pw=; h=Subject:From:To:Date:From; b=HaDlRUQx2vhxL8cTipIQieaUz7dyvKqKWyMaoT5LY0Ls5b8A0x8n8TlJ8hXFNLfZs 8Fzuyc29CylTwhQFCqnHwvi+i82tSsl8Y5pA6hV1yCc1bXnLuXqLQTF0qghRVhCKRx Itx7qmIjMQLUsgP+8WiHTEQ5LYoFpOXXIC92KtITqMj/HnAsPVSHhnYh6yWrwXETi1 +XZK7ML4S/L97ZK35DKpNJH2dvxZp7mFVxPc2HvQXrmdzTs7o4px2laYn0v8REESRi gbc6HmBZ1OHT3MOeYvh68F/PWGEVhf9mtsPXh8i72dnUR5zMUJnuEaY6zxhpIophFH GLnWyIfXi9rAA== Received: from [192.168.1.133] (h-39-105.A258.priv.bahnhof.se [79.136.39.105]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) (Authenticated sender: tjoppen) by mail.acc.umu.se (Postfix) with ESMTPSA id 1722444BA5 for ; Fri, 22 Jun 2018 15:41:27 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=acc.umu.se; s=mail1; t=1529674888; bh=SkWaJMreOQSTl+VnJFYxym/dQ0Qa5/3VmT0rBv1++Pw=; h=Subject:From:To:Date:From; b=odnrolYC9OaOLQrXSu1gNQ8/eqM6frkv2LruaMjOw+Q0cwOB9Xc1aaIC1x9gGklJv cRjoR8ABd7DB8NxithjbfYg2fDOYWnQNJ+TjUnc7Z/0lo+xcoW+qsJGTXQtPu4RZWW irusmR1Sk96szyWvu/3w31ZyRAhLrlg82TjnYYIb1WLlwWzUGOd6e8C/TtFcLmW4c2 2fqP2bKvPnD5dhLUi0jpfnLdfBJqNJhQl+ma4OaWOnB5f96iA/ktg4clmLdQQSxdXa N51X64ds337NZx6UKJYVzolQzvWaxiNhx5xORHoqKRddX1ut13DD73wSoj/gyAYRfp AVaqOAa1lWENQ== Message-ID: <1529674887.26162.7.camel@acc.umu.se> From: Tomas =?ISO-8859-1?Q?H=E4rdin?= To: FFmpeg development discussions and patches Date: Fri, 22 Jun 2018 15:41:27 +0200 X-Mailer: Evolution 3.22.6-1+deb9u1 Mime-Version: 1.0 Subject: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda) X-BeenThere: ffmpeg-devel@ffmpeg.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: FFmpeg development discussions and patches List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: FFmpeg development discussions and patches Errors-To: ffmpeg-devel-bounces@ffmpeg.org Sender: "ffmpeg-devel" Hi I've recently been looking at formal proof systems for minimizing bugs. One common example is SPARK, which is an Ada variant which uses contracts, guaranteed termination and lack of dynamic allocation to make reasoning about SPARK programs much easier. This allows automatic checking for things like overflows, out-of-bounds access and so on. A great thing for code quality. There is something similar for C called Frama-C (https://frama-c.com/). It allows you to add contracts to functions and then attempts to prove that the functions fulfill said contracts. Like SPARK it is also possible to check for things like out-of-bounds accesses or over/underflow. So I spent a few days going over qt-faststart.c (then yet again after the recent patch), adding ACSL annotations here and there, and rewriting parts of it to make the job of alt-ergo/why3/coq much easier. It's far from done, roughly 29% of goals are yet to be proven. But the purpose is to raise discussion rather than provide a perfect solution. I'd also like to know if anyone else on here has fiddled with frama-c, and might know how one could make this part of the test system. For example, I'd like a plot of % proved goals over time and the ability to fail a build if a file that was 100% proved suddenly no longer is. Doing this for a large project like FFmpeg is a serious undertaking, but something I feel should really be done for all C projects. In my case this is motivated by the recent cargo cult discussion about checks in mxfdec.c, which an automated prover could take care of. There are of course many more cases. Patch attached. One thing I discovered is that all atom parsers expect at least 8 bytes of atom data, so I was able to add contracts and checks for that. Here's what "frama-c -wp -wp-rte qt-faststart.c" says about it right now: [wp] Proved goals: 240 / 340 Qed: 156 (4ms-16ms-1.2s) Alt-Ergo: 84 (28ms-133ms-776ms) (403) (interrupted: 22) (unknown: 78) /Tomas From d4e00db4d0922e745eb23b791b4f51e9d4e4d079 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= Date: Tue, 5 Jun 2018 10:26:00 +0200 Subject: [PATCH] frama-c:ify qt-faststart.c It's far form perfect. Some modifications have been made to make it easier to prove: * some macros have been changed to inline functions * function pointers have been replaced with an integer specifying the desired callback * all atoms must be at least of size 8 (this already seemed to be the case, just not explicitly) * update_stco_offsets() got a bit of a rework --- tools/qt-faststart.c | 263 ++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 220 insertions(+), 43 deletions(-) diff --git a/tools/qt-faststart.c b/tools/qt-faststart.c index 5e88c38e6b..4b4733a418 100644 --- a/tools/qt-faststart.c +++ b/tools/qt-faststart.c @@ -42,33 +42,90 @@ #define ftello(x) _ftelli64(x) #endif -#define MIN(a,b) ((a) > (b) ? (b) : (a)) +/** +First we do Proof by Weakest Precondition Calculus. +We'll also want to do value analysis since thing can over/underflow. + +Some notes on WP options I've looked at: + +Option What I have to say What the manual says +----------------------------------------------------------------------------------------------------------------- +-wp Required to get it going Generate proof obligations for all (selected) properties. +-wp-rte For dealing with run-time exceptions? Generate RTE guards before WP. +-wp-dynamic Handle dynamic calls with specific annotations. +-wp-init-const Use initializers for global const variables. +-wp-invariants Handle generalized invariants inside loops. +-wp-split Split conjunctions into sub-goals. +-wp-model For setting memory model, such as + Hoare (simple, but incompatible with + heap memory pointers) + +frama-c -wp -wp-rte qt-faststart.c +[wp] Proved goals: 240 / 340 + Qed: 156 (4ms-18ms-1.4s) + Alt-Ergo: 84 (16ms-134ms-768ms) (403) (interrupted: 22) (unknown: 78) +*/ + +/*@ ensures a <= b ==> \result == a; + ensures a > b ==> \result == b; + assigns \nothing; + */ +static int64_t MIN(int64_t a, int64_t b) +{ + return a <= b ? a : b; +} -#define BE_32(x) (((uint32_t)(((uint8_t*)(x))[0]) << 24) | \ - (((uint8_t*)(x))[1] << 16) | \ - (((uint8_t*)(x))[2] << 8) | \ - ((uint8_t*)(x))[3]) +/*@ requires \valid(x + (0..3)); + assigns \nothing; + */ +static uint32_t BE_32(const uint8_t *x) +{ + return ((uint32_t)x[0] << 24) + + ((uint32_t)x[1] << 16) + + ((uint32_t)x[2] << 8) + + x[3]; +} -#define BE_64(x) (((uint64_t)(((uint8_t*)(x))[0]) << 56) | \ - ((uint64_t)(((uint8_t*)(x))[1]) << 48) | \ - ((uint64_t)(((uint8_t*)(x))[2]) << 40) | \ - ((uint64_t)(((uint8_t*)(x))[3]) << 32) | \ - ((uint64_t)(((uint8_t*)(x))[4]) << 24) | \ - ((uint64_t)(((uint8_t*)(x))[5]) << 16) | \ - ((uint64_t)(((uint8_t*)(x))[6]) << 8) | \ - ((uint64_t)( (uint8_t*)(x))[7])) +/*@ requires \valid(x + (0..3)); + assigns x[0..3]; + */ +static void AV_WB32(uint8_t *x, uint32_t a) +{ + x[0] = a >> 24; + x[1] = a >> 16; + x[2] = a >> 8; + x[3] = a; +} -#define AV_WB32(p, val) { \ - ((uint8_t*)(p))[0] = ((val) >> 24) & 0xff; \ - ((uint8_t*)(p))[1] = ((val) >> 16) & 0xff; \ - ((uint8_t*)(p))[2] = ((val) >> 8) & 0xff; \ - ((uint8_t*)(p))[3] = (val) & 0xff; \ - } +/*@ requires \valid(x + (0..7)); + assigns \nothing; + */ +static uint64_t BE_64(const uint8_t *x) +{ + return ((uint64_t)x[0] << 56) + + ((uint64_t)x[1] << 48) + + ((uint64_t)x[2] << 40) + + ((uint64_t)x[3] << 32) + + ((uint64_t)x[4] << 24) + + ((uint64_t)x[5] << 16) + + ((uint64_t)x[6] << 8) + + x[7]; +} -#define AV_WB64(p, val) { \ - AV_WB32(p, (val) >> 32) \ - AV_WB32(p + 4, val) \ - } +/*@ requires \valid(x + (0..7)); + assigns x[0..7]; + */ +static void AV_WB64(uint8_t *x, uint64_t a) +{ + x[0] = a >> 56; + x[1] = a >> 48; + x[2] = a >> 40; + x[3] = a >> 32; + x[4] = a >> 24; + x[5] = a >> 16; + x[6] = a >> 8; + x[7] = a; +} #define BE_FOURCC(ch0, ch1, ch2, ch3) \ ( (uint32_t)(unsigned char)(ch3) | \ @@ -122,23 +179,55 @@ typedef struct { uint64_t new_moov_size; } upgrade_stco_context_t; -typedef int (*parse_atoms_callback_t)(void *context, atom_t *atom); +//Called when fn == 0 in parse_atoms() +static int update_chunk_offsets_callback(update_chunk_offsets_context_t *context, atom_t *atom); +//Called when fn == 1 in parse_atoms() +static int upgrade_stco_callback(upgrade_stco_context_t *context, atom_t *atom); +/*@ requires size >= ATOM_PREAMBLE_SIZE; + requires \valid(buf + (0..size-1)); + ensures -1 <= \result <= 0; + + behavior update_chunk_offsets: + requires fn == 0; + requires \valid(chunk_context); + requires stco_context == NULL; + + behavior upgrade_stco: + requires fn == 1; + requires chunk_context == NULL; + requires \valid(stco_context); + + complete behaviors update_chunk_offsets, upgrade_stco; + */ static int parse_atoms( unsigned char *buf, uint64_t size, - parse_atoms_callback_t callback, - void *context) + int fn, //avoid function pointers + update_chunk_offsets_context_t *chunk_context, + upgrade_stco_context_t *stco_context) { unsigned char *pos = buf; unsigned char *end = pos + size; + //@ assert end >= pos + ATOM_PREAMBLE_SIZE; atom_t atom; int ret; + //this needs work + /*@ loop invariant \valid(pos + (0..(ATOM_PREAMBLE_SIZE-1))); + loop invariant end - pos >= ATOM_PREAMBLE_SIZE; + loop invariant \valid(pos + (0 .. (end-pos-1))); + loop assigns pos; + loop variant end - pos; + */ while (end - pos >= ATOM_PREAMBLE_SIZE) { + //@ assert \valid(pos + (0..7)); atom.size = BE_32(pos); atom.type = BE_32(pos + 4); pos += ATOM_PREAMBLE_SIZE; + //we probably need to handle pos == end specially + //@ assert pos <= end; + //@ assert pos < end ==> \valid(pos + (0 .. (end-pos-1))); atom.header_size = ATOM_PREAMBLE_SIZE; switch (atom.size) { @@ -148,6 +237,7 @@ static int parse_atoms( return -1; } + //@ assert \valid(pos + (0..7)); atom.size = BE_64(pos); pos += 8; atom.header_size = ATOM_PREAMBLE_SIZE + 8; @@ -158,6 +248,7 @@ static int parse_atoms( break; } + //@ assert atom.header_size == 8 || atom.header_size == 16; if (atom.size < atom.header_size) { fprintf(stderr, "atom size %"PRIu64" too small\n", atom.size); return -1; @@ -170,8 +261,20 @@ static int parse_atoms( return -1; } + //both callbacks expect >= 8 bytes + if (atom.size < 8) { + fprintf(stderr, "atom size %"PRIu64" too small\n", atom.size); + return -1; + } + atom.data = pos; - ret = callback(context, &atom); + //@ assert \valid(atom.data + ((-atom.header_size)..(atom.size-1))); + if (fn == 0) { + ret = update_chunk_offsets_callback(chunk_context, &atom); + } else { //1 + ret = upgrade_stco_callback(stco_context, &atom); + } + //@ assert -1 <= ret <= 0; if (ret < 0) { return ret; } @@ -182,12 +285,15 @@ static int parse_atoms( return 0; } +/*@ requires \valid(context); + requires \valid(atom); + requires 8 <= atom->size ==> \valid(atom->data + (0..(atom->size-1))); + ensures -1 <= \result <= 0; + */ static int update_stco_offsets(update_chunk_offsets_context_t *context, atom_t *atom) { uint32_t current_offset; uint32_t offset_count; - unsigned char *pos; - unsigned char *end; printf(" patching stco atom...\n"); if (atom->size < 8) { @@ -195,29 +301,48 @@ static int update_stco_offsets(update_chunk_offsets_context_t *context, atom_t * return -1; } + //@ assert atom->size >= 8; + //@ assert \valid(atom->data + (0..7)); + //@ assert \valid(atom->data + (0..(atom->size-1))); offset_count = BE_32(atom->data + 4); if (offset_count > (atom->size - 8) / 4) { fprintf(stderr, "stco offset count %"PRIu32" too big\n", offset_count); return -1; } + //@ assert offset_count*4 + 8 <= atom->size; + //@ assert \valid(atom->data + (8 .. (8 + 4*offset_count - 1))); context->stco_offset_count += offset_count; context->stco_data_size += atom->size - 8; - for (pos = atom->data + 8, end = pos + offset_count * 4; - pos < end; - pos += 4) { + /*@ loop invariant \valid(atom->data + ((8 + 4*i) .. (8 + 4*i + 3))); + loop assigns i; + loop variant offset_count - i; + */ + for (uint32_t i = 0; i < offset_count; i++) { + //@ assert \valid(atom->data + ((8 + 4*i) .. (8 + 4*i + 3))); + unsigned char *pos = atom->data + 8 + 4*i; + //@ assert \valid(pos + (0..3)); current_offset = BE_32(pos); if (current_offset > UINT_MAX - context->moov_atom_size) { context->stco_overflow = 1; + //make frama-c happy + current_offset = ((uint64_t)current_offset + (context->moov_atom_size & 0xFFFFFFFF)) & 0xFFFFFFFF; + } else { + current_offset += context->moov_atom_size; } - current_offset += context->moov_atom_size; + //@ assert \valid(pos + (0..3)); AV_WB32(pos, current_offset); } return 0; } +/*@ requires \valid(context); + requires \valid(atom); + requires 8 <= atom->size ==> \valid(atom->data + (0..(atom->size-1))); + ensures -1 <= \result <= 0; + */ static int update_co64_offsets(update_chunk_offsets_context_t *context, atom_t *atom) { uint64_t current_offset; @@ -248,9 +373,15 @@ static int update_co64_offsets(update_chunk_offsets_context_t *context, atom_t * return 0; } -static int update_chunk_offsets_callback(void *ctx, atom_t *atom) +/*@ requires \valid(context); + requires \valid(atom); + requires 8 <= atom->size; + requires 8 <= atom->header_size <= 16; + requires \valid(atom->data + ((-atom->header_size) .. (atom->size-1))); + ensures -1 <= \result <= 0; + */ +static int update_chunk_offsets_callback(update_chunk_offsets_context_t *context, atom_t *atom) { - update_chunk_offsets_context_t *context = ctx; int ret; switch (atom->type) { @@ -274,15 +405,29 @@ static int update_chunk_offsets_callback(void *ctx, atom_t *atom) ret = parse_atoms( atom->data, atom->size, - update_chunk_offsets_callback, - context); + 0, + context, + NULL); context->depth--; + //@ assert -1 <= ret <= 0; return ret; } return 0; } +/*@ behavior narrow_header: + requires header_size == 8; + requires \valid(header + (0..3)); + assigns header[0..3]; + + behavior wide_header: + requires header_size == 16; + requires \valid(header + (8..15)); + assigns header[8..15]; + + complete behaviors narrow_header, wide_header; + */ static void set_atom_size(unsigned char *header, uint32_t header_size, uint64_t size) { switch (header_size) { @@ -296,6 +441,12 @@ static void set_atom_size(unsigned char *header, uint32_t header_size, uint64_t } } +/*@ requires \valid(context); + requires \valid(atom); + requires 8 <= atom->size; + requires \valid(atom->data + (0 .. (atom->size-1))); + requires \valid(context->dest + (0..7)); + */ static void upgrade_stco_atom(upgrade_stco_context_t *context, atom_t *atom) { unsigned char *pos; @@ -325,9 +476,15 @@ static void upgrade_stco_atom(upgrade_stco_context_t *context, atom_t *atom) } } -static int upgrade_stco_callback(void *ctx, atom_t *atom) +/*@ requires \valid(context); + requires \valid(atom); + requires 8 <= atom->size; + requires 8 <= atom->header_size <= 16; + requires \valid(atom->data + ((-atom->header_size) .. (atom->size-1))); + ensures -1 <= \result <= 0; + */ +static int upgrade_stco_callback(upgrade_stco_context_t *context, atom_t *atom) { - upgrade_stco_context_t *context = ctx; unsigned char *start_pos; uint64_t copy_size; @@ -350,7 +507,8 @@ static int upgrade_stco_callback(void *ctx, atom_t *atom) if (parse_atoms( atom->data, atom->size, - upgrade_stco_callback, + 1, + NULL, context) < 0) { return -1; } @@ -369,6 +527,12 @@ static int upgrade_stco_callback(void *ctx, atom_t *atom) return 0; } +/*@ requires \valid(moov_atom); + requires \valid(moov_atom_size); + requires \valid((*moov_atom) + (0..(*moov_atom_size))); + requires *moov_atom_size >= 16; + ensures -1 <= \result <= 0; + */ static int update_moov_atom( unsigned char **moov_atom, uint64_t *moov_atom_size) @@ -382,8 +546,9 @@ static int update_moov_atom( if (parse_atoms( *moov_atom, *moov_atom_size, - update_chunk_offsets_callback, - &update_context) < 0) { + 0, + &update_context, + NULL) < 0) { return -1; } @@ -409,7 +574,8 @@ static int update_moov_atom( if (parse_atoms( *moov_atom, *moov_atom_size, - upgrade_stco_callback, + 1, + NULL, &upgrade_context) < 0) { free(new_moov_atom); return -1; @@ -427,6 +593,11 @@ static int update_moov_atom( return 0; } +/*@ requires argc >= 1; + requires \valid(argv + (0..argc-1)); + requires \forall int i; 0 <= i <= argc-1 ==> \valid(argv[i]); + ensures 0 <= \result <= 1; + */ int main(int argc, char *argv[]) { FILE *infile = NULL; @@ -450,6 +621,8 @@ int main(int argc, char *argv[]) return 0; } + //@ assert argc == 3; + //@ assert \valid(argv + (0..2)); if (!strcmp(argv[1], argv[2])) { fprintf(stderr, "input and output files need to be different\n"); return 1; @@ -485,6 +658,7 @@ int main(int argc, char *argv[]) atom_size); goto error_out; } + //@ assert \valid(ftyp_atom + (0..(ftyp_atom_size-1))); if (fseeko(infile, -ATOM_PREAMBLE_SIZE, SEEK_CUR) || fread(ftyp_atom, atom_size, 1, infile) != 1 || (start_offset = ftello(infile)) < 0) { @@ -566,6 +740,7 @@ int main(int argc, char *argv[]) fprintf(stderr, "could not allocate %"PRIu64" bytes for moov atom\n", atom_size); goto error_out; } + //@ assert \valid(moov_atom + (0..(moov_atom_size-1))); if (fread(moov_atom, atom_size, 1, infile) != 1) { perror(argv[1]); goto error_out; @@ -631,9 +806,11 @@ int main(int argc, char *argv[]) fprintf(stderr, "could not allocate %d bytes for copy_buffer\n", bytes_to_copy); goto error_out; } + //@ assert \valid(copy_buffer + (0..(bytes_to_copy-1))); printf(" copying rest of file...\n"); while (last_offset) { bytes_to_copy = MIN(bytes_to_copy, last_offset); + //@ assert \valid(copy_buffer + (0..(bytes_to_copy-1))); if (fread(copy_buffer, bytes_to_copy, 1, infile) != 1) { perror(argv[1]); -- 2.11.0