Skip to content

Commit 6d68345

Browse files
tautschnigtautschnig
committed
ansi-c library: explicit non-det initialisation, cleanup, syntax fixes
1 parent 10a0c01 commit 6d68345

File tree

15 files changed

+353
-130
lines changed

15 files changed

+353
-130
lines changed

‎src/ansi-c/library/fcntl.c‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,12 @@
55
#define __CPROVER_FCNTL_H_INCLUDED
66
#endif
77

8+
int __VERIFIER_nondet_int();
9+
810
int fcntl(int fd, int cmd, ...)
911
{
1012
__CPROVER_HIDE:;
11-
int return_value;
13+
int return_value=__VERIFIER_nondet_int();
1214
(void)fd;
1315
(void)cmd;
1416
return return_value;

‎src/ansi-c/library/getopt.c‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,11 @@ extern int optind;
88
#define __CPROVER_STRING_H_INCLUDED
99
#endif
1010

11-
inline int getopt(int argc, char * const argv[],
12-
const char *optstring)
11+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
12+
size_t __VERIFIER_nondet_size_t();
13+
14+
inline int getopt(
15+
int argc, char * const argv[], const char *optstring)
1316
{
1417
__CPROVER_HIDE:;
1518
int result=-1;
@@ -20,25 +23,26 @@ inline int getopt(int argc, char * const argv[],
2023
if(optind>=argc || argv[optind][0]!='-')
2124
return -1;
2225

23-
size_t result_index;
26+
size_t result_index=__VERIFIER_nondet_size_t();
2427
__CPROVER_assume(
2528
result_index<strlen(optstring) && optstring[result_index]!=':');
2629
#ifdef __CPROVER_STRING_ABSTRACTION
2730
__CPROVER_assert(__CPROVER_is_zero_string(optstring),
2831
"getopt zero-termination of 3rd argument");
2932
#endif
3033

31-
_Bool found;
34+
__CPROVER_bool found=__VERIFIER_nondet___CPROVER_bool();
3235
if(found)
3336
{
3437
result=optstring[result_index];
38+
__CPROVER_bool skipped=__VERIFIER_nondet___CPROVER_bool();
3539
if(skipped)
3640
++optind;
3741
}
3842

3943
if(result!=-1 && optind<argc && optstring[result_index+1]==':')
4044
{
41-
_Bool has_no_arg;
45+
__CPROVER_bool has_no_arg=__VERIFIER_nondet___CPROVER_bool();
4246
if(has_no_arg)
4347
{
4448
optarg=argv[optind];
@@ -53,10 +57,17 @@ inline int getopt(int argc, char * const argv[],
5357

5458
/* FUNCTION: getopt_long */
5559

56-
int getopt(int argc, char * const argv[], const char *optstring);
60+
#ifndef __CPROVER_GETOPT_H_INCLUDED
61+
#include <getopt.h>
62+
#define __CPROVER_GETOPT_H_INCLUDED
63+
#endif
5764

58-
inline int getopt_long(int argc, char * const argv[], const char *optstring,
59-
const struct option *longopts, int *longindex)
65+
inline int getopt_long(
66+
int argc,
67+
char * const argv[],
68+
const char *optstring,
69+
const struct option *longopts,
70+
int *longindex)
6071
{
6172
// trigger valid-pointer checks (if enabled), even though we don't
6273
// use the parameter in this model

‎src/ansi-c/library/inet.c‎

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22

33
#include <arpa/inet.h>
44

5+
in_addr_t __VERIFIER_nondet_in_addr_t();
6+
57
in_addr_t inet_addr(const char *cp)
68
{
79
__CPROVER_HIDE:;
@@ -10,12 +12,14 @@ in_addr_t inet_addr(const char *cp)
1012
__CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_addr zero-termination of argument");
1113
#endif
1214

13-
in_addr_t result;
15+
in_addr_t result=__VERIFIER_nondet_in_addr_t();
1416
return result;
1517
}
1618

1719
/* FUNCTION: inet_aton */
1820

21+
int __VERIFIER_nondet_int();
22+
1923
int inet_aton(const char *cp, struct in_addr *pin)
2024
{
2125
__CPROVER_HIDE:;
@@ -25,12 +29,14 @@ int inet_aton(const char *cp, struct in_addr *pin)
2529
__CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_aton zero-termination of name argument");
2630
#endif
2731

28-
int result;
32+
int result=__VERIFIER_nondet_int();
2933
return result;
3034
}
3135

3236
/* FUNCTION: inet_network */
3337

38+
in_addr_t __VERIFIER_nondet_in_addr_t();
39+
3440
in_addr_t inet_network(const char *cp)
3541
{
3642
__CPROVER_HIDE:;
@@ -39,6 +45,6 @@ in_addr_t inet_network(const char *cp)
3945
__CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_network zero-termination of name argument");
4046
#endif
4147

42-
in_addr_t result;
48+
in_addr_t result=__VERIFIER_nondet_in_addr_t();
4349
return result;
4450
}

‎src/ansi-c/library/math.c‎

Lines changed: 39 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -64,22 +64,17 @@ int __CPROVER_islessgreaterd(double f, double g) { return (f < g) || (f > g); }
6464

6565
/* FUNCTION: __CPROVER_isunorderedf */
6666

67-
#ifndef __CPROVER_MATH_H_INCLUDED
68-
#include <math.h>
69-
#define __CPROVER_MATH_H_INCLUDED
70-
#endif
71-
72-
int __CPROVER_isunorderedf(float f, float g) { return isnanf(f) || isnanf(g); }
67+
int __CPROVER_isunorderedf(float f, float g)
68+
{
69+
return __CPROVER_isnanf(f) || __CPROVER_isnanf(g);
70+
}
7371

7472
/* FUNCTION: __CPROVER_isunorderedd */
7573

76-
#ifndef __CPROVER_MATH_H_INCLUDED
77-
#include <math.h>
78-
#define __CPROVER_MATH_H_INCLUDED
79-
#endif
80-
81-
int __CPROVER_isunorderedd(double f, double g) { return isnan(f) || isnan(g); }
82-
74+
int __CPROVER_isunorderedd(double f, double g)
75+
{
76+
return __CPROVER_isnand(f) || __CPROVER_isnand(g);
77+
}
8378

8479
/* FUNCTION: isfinite */
8580

@@ -363,10 +358,12 @@ inline int __fpclassify(double d) {
363358

364359
/* FUNCTION: sin */
365360

361+
double __VERIFIER_nondet_double();
362+
366363
double sin(double x)
367364
{
368365
// gross over-approximation
369-
double ret;
366+
double ret=__VERIFIER_nondet_double();
370367

371368
if(__CPROVER_isinfd(x) || __CPROVER_isnand(x))
372369
__CPROVER_assume(__CPROVER_isnand(ret));
@@ -382,10 +379,12 @@ double sin(double x)
382379

383380
/* FUNCTION: sinl */
384381

382+
long double __VERIFIER_nondet_long_double();
383+
385384
long double sinl(long double x)
386385
{
387386
// gross over-approximation
388-
long double ret;
387+
long double ret=__VERIFIER_nondet_long_double();
389388

390389
if(__CPROVER_isinfld(x) || __CPROVER_isnanld(x))
391390
__CPROVER_assume(__CPROVER_isnanld(ret));
@@ -401,10 +400,12 @@ long double sinl(long double x)
401400

402401
/* FUNCTION: sinf */
403402

403+
float __VERIFIER_nondet_float();
404+
404405
float sinf(float x)
405406
{
406407
// gross over-approximation
407-
float ret;
408+
float ret=__VERIFIER_nondet_float();
408409

409410
if(__CPROVER_isinff(x) || __CPROVER_isnanf(x))
410411
__CPROVER_assume(__CPROVER_isnanf(ret));
@@ -420,10 +421,12 @@ float sinf(float x)
420421

421422
/* FUNCTION: cos */
422423

424+
double __VERIFIER_nondet_double();
425+
423426
double cos(double x)
424427
{
425428
// gross over-approximation
426-
double ret;
429+
double ret=__VERIFIER_nondet_double();
427430

428431
if(__CPROVER_isinfd(x) || __CPROVER_isnand(x))
429432
__CPROVER_assume(__CPROVER_isnand(ret));
@@ -439,10 +442,12 @@ double cos(double x)
439442

440443
/* FUNCTION: cosl */
441444

445+
long double __VERIFIER_nondet_long_double();
446+
442447
long double cosl(long double x)
443448
{
444449
// gross over-approximation
445-
long double ret;
450+
long double ret=__VERIFIER_nondet_long_double();
446451

447452
if(__CPROVER_isinfld(x) || __CPROVER_isnanld(x))
448453
__CPROVER_assume(__CPROVER_isnanld(ret));
@@ -458,11 +463,13 @@ long double cosl(long double x)
458463

459464
/* FUNCTION: cosf */
460465

466+
float __VERIFIER_nondet_float();
467+
461468
float cosf(float x)
462469
{
463470
__CPROVER_hide:;
464471
// gross over-approximation
465-
float ret;
472+
float ret=__VERIFIER_nondet_float();
466473

467474
if(__CPROVER_isinff(x) || __CPROVER_isnanf(x))
468475
__CPROVER_assume(__CPROVER_isnanf(ret));
@@ -512,11 +519,6 @@ __CPROVER_hide:;
512519

513520
/* FUNCTION: nan */
514521

515-
#ifndef __CPROVER_MATH_H_INCLUDED
516-
#include <math.h>
517-
#define __CPROVER_MATH_H_INCLUDED
518-
#endif
519-
520522
double nan(const char *str) {
521523
// the 'str' argument is not yet used
522524
__CPROVER_hide:;
@@ -526,11 +528,6 @@ double nan(const char *str) {
526528

527529
/* FUNCTION: nanf */
528530

529-
#ifndef __CPROVER_MATH_H_INCLUDED
530-
#include <math.h>
531-
#define __CPROVER_MATH_H_INCLUDED
532-
#endif
533-
534531
float nanf(const char *str) {
535532
// the 'str' argument is not yet used
536533
__CPROVER_hide:;
@@ -540,22 +537,13 @@ float nanf(const char *str) {
540537

541538
/* FUNCTION: nanl */
542539

543-
#ifndef __CPROVER_MATH_H_INCLUDED
544-
#include <math.h>
545-
#define __CPROVER_MATH_H_INCLUDED
546-
#endif
547-
548540
long double nanl(const char *str) {
549541
// the 'str' argument is not yet used
550542
__CPROVER_hide:;
551543
(void)*str;
552544
return 0.0/0.0;
553545
}
554546

555-
556-
557-
558-
559547
/* FUNCTION: nextUpf */
560548

561549
#ifndef __CPROVER_LIMITS_H_INCLUDED
@@ -738,6 +726,8 @@ __CPROVER_hide:;
738726

739727
float nextUpf(float f);
740728

729+
float __VERIFIER_nondet_float();
730+
741731
float sqrtf(float f)
742732
{
743733
__CPROVER_hide:;
@@ -750,7 +740,7 @@ float sqrtf(float f)
750740
return f;
751741
else if (__CPROVER_isnormalf(f))
752742
{
753-
float lower; // Intentionally non-deterministic
743+
float lower=__VERIFIER_nondet_float();
754744
__CPROVER_assume(lower > 0.0f);
755745
__CPROVER_assume(__CPROVER_isnormalf(lower));
756746
// Tighter bounds can be given but are dependent on the
@@ -795,7 +785,7 @@ float sqrtf(float f)
795785
// With respect to the algebra of floating point number
796786
// all subnormals seem to be perfect squares, thus ...
797787

798-
float root; // Intentionally non-deterministic
788+
float root=__VERIFIER_nondet_float();
799789
__CPROVER_assume(root >= 0.0f);
800790

801791
__CPROVER_assume(root * root == f);
@@ -823,6 +813,8 @@ float sqrtf(float f)
823813

824814
double nextUp(double d);
825815

816+
double __VERIFIER_nondet_double();
817+
826818
double sqrt(double d)
827819
{
828820
__CPROVER_hide:;
@@ -835,7 +827,7 @@ double sqrt(double d)
835827
return d;
836828
else if (__CPROVER_isnormald(d))
837829
{
838-
double lower; // Intentionally non-deterministic
830+
double lower=__VERIFIER_nondet_double();
839831
__CPROVER_assume(lower > 0.0);
840832
__CPROVER_assume(__CPROVER_isnormald(lower));
841833

@@ -867,7 +859,7 @@ double sqrt(double d)
867859
//assert(fpclassify(d) == FP_SUBNORMAL);
868860
//assert(d > 0.0);
869861

870-
double root; // Intentionally non-deterministic
862+
double root=__VERIFIER_nondet_double();
871863
__CPROVER_assume(root >= 0.0);
872864

873865
__CPROVER_assume(root * root == d);
@@ -892,6 +884,8 @@ double sqrt(double d)
892884

893885
long double nextUpl(long double d);
894886

887+
long double __VERIFIER_nondet_long_double();
888+
895889
long double sqrtl(long double d)
896890
{
897891
__CPROVER_hide:;
@@ -904,7 +898,7 @@ long double sqrtl(long double d)
904898
return d;
905899
else if (__CPROVER_isnormalld(d))
906900
{
907-
long double lower; // Intentionally non-deterministic
901+
long double lower=__VERIFIER_nondet_long_double();
908902
__CPROVER_assume(lower > 0.0l);
909903
__CPROVER_assume(__CPROVER_isnormalld(lower));
910904

@@ -936,7 +930,7 @@ long double sqrtl(long double d)
936930
//assert(fpclassify(d) == FP_SUBNORMAL);
937931
//assert(d > 0.0l);
938932

939-
long double root; // Intentionally non-deterministic
933+
long double root=__VERIFIER_nondet_long_double();
940934
__CPROVER_assume(root >= 0.0l);
941935

942936
__CPROVER_assume(root * root == d);
@@ -2316,7 +2310,7 @@ long double fabsl (long double d);
23162310

23172311
long double copysignl(long double x, long double y)
23182312
{
2319-
long double abs = fabs(x);
2313+
long double abs = fabsl(x);
23202314
return (signbit(y)) ? -abs : abs;
23212315
}
23222316

0 commit comments

Comments
 (0)