Skip to content

GitLab

why3
why3
Commit 434cd641 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

add/sub in place

parent 1887afd9
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 125380 additions and 118906 deletions
examples/in_progress/multiprecision/Makefile
View file @ 434cd641
......@@ -2,7 +2,7 @@ all: why3 extract
why3:
make -C ../../..
extract: why3
why3 extract -D c -D mp.drv -o build/N.c -L . mp2.N
why3 extract -D c -o build/N.c -L . mp2.N
tests: extract check-gmp
gcc -O2 -Wall -g -std=gnu99 tests.c build/N.c -I$(GMP_DIR) -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o tests
gcc -O2 -Wall -g -std=gnu99 -DCOMPARE_MINI tests.c build/N.c -I$(GMP_DIR) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o minitests
......
examples/in_progress/multiprecision/bench/gmpadd
View file @ 434cd641
#an bn t(s)
2 1 0.004941
2 2 0.004393
3 1 0.007420
3 2 0.006716
3 3 0.008185
4 1 0.006072
4 2 0.008175
4 3 0.007286
4 4 0.007258
5 1 0.005710
5 2 0.006883
5 3 0.008608
5 4 0.008320
5 5 0.008141
6 1 0.006268
6 2 0.006652
6 3 0.008227
6 4 0.009744
6 5 0.009681
6 6 0.009157
7 1 0.006845
7 2 0.007867
7 3 0.007816
7 4 0.009650
7 5 0.011087
7 6 0.010619
7 7 0.010409
8 1 0.006906
8 2 0.008087
8 3 0.008404
8 4 0.009158
8 5 0.010550
8 6 0.012132
8 7 0.011996
8 8 0.011601
9 1 0.006865
9 2 0.007917
9 3 0.009011
9 4 0.009486
9 5 0.010218
9 6 0.011890
9 7 0.013563
9 8 0.013208
9 9 0.012782
10 1 0.006892
10 2 0.007845
10 3 0.008973
10 4 0.009801
10 5 0.010797
10 6 0.011624
10 7 0.013288
10 8 0.014673
10 9 0.014457
10 10 0.013995
11 1 0.007185
11 2 0.007911
11 3 0.009021
11 4 0.009818
11 5 0.010975
11 6 0.011764
11 7 0.012684
11 8 0.014426
11 9 0.015938
11 10 0.015583
11 11 0.015287
12 1 0.006915
12 2 0.008002
12 3 0.008950
12 4 0.009741
12 5 0.010876
12 6 0.012125
12 7 0.013223
12 8 0.014134
12 9 0.015525
12 10 0.016946
12 11 0.017150
12 12 0.016351
13 1 0.007183
13 2 0.008059
13 3 0.009188
13 4 0.010022
13 5 0.010960
13 6 0.012190
13 7 0.013514
13 8 0.014226
13 9 0.015388
13 10 0.016763
13 11 0.018244
13 12 0.018192
13 13 0.017653
14 1 0.007029
14 2 0.008063
14 3 0.009521
14 4 0.010569
14 5 0.011598
14 6 0.012230
14 7 0.013384
14 8 0.014742
14 9 0.015397
14 10 0.016408
14 11 0.018268
14 12 0.019582
14 13 0.019391
14 14 0.018951
15 1 0.007032
15 2 0.008430
15 3 0.009384
15 4 0.010686
15 5 0.011695
15 6 0.012788
15 7 0.013518
15 8 0.014679
15 9 0.015862
15 10 0.016615
15 11 0.017627
15 12 0.019223
15 13 0.021183
15 14 0.020701
15 15 0.020256
16 1 0.007099
16 2 0.008061
16 3 0.009214
16 4 0.010519
16 5 0.011716
16 6 0.012800
16 7 0.013678
16 8 0.014647
16 9 0.015890
16 10 0.017174
16 11 0.018056
16 12 0.018797
16 13 0.020591
16 14 0.021932
16 15 0.021984
16 16 0.021419
17 1 0.006955
17 2 0.007990
17 3 0.009340
17 4 0.010512
17 5 0.012136
17 6 0.013118
17 7 0.014121
17 8 0.014872
17 9 0.015815
17 10 0.017083
17 11 0.018140
17 12 0.019338
17 13 0.020191
17 14 0.021533
17 15 0.023332
17 16 0.023175
17 17 0.022572
18 1 0.008699
18 2 0.007945
18 3 0.009384
18 4 0.010861
18 5 0.011675
18 6 0.013154
18 7 0.014085
18 8 0.015102
18 9 0.016308
18 10 0.017090
18 11 0.018220
18 12 0.019379
18 13 0.020438
18 14 0.021576
18 15 0.022688
18 16 0.024403
18 17 0.024226
18 18 0.023891
19 1 0.009825
19 2 0.008812
19 3 0.009177
19 4 0.010556
19 5 0.011735
19 6 0.012809
19 7 0.014101
19 8 0.015300
19 9 0.016541
19 10 0.017410
19 11 0.018504
19 12 0.020095
19 13 0.020755
19 14 0.024580
19 15 0.022432
19 16 0.024169
19 17 0.025694
19 18 0.025546
19 19 0.025121
20 1 0.009701
20 2 0.009733
20 3 0.010019
20 4 0.010490
20 5 0.011610
20 6 0.012675
20 7 0.014119
20 8 0.015266
20 9 0.016381
20 10 0.017651
20 11 0.018529
20 12 0.021192
20 13 0.020809
20 14 0.021856
20 15 0.022755
20 16 0.023775
20 17 0.025533
20 18 0.026984
20 19 0.026780
20 20 0.026261
2 1 0.004937
2 2 0.004356
3 1 0.007065
3 2 0.006283
3 3 0.006133
4 1 0.005996
4 2 0.007963
4 3 0.007198
4 4 0.006925
5 1 0.005664
5 2 0.006923
5 3 0.008605
5 4 0.008553
5 5 0.007782
6 1 0.006237
6 2 0.006712
6 3 0.008137
6 4 0.009727
6 5 0.009553
6 6 0.009037
7 1 0.006866
7 2 0.007215
7 3 0.008088
7 4 0.009408
7 5 0.010832
7 6 0.010668
7 7 0.010431
8 1 0.006855
8 2 0.007914
8 3 0.008412
8 4 0.008984
8 5 0.010593
8 6 0.012107
8 7 0.012099
8 8 0.011458
9 1 0.006802
9 2 0.007921
9 3 0.008997
9 4 0.009645
9 5 0.010286
9 6 0.011956
9 7 0.013448
9 8 0.013112
9 9 0.012651
10 1 0.006854
10 2 0.007922
10 3 0.009405
10 4 0.010042
10 5 0.010848
10 6 0.011733
10 7 0.013361
10 8 0.014508
10 9 0.014388
10 10 0.013883
11 1 0.007027
11 2 0.007821
11 3 0.009026
11 4 0.009783
11 5 0.010997
11 6 0.011986
11 7 0.012653
11 8 0.014496
11 9 0.015928
11 10 0.015642
11 11 0.015156
12 1 0.007228
12 2 0.008003
12 3 0.008953
12 4 0.009891
12 5 0.011118
12 6 0.012316
12 7 0.012992
12 8 0.014203
12 9 0.015681
12 10 0.017018
12 11 0.016889
12 12 0.016328
13 1 0.006885
13 2 0.008078
13 3 0.009330
13 4 0.009983
13 5 0.011079
13 6 0.012309
13 7 0.013342
13 8 0.014437
13 9 0.015085
13 10 0.016583
13 11 0.018396
13 12 0.018348
13 13 0.017594
14 1 0.007051
14 2 0.008027
14 3 0.009121
14 4 0.010525
14 5 0.011496
14 6 0.012214
14 7 0.013336
14 8 0.014478
14 9 0.015591
14 10 0.016348
14 11 0.018041
14 12 0.019493
14 13 0.019269
14 14 0.019009
15 1 0.006930
15 2 0.007962
15 3 0.009221
15 4 0.010244
15 5 0.011532
15 6 0.012458
15 7 0.013402
15 8 0.014722
15 9 0.015730
15 10 0.016637
15 11 0.017891
15 12 0.019358
15 13 0.020901
15 14 0.020503
15 15 0.020290
16 1 0.007114
16 2 0.008221
16 3 0.009208
16 4 0.010214
16 5 0.011430
16 6 0.012963
16 7 0.013968
16 8 0.014673
16 9 0.015942
16 10 0.016902
16 11 0.017825
16 12 0.018901
16 13 0.020567
16 14 0.021822
16 15 0.021591
16 16 0.021339
17 1 0.006959
17 2 0.007953
17 3 0.009184
17 4 0.010426
17 5 0.011461
17 6 0.012746
17 7 0.013912
17 8 0.014799
17 9 0.015679
17 10 0.016938
17 11 0.018160
17 12 0.019291
17 13 0.020229
17 14 0.021547
17 15 0.023015
17 16 0.022774
17 17 0.022451
18 1 0.008591
18 2 0.008082
18 3 0.009652
18 4 0.010528
18 5 0.011504
18 6 0.012732
18 7 0.013994
18 8 0.015105
18 9 0.015987
18 10 0.017027
18 11 0.018301
18 12 0.019393
18 13 0.020314
18 14 0.021297
18 15 0.022726
18 16 0.024518
18 17 0.024337
18 18 0.023841
19 1 0.009843
19 2 0.008880
19 3 0.009296
19 4 0.010732
19 5 0.011688
19 6 0.012997
19 7 0.014206
19 8 0.015302
19 9 0.016407
19 10 0.017559
19 11 0.018173
19 12 0.019562
19 13 0.020599
19 14 0.021709
19 15 0.022567
19 16 0.024237
19 17 0.025752
19 18 0.025674
19 19 0.025200
20 1 0.009461
20 2 0.009742
20 3 0.010312
20 4 0.010588
20 5 0.011633
20 6 0.012679
20 7 0.014008
20 8 0.015089
20 9 0.016379
20 10 0.017614
20 11 0.018436
20 12 0.019554
20 13 0.020767
20 14 0.021977
20 15 0.022856
20 16 0.023780
20 17 0.025208
20 18 0.026956
20 19 0.026758
20 20 0.026437
examples/in_progress/multiprecision/bench/gmpdiv
View file @ 434cd641
#an bn t(s)
2 1 0.043699
2 2 0.049329
3 1 0.046708
3 2 0.063432
3 3 0.042070
4 1 0.054283
4 2 0.077571
4 3 0.089467
4 4 0.046544
5 1 0.061763
5 2 0.089876
5 3 0.106385
5 4 0.102456
5 5 0.045954
6 1 0.068991
6 2 0.103259
6 3 0.116560
6 4 0.131169
6 5 0.111209
6 6 0.048600
7 1 0.076612
7 2 0.118193
7 3 0.133950
7 4 0.144076
7 5 0.149833
7 6 0.118531
7 7 0.050748
8 1 0.084264
8 2 0.130553
8 3 0.153980
8 4 0.151278
8 5 0.174756
8 6 0.164003
8 7 0.121281
8 8 0.054510
9 1 0.091451
9 2 0.143720
9 3 0.173528
9 4 0.172921
9 5 0.184977
9 6 0.199405
9 7 0.173830
9 8 0.128722
9 9 0.058049
10 1 0.098818
10 2 0.157958
10 3 0.192863
10 4 0.195207
10 5 0.193434
10 6 0.218934
10 7 0.216012
10 8 0.185834
10 9 0.136447
10 10 0.055915
11 1 0.106727
11 2 0.171523
11 3 0.210439
11 4 0.218348
11 5 0.220214
11 6 0.233273
11 7 0.248101
11 8 0.230493
11 9 0.193404
11 10 0.142382
11 11 0.062313
12 1 0.113742
12 2 0.185114
12 3 0.230288
12 4 0.241638
12 5 0.247528
12 6 0.246281
12 7 0.273703
12 8 0.336447
12 9 0.246192
12 10 0.203588
12 11 0.149263
12 12 0.065651
13 1 0.121147
13 2 0.198384
13 3 0.250973
13 4 0.263012
13 5 0.272858
13 6 0.276254
13 7 0.291903
13 8 0.305127
13 9 0.287004
13 10 0.257069
13 11 0.214298
13 12 0.154311
13 13 0.071384
14 1 0.128211
14 2 0.212300
14 3 0.269714
14 4 0.286353
14 5 0.298253
14 6 0.306627
14 7 0.303433
14 8 0.332067
14 9 0.331278
14 10 0.307722
14 11 0.269047
14 12 0.224616
14 13 0.161923
14 14 0.071321
15 1 0.135617
15 2 0.225261
15 3 0.287579
15 4 0.309702
15 5 0.324281
15 6 0.336259
15 7 0.336889
15 8 0.355667
15 9 0.367920
15 10 0.356773
15 11 0.324272
15 12 0.282679
15 13 0.233243
15 14 0.167084
15 15 0.075010
16 1 0.143175
16 2 0.239497
16 3 0.307794
16 4 0.332491
16 5 0.350770
16 6 0.363953
16 7 0.471088
16 8 0.463613
16 9 0.401472
16 10 0.396611
16 11 0.376844
16 12 0.339024
16 13 0.295102
16 14 0.242436
16 15 0.174557
16 16 0.078082
17 1 0.150559
17 2 0.253078
17 3 0.327192
17 4 0.354493
17 5 0.375476
17 6 0.395437
17 7 0.403657
17 8 0.410624
17 9 0.426653
17 10 0.439582
17 11 0.424278
17 12 0.397156
17 13 0.355703
17 14 0.309768
17 15 0.254577
17 16 0.180602
17 17 0.082250
18 1 0.157930
18 2 0.266318
18 3 0.345480
18 4 0.378868
18 5 0.445719
18 6 0.427645
18 7 0.438075
18 8 0.450223
18 9 0.449063
18 10 0.559838