Skip to content

Commit 0f3f6b0

Browse files
author
Daniel Kroening
committed
remove the --fixedbv command-line option
The option was marked deprecated in January 2017. A similar effect can be achieved with #define float/double __CPROVER_fixedbv[].
1 parent 955c54a commit 0f3f6b0

File tree

14 files changed

+160
-325
lines changed

14 files changed

+160
-325
lines changed

‎regression/cbmc/Fixedbv4/main.c

+33-29
Original file line numberDiff line numberDiff line change
@@ -1,61 +1,65 @@
1+
#include <assert.h>
2+
3+
typedef __CPROVER_fixedbv[32][16] fbvt;
4+
15
int main()
26
{
3-
double f;
7+
fbvt f;
48

59
// addition
610
assert(100.0+10==110);
711
assert(0+f==f);
812
assert(f+0==f);
913
assert(100+0.5==100.5);
10-
assert(0.0+0.0+f==f);
14+
assert((fbvt)0.0+(fbvt)0.0+f==f);
1115

1216
// subtraction
13-
assert(100.0-10==90);
17+
assert((fbvt)100.0-10==90);
1418
assert(0-f==-f);
1519
assert(f-0==f);
16-
assert(100-0.5==99.5);
17-
assert(0.0-0.0-f==-f);
20+
assert((fbvt)100-(fbvt)0.5==(fbvt)99.5);
21+
assert((fbvt)0.0-(fbvt)0.0-f==-f);
1822

1923
// unary minus
20-
assert(-(-100.0)==100);
21-
assert(-(1-2.0)==1);
24+
assert(-(fbvt)(-100.0)==100);
25+
assert(-(1-(fbvt)2.0)==1);
2226
assert(-(-f)==f);
2327

2428
// multiplication
25-
assert(100.0*10==1000);
29+
assert((fbvt)100.0*10==1000);
2630
assert(0*f==0);
2731
assert(f*0==0);
28-
assert(100*0.5==50);
32+
assert((fbvt)100*(fbvt)0.5==50);
2933
assert(f*1==f);
3034
assert(1*f==f);
31-
assert(1.0*1.0*f==f);
35+
assert((fbvt)1.0*(fbvt)1.0*f==f);
3236

3337
// division
34-
assert(100.0/1.0==100);
35-
assert(100.1/1.0==100.1);
36-
assert(100.0/2.0==50);
37-
assert(100.0/0.5==200);
38-
assert(0/1.0==0);
39-
assert(f/1.0==f);
38+
assert((fbvt)100.0/(fbvt)1.0==100);
39+
assert((fbvt)100.1/(fbvt)1.0==(fbvt)100.1);
40+
assert((fbvt)100.0/(fbvt)2.0==50);
41+
assert((fbvt)100.0/(fbvt)0.5==200);
42+
assert(0/(fbvt)1.0==0);
43+
assert(f/(fbvt)1.0==f);
4044

4145
// conversion
4246
assert(((double)(float)100)==100.0);
4347
assert(((unsigned int)100.0)==100.0);
4448
assert(100.0);
4549
assert(!0.0);
46-
assert((int)0.5==0);
47-
assert((int)0.49==0);
48-
assert((int)-1.5==-1);
49-
assert((int)-10.49==-10);
50+
assert((int)(fbvt)0.5==0);
51+
assert((int)(fbvt)0.49==0);
52+
assert((int)(fbvt)-1.5==-1);
53+
assert((int)(fbvt)-10.49==-10);
5054

5155
// relations
52-
assert(1.0<2.5);
53-
assert(1.0<=2.5);
54-
assert(1.01<=1.01);
55-
assert(2.5>1.0);
56-
assert(2.5>=1.0);
57-
assert(1.01>=1.01);
58-
assert(!(1.0>=2.5));
59-
assert(!(1.0>2.5));
60-
assert(1.0!=2.5);
56+
assert((fbvt)1.0<(fbvt)2.5);
57+
assert((fbvt)1.0<=(fbvt)2.5);
58+
assert((fbvt)1.01<=(fbvt)1.01);
59+
assert((fbvt)2.5>(fbvt)1.0);
60+
assert((fbvt)2.5>=(fbvt)1.0);
61+
assert((fbvt)1.01>=(fbvt)1.01);
62+
assert(!((fbvt)1.0>=(fbvt)2.5));
63+
assert(!((fbvt)1.0>(fbvt)2.5));
64+
assert((fbvt)1.0!=(fbvt)2.5);
6165
}

