Commit e39493d3 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

[mini-gmp] use Frama-C's libc asprintf for better coverage

parent 092871ef
......@@ -15,6 +15,7 @@ MACHDEP = gcc_x86_32
CPPFLAGS += \
-std=c99 \
-I .. \
-D__gmp_asprintf=asprintf
# note: '-std=c99' is used to avoid issues with old GCCs (< 5) due to the
# presence of inline attributes.
......@@ -38,8 +39,9 @@ TARGETS = mini-gmp.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
mini-gmp.parse: \
$(shell $(FRAMAC)-config -print-share-path)/libc/stdio.c \
../tests/testutils.c \
../tests/t-add.c \
../mini-gmp.c \
../tests/hex-random.c \
../tests/mini-random.c \
fc_stubs.h \
......
#include <stdint.h>
#include <stdlib.h>
/*@
requires \valid(strp);
assigns \result, *strp \from fmt;
ensures \initialized(strp);
allocates strp;
*/
int asprintf(char **strp, const char *fmt, ...);
/*@
requires \valid(strp);
assigns \result, *strp \from fmt;
ensures \initialized(strp);
allocates strp;
*/
int __gmp_asprintf(char **strp, const char *fmt, ...);
#include "gmp.h"
/*@
assigns *a, __fc_random_counter \from __fc_random_counter;
......
directory file line function property kind status property
. mini-gmp.c 255 gmp_default_alloc precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 358 mpn_cmp initialization Unknown \initialized(ap + n)
. mini-gmp.c 358 mpn_cmp initialization Unknown \initialized(bp + n)
. mini-gmp.c 358 mpn_cmp mem_access Unknown \valid_read(ap + n)
. mini-gmp.c 358 mpn_cmp mem_access Unknown \valid_read(bp + n)
. mini-gmp.c 376 mpn_normalized_size initialization Unknown \initialized(xp + (mp_size_t)(n - 1))
. mini-gmp.c 376 mpn_normalized_size mem_access Unknown \valid_read(xp + (mp_size_t)(n - 1))
. mini-gmp.c 399 mpn_add_1 precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 403 mpn_add_1 initialization Unknown \initialized(ap + i)
. mini-gmp.c 403 mpn_add_1 mem_access Unknown \valid_read(ap + i)
. mini-gmp.c 406 mpn_add_1 mem_access Unknown \valid(rp + i)
. mini-gmp.c 422 mpn_add_n initialization Unknown \initialized(ap + i)
. mini-gmp.c 422 mpn_add_n mem_access Unknown \valid_read(ap + i)
. mini-gmp.c 422 mpn_add_n initialization Unknown \initialized(bp + i)
. mini-gmp.c 422 mpn_add_n mem_access Unknown \valid_read(bp + i)
. mini-gmp.c 427 mpn_add_n mem_access Unknown \valid(rp + i)
. mini-gmp.c 437 mpn_add precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 450 mpn_sub_1 precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 455 mpn_sub_1 initialization Unknown \initialized(ap + i)
. mini-gmp.c 455 mpn_sub_1 mem_access Unknown \valid_read(ap + i)
. mini-gmp.c 458 mpn_sub_1 mem_access Unknown \valid(rp + i)
. mini-gmp.c 475 mpn_sub_n initialization Unknown \initialized(ap + i)
. mini-gmp.c 475 mpn_sub_n mem_access Unknown \valid_read(ap + i)
. mini-gmp.c 475 mpn_sub_n initialization Unknown \initialized(bp + i)
. mini-gmp.c 475 mpn_sub_n mem_access Unknown \valid_read(bp + i)
. mini-gmp.c 479 mpn_sub_n mem_access Unknown \valid(rp + i)
. mini-gmp.c 489 mpn_sub precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 1151 mpn_limb_size_in_base_2 precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 1164 mpn_get_str_bits initialization Unknown \initialized(up + (mp_size_t)(un - 1))
. mini-gmp.c 1164 mpn_get_str_bits mem_access Unknown \valid_read(up + (mp_size_t)(un - 1))
. mini-gmp.c 1171 mpn_get_str_bits initialization Unknown \initialized(up + i)
. mini-gmp.c 1171 mpn_get_str_bits mem_access Unknown \valid_read(up + i)
. mini-gmp.c 1171 mpn_get_str_bits shift Unknown 0 ≤ shift < 32
. mini-gmp.c 1178 mpn_get_str_bits initialization Unknown \initialized(up + i)
. mini-gmp.c 1178 mpn_get_str_bits mem_access Unknown \valid_read(up + i)
. mini-gmp.c 1180 mpn_get_str_bits mem_access Unknown \valid(sp + j)
. mini-gmp.c 1284 mpn_set_str_bits signed_overflow Unknown rn + 1 ≤ 2147483647
. mini-gmp.c 1284 mpn_set_str_bits initialization Unknown \initialized(sp + j)
. mini-gmp.c 1284 mpn_set_str_bits mem_access Unknown \valid(rp + tmp)
. mini-gmp.c 1284 mpn_set_str_bits mem_access Unknown \valid_read(sp + j)
. mini-gmp.c 1289 mpn_set_str_bits initialization Unknown \initialized(rp + (mp_size_t)(rn - 1))
. mini-gmp.c 1289 mpn_set_str_bits initialization Unknown \initialized(sp + j)
. mini-gmp.c 1289 mpn_set_str_bits mem_access Unknown \valid(rp + (mp_size_t)(rn - 1))
. mini-gmp.c 1289 mpn_set_str_bits mem_access Unknown \valid_read(sp + j)
. mini-gmp.c 1911 mpz_abs_add mem_access Unknown \valid(rp + an)
. mini-gmp.c 1928 mpz_abs_sub precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 1934 mpz_abs_sub precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. mini-gmp.c 3998 mpz_sizeinbase initialization Unknown \initialized(up + (mp_size_t)(un - 1))
. mini-gmp.c 3998 mpz_sizeinbase mem_access Unknown \valid_read(up + (mp_size_t)(un - 1))
. mini-gmp.c 4091 mpz_get_str initialization Unknown \initialized(sp + i)
. mini-gmp.c 4091 mpz_get_str mem_access Unknown \valid(sp + i)
. mini-gmp.c 4091 mpz_get_str mem_access Unknown \valid_read(digits + (unsigned char)*(sp + i))
. mini-gmp.c 4093 mpz_get_str mem_access Unknown \valid(sp + sn)
. mini-gmp.c 4109 mpz_set_str initialization Unknown \initialized(sp)
. mini-gmp.c 4109 mpz_set_str mem_access Unknown \valid_read(sp)
. mini-gmp.c 4137 mpz_set_str precondition of strlen Unknown valid_string_s: valid_read_string(s)
. mini-gmp.c 4140 mpz_set_str initialization Unknown \initialized(sp)
. mini-gmp.c 4140 mpz_set_str mem_access Unknown \valid_read(sp)
. mini-gmp.c 4162 mpz_set_str mem_access Unknown \valid(dp + tmp_3)
. mini-gmp.c 4181 mpz_set_str precondition of __FC_assert Unknown nonnull_c: c ≢ 0
FRAMAC_SHARE/libc __fc_builtin.h 33 Frama_C_make_unknown precondition Unknown valid_p: \valid(p + (0 .. l - 1))
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Unknown nonnull_c: c ≢ 0
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
tests mini-random.c 30 set_str precondition of fprintf_va_3 Unknown valid_read_string(param0)
tests mini-random.c 91 mini_random_op3 precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
tests mini-random.c 92 mini_random_op3 precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
tests mini-random.c 93 mini_random_op3 precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdio.c 109 asprintf precondition of Frama_C_make_unknown Unknown valid_p: \valid(p + (0 .. l - 1))
FRAMAC_SHARE/libc stdio.c 110 asprintf mem_access Unknown \valid(*strp + (unsigned int)(len - 1U))
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_12 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_7 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc string.h 141 strlen precondition Unknown valid_string_s: valid_read_string(s)
tests mini-random.c 30 set_str precondition of fprintf_va_12 Unknown valid_read_string(param0)
tests testutils.c 159 dump precondition of fprintf_va_7 Unknown valid_read_string(param1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 47 (out of 250)
Semantically reached functions = 27
Coverage estimation = 57.4%
Syntactically reachable functions = 59 (out of 257)
Semantically reached functions = 42
Coverage estimation = 71.2%
Unreached functions (20) =
Unreached functions (17) =
<gmp.h>: __gmpz_and; __gmpz_gcd; __gmpz_ior; __gmpz_lcm; __gmpz_mul;
__gmpz_sub; __gmpz_xor;
<mini-gmp.c>: gmp_default_realloc; gmp_xrealloc_limbs; mpn_add_1; mpn_cmp4;
mpn_get_base_info; mpn_mul_1; mpn_set_str_other; mpn_sub; mpn_sub_1;
mpn_sub_n; mpz_abs_sub; mpz_realloc;
<tests/testutils.h>: dump;
<mini-gmp.c>: mpn_copyi; mpn_div_qr_1_invert; mpn_div_qr_1_preinv;
mpn_get_base_info; mpn_get_str_other; mpn_invert_3by2; mpn_limb_get_str;
mpn_lshift; mpn_mul_1; mpn_set_str_other;
[metrics] References to non-analyzed functions
------------------------------------
Function hex_random_op3 calls __gmpz_sub (at tests/hex-random.c:163)
......@@ -24,38 +23,50 @@ Function hex_random_op3 calls __gmpz_lcm (at tests/hex-random.c:188)
Function hex_random_op3 calls __gmpz_and (at tests/hex-random.c:191)
Function hex_random_op3 calls __gmpz_ior (at tests/hex-random.c:194)
Function hex_random_op3 calls __gmpz_xor (at tests/hex-random.c:197)
Function mpn_add calls mpn_add_1 (at mini-gmp.c:441)
Function mpz_abs_add calls mpz_realloc (at mini-gmp.c:1908)
Function mpz_add calls mpz_abs_sub (at mini-gmp.c:1949)
Function mpz_set_str calls mpz_realloc (at mini-gmp.c:4170)
Function mpz_get_str calls mpn_get_base_info (at mini-gmp.c:4082)
Function mpz_get_str calls mpn_copyi (at mini-gmp.c:4084)
Function mpz_get_str calls mpn_get_str_other (at mini-gmp.c:4086)
Function mpz_set_str calls mpn_get_base_info (at mini-gmp.c:4176)
Function mpz_set_str calls mpz_realloc (at mini-gmp.c:4178)
Function mpz_set_str calls mpn_set_str_other (at mini-gmp.c:4179)
Function testmain calls dump (at tests/t-add.c:46)
Function testmain calls dump (at tests/t-add.c:47)
Function testmain calls dump (at tests/t-add.c:48)
Function testmain calls dump (at tests/t-add.c:49)
Initializer of gmp_reallocate_func references gmp_default_realloc (at mini-gmp.c:284)
Function mpz_sizeinbase calls mpn_copyi (at mini-gmp.c:4016)
Function mpz_sizeinbase calls mpn_div_qr_1_invert (at mini-gmp.c:4017)
Function mpz_sizeinbase calls mpn_div_qr_1_preinv (at mini-gmp.c:4023)
[metrics] Statements analyzed by Eva
--------------------------
356 stmts in analyzed functions, 198 stmts analyzed (55.6%)
626 stmts in analyzed functions, 497 stmts analyzed (79.4%)
dump: 4 stmts out of 4 (100.0%)
gmp_default_alloc: 5 stmts out of 5 (100.0%)
gmp_default_free: 2 stmts out of 2 (100.0%)
gmp_default_realloc: 4 stmts out of 4 (100.0%)
gmp_xalloc_limbs: 2 stmts out of 2 (100.0%)
gmp_xrealloc_limbs: 3 stmts out of 3 (100.0%)
mini_random_op3: 8 stmts out of 8 (100.0%)
mpn_add: 5 stmts out of 5 (100.0%)
mpn_add_1: 13 stmts out of 13 (100.0%)
mpn_add_n: 15 stmts out of 15 (100.0%)
mpn_cmp: 14 stmts out of 14 (100.0%)
mpn_cmp4: 12 stmts out of 12 (100.0%)
mpn_get_str_bits: 26 stmts out of 26 (100.0%)
mpn_limb_size_in_base_2: 17 stmts out of 17 (100.0%)
mpn_normalized_size: 7 stmts out of 7 (100.0%)
mpn_sub: 5 stmts out of 5 (100.0%)
mpn_sub_1: 14 stmts out of 14 (100.0%)
mpn_sub_n: 14 stmts out of 14 (100.0%)
mpz_abs_add: 24 stmts out of 24 (100.0%)
mpz_abs_sub: 35 stmts out of 35 (100.0%)
mpz_add: 7 stmts out of 7 (100.0%)
mpz_clear: 2 stmts out of 2 (100.0%)
mpz_cmp: 19 stmts out of 19 (100.0%)
mpz_init: 4 stmts out of 4 (100.0%)
set_str: 5 stmts out of 5 (100.0%)
mpn_add: 4 stmts out of 5 (80.0%)
testmain: 19 stmts out of 25 (76.0%)
mpz_add: 5 stmts out of 7 (71.4%)
testfree: 3 stmts out of 3 (100.0%)
testmain: 25 stmts out of 25 (100.0%)
mpz_realloc: 14 stmts out of 15 (93.3%)
mpn_set_str_bits: 24 stmts out of 28 (85.7%)
mpz_get_str: 37 stmts out of 50 (74.0%)
mpz_set_str: 63 stmts out of 88 (71.6%)
mp_get_memory_functions: 5 stmts out of 7 (71.4%)
gmp_die: 2 stmts out of 3 (66.7%)
mpz_set_str: 51 stmts out of 88 (58.0%)
mpn_normalized_size: 4 stmts out of 7 (57.1%)
hex_random_op3: 35 stmts out of 64 (54.7%)
mpz_abs_add: 13 stmts out of 24 (54.2%)
mpz_cmp: 9 stmts out of 19 (47.4%)
mpn_cmp: 6 stmts out of 14 (42.9%)
mpn_set_str_bits: 12 stmts out of 28 (42.9%)
mpn_add_n: 6 stmts out of 15 (40.0%)
mpz_sizeinbase: 19 stmts out of 48 (39.6%)
mpn_base_power_of_two_p: 4 stmts out of 29 (13.8%)
tests/hex-random.c:151:[eva:garbled-mix] warning: The specification of function __gmpz_neg has generated a garbled mix for assigns clause *res.
tests/hex-random.c:153:[eva:garbled-mix] warning: The specification of function __gmpz_neg has generated a garbled mix for assigns clause *res.
tests/hex-random.c:160:[eva:garbled-mix] warning: The specification of function __gmpz_add has generated a garbled mix for assigns clause *res.
tests/hex-random.c:201:[eva] warning: ignoring unsupported \allocates clause
tests/hex-random.c:201:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause \result.
tests/hex-random.c:201:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause *strp.
tests/hex-random.c:202:[eva] warning: ignoring unsupported \allocates clause
tests/hex-random.c:202:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause \result.
tests/hex-random.c:202:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause *strp.
tests/hex-random.c:203:[eva] warning: ignoring unsupported \allocates clause
tests/hex-random.c:203:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause \result.
tests/hex-random.c:203:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause *strp.
tests/hex-random.c:205:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause *a.
tests/hex-random.c:206:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause *a.
tests/hex-random.c:207:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause *a.
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "assert.h"
#include "ctype.h"
#include "errno.h"
......@@ -6,10 +7,12 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.c"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
#include "sys/types.h"
#include "time.h"
#include "unistd.h"
typedef unsigned long mp_limb_t;
......@@ -488,55 +491,13 @@ void mini_random_bit_op(enum hex_random_op op, unsigned long maxbits,
void testmain(int argc, char **argv);
void dump(char const *label, __mpz_struct const x[1]);
void testhalves(int count, void (*tested_fun)(int ));
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
void testfree(void *p);
void testmain(int argc, char **argv)
{
unsigned int i;
mpz_t a;
mpz_t b;
mpz_t res;
mpz_t ref;
mpz_init(a);
mpz_init(b);
mpz_init(res);
mpz_init(ref);
i = (unsigned int)0;
while (i < (unsigned int)10000) {
{
int tmp;
mini_random_op3(OP_ADD,(unsigned long)400,a,b,ref);
mpz_add(res,(__mpz_struct const *)(a),(__mpz_struct const *)(b));
tmp = mpz_cmp((__mpz_struct const *)(res),(__mpz_struct const *)(ref));
if (tmp) {
fprintf(__fc_stderr,"mpz_add failed:\n"); /* fprintf_va_1 */
dump("a",(__mpz_struct const *)(a));
dump("b",(__mpz_struct const *)(b));
dump("r",(__mpz_struct const *)(res));
dump("ref",(__mpz_struct const *)(ref));
abort();
}
}
i ++;
}
mpz_clear(a);
mpz_clear(b);
mpz_clear(res);
mpz_clear(ref);
return;
}
void dump(char const *label, __mpz_struct const x[1]);
void mpz_set_str_or_abort(mpz_ptr z, char const *str, int base);
int const mp_bits_per_limb = (int)(sizeof(mp_limb_t) * (unsigned int)8);
/*@ requires valid_read_string(param0);
......@@ -550,12 +511,12 @@ int const mp_bits_per_limb = (int)(sizeof(mp_limb_t) * (unsigned int)8);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), *(param0 + (0 ..));
*/
int fprintf_va_2(FILE * restrict stream, char const * restrict format,
int fprintf_va_1(FILE * restrict stream, char const * restrict format,
char *param0);
static void gmp_die(char const *msg)
{
fprintf(__fc_stderr,"%s\n",(char *)msg); /* fprintf_va_2 */
fprintf(__fc_stderr,"%s\n",(char *)msg); /* fprintf_va_1 */
abort();
return;
}
......@@ -5494,6 +5455,313 @@ void *mpz_export(void *r, size_t *countp, int order, size_t size, int endian,
return r;
}
static size_t total_alloc = (unsigned int)0;
static char block_end[8] =
{(char)0x7c,
(char)0x37,
(char)0xd6,
(char)0x12,
(char)0xa8,
(char)0x6c,
(char)0x01,
(char)0xd1};
static void *block_init(size_t *block, size_t size)
{
void *__retres;
char *p;
size_t *tmp;
tmp = block;
block ++;
*tmp = size;
p = (char *)block;
memcpy((void *)(p + size),(void const *)(block_end),sizeof(block_end));
total_alloc += size;
__retres = (void *)p;
return __retres;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
static size_t *block_check(void *p)
{
int tmp;
size_t *block = (size_t *)p - 1;
size_t size = *(block + 0);
tmp = memcmp((void const *)((char *)p + size),(void const *)(block_end),
sizeof(block_end));
if (tmp != 0) {
fprintf(__fc_stderr,"red zone overwritten.\n"); /* fprintf_va_2 */
abort();
}
total_alloc -= size;
return block;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_3(FILE * restrict stream, char const * restrict format);
static void *tu_alloc(size_t size)
{
void *tmp_0;
size_t *block = malloc((sizeof(size_t) + size) + sizeof(block_end));
if (! block) {
fprintf(__fc_stderr,"Virtual memory exhausted.\n"); /* fprintf_va_3 */
abort();
}
tmp_0 = block_init(block,size);
return tmp_0;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_4(FILE * restrict stream, char const * restrict format);
static void *tu_realloc(void *p, size_t old_size, size_t new_size)
{
void *tmp_1;
size_t *block = block_check(p);
block = (size_t *)realloc((void *)block,
(sizeof(size_t) + new_size) + sizeof(block_end));
if (! block) {
fprintf(__fc_stderr,"Virtual memory exhausted.\n"); /* fprintf_va_4 */
abort();
}
tmp_1 = block_init(block,new_size);
return tmp_1;
}
static void tu_free(void *p, size_t old_size)
{
size_t *tmp;
tmp = block_check(p);
free((void *)tmp);
return;
}
void testfree(void *p)
{
void (*freefunc)(void *, size_t );
mp_get_memory_functions((void *(**)(size_t ))0,
(void *(**)(void *, size_t , size_t ))0,& freefunc);
(*freefunc)(p,(unsigned int)0);
return;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param0;
*/
int fprintf_va_5(FILE * restrict stream, char const * restrict format,
unsigned long param0);
int main(int argc, char **argv)
{
int __retres;
hex_random_init();
mp_set_memory_functions(& tu_alloc,& tu_realloc,& tu_free);
testmain(argc,argv);
if (total_alloc != (size_t)0) {
fprintf(__fc_stderr,"Memory leaked: %lu bytes.\n",
(unsigned long)total_alloc); /* fprintf_va_5 */
abort();
}
__retres = 0;
return __retres;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param0;
*/
int fprintf_va_6(FILE * restrict stream, char const * restrict format,
unsigned long param0);
void testhalves(int count, void (*tested_fun)(int ))
{
void (*freefunc)(void *, size_t );
void *(*reallocfunc)(void *, size_t , size_t );
void *(*allocfunc)(size_t );
size_t initial_alloc;
mp_get_memory_functions(& allocfunc,& reallocfunc,& freefunc);
initial_alloc = total_alloc;
(*tested_fun)(count / 2);
if (initial_alloc != total_alloc) {
fprintf(__fc_stderr,"First half, memory leaked: %lu bytes.\n",
(unsigned long)total_alloc - (unsigned long)initial_alloc); /* fprintf_va_6 */
abort();
}
mp_set_memory_functions((void *(*)(size_t ))0,
(void *(*)(void *, size_t , size_t ))0,
(void (*)(void *, size_t ))0);
(*tested_fun)(count / 2);
mp_set_memory_functions(allocfunc,reallocfunc,freefunc);
return;
}
/*@ requires valid_read_string(param0);
requires valid_read_string(param1);
requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: *(param1 + (0 ..))),
(indirect: *(param0 + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), *(param1 + (0 ..)),
*(param0 + (0 ..));
*/
int fprintf_va_7(FILE * restrict stream, char const * restrict format,
char *param0, char *param1);
void dump(char const *label, __mpz_struct const x[1])
{
char *buf = mpz_get_str((char *)0,16,x);
fprintf(__fc_stderr,"%s: %s\n",(char *)label,buf); /* fprintf_va_7 */
testfree((void *)buf);
return;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_8(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(param0);
requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), *(param0 + (0 ..));
*/
int fprintf_va_9(FILE * restrict stream, char const * restrict format,
char *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param0;
*/
int fprintf_va_10(FILE * restrict stream, char const * restrict format,
int param0);
void mpz_set_str_or_abort(mpz_ptr z, char const *str, int base)
{
int tmp;
tmp = mpz_set_str(z,str,base);
if (tmp != 0) {
fprintf(__fc_stderr,"ERROR: mpz_set_str failed\n"); /* fprintf_va_8 */
fprintf(__fc_stderr," str = \"%s\"\n",(char *)str); /* fprintf_va_9 */
fprintf(__fc_stderr," base = %d\n",base); /* fprintf_va_10 */
abort();
}
return;
}
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_11(FILE * restrict stream, char const * restrict format);
void testmain(int argc, char **argv)
{
unsigned int i;
mpz_t a;
mpz_t b;
mpz_t res;
mpz_t ref;
mpz_init(a);
mpz_init(b);
mpz_init(res);
mpz_init(ref);
i = (unsigned int)0;
while (i < (unsigned int)10000) {
{
int tmp;
mini_random_op3(OP_ADD,(unsigned long)400,a,b,ref);
mpz_add(res,(__mpz_struct const *)(a),(__mpz_struct const *)(b));
tmp = mpz_cmp((__mpz_struct const *)(res),(__mpz_struct const *)(ref));
if (tmp) {
fprintf(__fc_stderr,"mpz_add failed:\n"); /* fprintf_va_11 */
dump("a",(__mpz_struct const *)(a));
dump("b",(__mpz_struct const *)(b));
dump("r",(__mpz_struct const *)(res));
dump("ref",(__mpz_struct const *)(ref));
abort();
}
}
i ++;
}
mpz_clear(a);
mpz_clear(b);