‎regression/cbmc/Fixedbv4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--fixedbv
3+
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc/Fixedbv6/main.c

+21-19
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,29 @@
1+
typedef __CPROVER_fixedbv[32][16] fbvt;
2+
13
int main()
24
{
35
// constants
4-
assert(1.0!=2.0);
5-
assert(1.0==1.0);
6-
assert(1.0<2.0);
7-
assert(!(-1.0<-2.0));
8-
assert(2.0>1.0);
9-
assert(!(-2.0>-1.0));
10-
assert(!(2.0<2.0));
11-
assert(!(-2.0<-2.0));
12-
assert(!(2.0>2.0));
13-
assert(!(-2.0>-2.0));
14-
assert(2.0<=2.0);
15-
assert(-2.0<=-2.0);
16-
assert(2.0>=2.0);
17-
assert(-2.0>=-2.0);
18-
assert(1.0<=2.0);
19-
assert(!(-1.0<=-2.0));
20-
assert(2.0>=1.0);
21-
assert(!(-2.0>=-1.0));
6+
assert((fbvt)1.0!=(fbvt)2.0);
7+
assert((fbvt)1.0==(fbvt)1.0);
8+
assert((fbvt)1.0<(fbvt)2.0);
9+
assert(!((fbvt)-1.0<(fbvt)-2.0));
10+
assert((fbvt)2.0>(fbvt)1.0);
11+
assert(!((fbvt)-2.0>(fbvt)-1.0));
12+
assert(!((fbvt)2.0<(fbvt)2.0));
13+
assert(!((fbvt)-2.0<(fbvt)-2.0));
14+
assert(!((fbvt)2.0>(fbvt)2.0));
15+
assert(!((fbvt)-2.0>(fbvt)-2.0));
16+
assert((fbvt)2.0<=(fbvt)2.0);
17+
assert((fbvt)-2.0<=(fbvt)-2.0);
18+
assert((fbvt)2.0>=(fbvt)2.0);
19+
assert((fbvt)-2.0>=(fbvt)-2.0);
20+
assert((fbvt)1.0<=(fbvt)2.0);
21+
assert(!((fbvt)-1.0<=(fbvt)-2.0));
22+
assert((fbvt)2.0>=(fbvt)1.0);
23+
assert(!((fbvt)-2.0>=(fbvt)-1.0));
2224

2325
// variables
24-
float a, b, _a=a, _b=b;
26+
fbvt a, b, _a=a, _b=b;
2527
__CPROVER_assume(a==1 && b==2);
2628

2729
assert(a!=b);

‎regression/cbmc/Fixedbv6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--fixedbv
3+
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc/Fixedbv7/main.c

+37-33
Original file line numberDiff line numberDiff line change
@@ -1,61 +1,65 @@
1+
#include <assert.h>
2+
3+
typedef __CPROVER_fixedbv[32][16] fbvt;
4+
15
int main()
26
{
3-
double f;
7+
fbvt f;
48

59
// addition
6-
assert(100.0+10==110);
10+
assert((fbvt)100.0+10==110);
711
assert(0+f==f);
812
assert(f+0==f);
9-
assert(100+0.5==100.5);
10-
assert(0.0+0.0+f==f);
13+
assert(100+(fbvt)0.5==(fbvt)100.5);
14+
assert((fbvt)0.0+(fbvt)0.0+f==f);
1115

1216
// subtraction
13-
assert(100.0-10==90);
17+
assert((fbvt)100.0-10==90);
1418
assert(0-f==-f);
1519
assert(f-0==f);
16-
assert(100-0.5==99.5);
17-
assert(0.0-0.0-f==-f);
20+
assert(100-(fbvt)0.5==(fbvt)99.5);
21+
assert((fbvt)0.0-(fbvt)0.0-f==-f);
1822

1923
// unary minus
20-
assert(-(-100.0)==100);
21-
assert(-(1-2.0)==1);
24+
assert(-(fbvt)(-100.0)==100);
25+
assert(-(1-(fbvt)2.0)==1);
2226
assert(-(-f)==f);
2327

2428
// multiplication
25-
assert(100.0*10==1000);
29+
assert((fbvt)100.0*10==1000);
2630
assert(0*f==0);
2731
assert(f*0==0);
28-
assert(100*0.5==50);
32+
assert(100*(fbvt)0.5==50);
2933
assert(f*1==f);
3034
assert(1*f==f);
31-
assert(1.0*1.0*f==f);
35+
assert((fbvt)1.0*(fbvt)1.0*f==f);
3236

3337
// division
34-
assert(100.0/1.0==100);
35-
assert(100.1/1.0==100.1);
36-
assert(100.0/2.0==50);
37-
assert(100.0/0.5==200);
38-
assert(0/1.0==0);
39-
assert(f/1.0==f);
38+
assert((fbvt)100.0/(fbvt)1.0==100);
39+
assert((fbvt)100.1/(fbvt)1.0==(fbvt)100.1);
40+
assert((fbvt)100.0/(fbvt)2.0==50);
41+
assert((fbvt)100.0/(fbvt)0.5==200);
42+
assert(0/(fbvt)1.0==0);
43+
assert(f/(fbvt)1.0==f);
4044

4145
// conversion
42-
assert(((double)(float)100)==100.0);
43-
assert(((unsigned int)100.0)==100.0);
46+
assert(((__CPROVER_fixedbv[40][16])(fbvt)100)==(__CPROVER_fixedbv[40][16])100.0);
47+
assert(((unsigned int)(fbvt)100.0)==100.0);
4448
assert(100.0);
4549
assert(!0.0);
46-
assert((int)0.5==0);
47-
assert((int)0.49==0);
48-
assert((int)-1.5==-1);
49-
assert((int)-10.49==-10);
50+
assert((int)(fbvt)0.5==0);
51+
assert((int)(fbvt)0.49==0);
52+
assert((int)(fbvt)-1.5==-1);
53+
assert((int)(fbvt)-10.49==-10);
5054

5155
// relations
52-
assert(1.0<2.5);
53-
assert(1.0<=2.5);
54-
assert(1.01<=1.01);
55-
assert(2.5>1.0);
56-
assert(2.5>=1.0);
57-
assert(1.01>=1.01);
58-
assert(!(1.0>=2.5));
59-
assert(!(1.0>2.5));
60-
assert(1.0!=2.5);
56+
assert((fbvt)1.0<(fbvt)2.5);
57+
assert((fbvt)1.0<=(fbvt)2.5);
58+
assert((fbvt)1.01<=(fbvt)1.01);
59+
assert((fbvt)2.5>(fbvt)1.0);
60+
assert((fbvt)2.5>=(fbvt)1.0);
61+
assert((fbvt)1.01>=(fbvt)1.01);
62+
assert(!((fbvt)1.0>=(fbvt)2.5));
63+
assert(!((fbvt)1.0>(fbvt)2.5));
64+
assert((fbvt)1.0!=(fbvt)2.5);
6165
}

‎regression/cbmc/Fixedbv7/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE
1+
KNOWNBUG
22
main.c
3-
--fixedbv --no-simplify
3+
--no-simplify
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎src/ansi-c/ansi_c_internal_additions.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,6 @@ void ansi_c_architecture_strings(std::string &code)
243243
code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
244244
code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
245245
code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
246-
code+=architecture_string(config.ansi_c.use_fixed_for_float, "fixed_for_float"); // NOLINT(whitespace/line_length)
247246
code+=architecture_string(config.ansi_c.alignment, "alignment");
248247
code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
249248
code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)

‎src/ansi-c/expr2c.cpp

-9
Original file line numberDiff line numberDiff line change
@@ -219,15 +219,6 @@ std::string expr2ct::convert_rec(
219219
{
220220
const std::size_t width=to_fixedbv_type(src).get_width();
221221

222-
if(config.ansi_c.use_fixed_for_float)
223-
{
224-
if(width==config.ansi_c.single_width)
225-
return q+"float"+d;
226-
if(width==config.ansi_c.double_width)
227-
return q+"double"+d;
228-
if(width==config.ansi_c.long_double_width)
229-
return q+"long double"+d;
230-
}
231222
const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
232223
return
233224
q+"__CPROVER_fixedbv["+std::to_string(width)+"]["+

0 commit comments

Comments
 (0)