-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathChangelog
3892 lines (3823 loc) · 240 KB
/
Changelog
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
###############################################################################
# Preliminary notes: #
# ------------------ #
# Mark "-": change with an impact for users (and possibly developers). #
# Mark "o": change with an impact for developers only. #
# Mark "+": change for Frama-C-commits audience (not in html version). #
# Mark "*": bug fixed. #
# Mark "!": change that can break compatibility with existing development. #
# '#nnn' : BTS entry #nnn #
# '#!nnn' : BTS private entry #nnn #
# '#@nnn' : Gitlab frama-c/frama-c issue #
# For compatibility with old change log formats: #
# '#?nnn' : OLD-BTS entry #nnn #
###############################################################################
##################################
Open Source Release 20.0 (Calcium)
##################################
- Eva [2019/11/25] In the summary, fixes the number of alarms by
category when the RTE plugin is used, and do not count logical
properties in dead code as proven.
-! Kernel [2019/10/31] More stringent verifications on the use of ghost
variable in non ghost-code. Fixes #2421
- MdR [2019/10/31] New plug-in Markdown-Report (MdR) for markdown and
SARIF outputs
- Eva [2019/10/23] In the summary, fixes the total number of functions
(and thus the computed analysis coverage).
- Eva [2019/10/23] New option -eva-auto-loop-unroll N to unroll all
loops whose number of iterations can be easily bounded by <N>.
- Eva [2019/10/21] New octagon domain inferring relations of the form
l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled
with option -eva-octagon-domain. Only infers relations between
pairs of scalar variables occuring in a same instruction.
Intra-procedural by default; octagons can be propagated through
function calls with option -eva-octagon-through-calls.
- ACSL [2019/10/04] Support for ghost parameters
- Eva [2019/10/04] Evaluates ACSL predicates \is_plus_infinity and
\is_minus_infinity.
- Kernel [2019/10/04] Supports macro INFINITY and NAN.
o Config [2019/09/27] ocp-indent 1.7.0 is now used for indentation
o Eva [2019/09/16] Dynamic registration of abstract values and domains:
developers of new domains no longer need to modify Eva's engine.
-* Kernel [2019/09/13] Fixes Hptmap on keys with id greater than 2^28.
-* Makefile [2019/09/12] Fixes #2378 - bytecode only compilation (patch
contributed by madroach) and use -thread where needed.
-* Eva [2019/08/21] Fixes the reduction by the negation of \initialized
and \dangling predicates on imprecise lvalues.
-* Kernel [2019/08/20] Fixes a rare but critical bug which occured when
Frama-C internally switched the current project in presence of >2
projects and destroyed the old current project at about the same
time: the Frama-C internal state became inconsistent and lead to
unsound computations and crashes. It may be revealed to the
end-user when using a long sequence of -then-replace (at least 3
of them).
-* Kernel [2019/08/20] Fixed sequence of -removed-projects and -then
options.
o Ptests [2019/08/05] Add new MODULE directive for compiling and loading
an auxiliary OCaml module for a test
- Kernel [2019/08/05] Add -keep-unused-types normalization option
- Libc [2019/08/05] Remove obsolete (and forcing cpp error) builtins.h
o! Kernel [2019/08/02] Functions over visitor's behaviors have been moved
from Cil into a new module Visitor_behavior. Apply the migration
script potassium2calcium.sh to update your plug-ins automatically.
o! Sparecode [2019/07/26] Removed from Db. Use proper Sparecode API instead.
-! Kernel [2019/07/24] OCaml version greater than or equal to 4.05.0 required.
- Kernel [2019/07/24] Improve placeholders handling in -cpp-command
o! Kernel [2019/07/23] Types in Properties are now records and not tuples
- Eva [2019/07/09] Supports ACSL floating-point comparison operators
eq_float, le_float, eq_double, le_double, etc.
o! Kernel [2019/06/28] removes AST constructors TCoerce, TCoerceE,
PLCoercion, PLCoercionE, Psubtype and PLsubtype
-* Kernel [2019/06/20] fixes dangling ref when removing unused static local
####################################
Open Source Release 19.0 (Potassium)
####################################
-* RTE [2019/05/24] fixes a crash when visiting variable declarations
- Eva [2019/04/19] The new annotation /*@ split exp; */ enumerates the
possible values of an expression and continues the analysis
for each of these value separately, until a /*@ merge exp; */
is encountered. It is also possible to maintain this partitioning
at all times with the option -eva-partition-value exp.
- Eva [2019/04/19] New option -eva-partition-history N to delay the join
of abstract states for up to N merging points, thus keeping these
states separate longer. Useful when a reasoning depends on the
path taken to reach a control point, but can increase the analysis
time exponentially in N.
- Eva [2019/04/19] Loop unroll annotations now accept non-constant but
bounded expressions as the maximum number of unrollings to perform.
-* Kernel [2019/04/09] Avoid crashing on one-letter attributes. Fixes #2432
-* Obfuscator [2019/04/09] Also obfuscate formals in function pointer types.
Fixes #2433.
- Eva [2019/04/05] Prints an analysis summary at the end, outlining the
analysis coverage and the number of errors, warnings and emitted
alarms. It can be disabled with the option -eva-msg-key=-summary
- Eva [2019/04/03] New option -eva-precision to globally configure the
analysis from 0 (fast but imprecise) to 11 (accurate but slow).
A precision of 5 is often a reasonable trade-off. This meta-option
automatically sets up other options that can also be overriden.
- Inout [2019/04/01] Fix performance issue when initializing large arrays.
- ACSL [2019/03/08] Add check annotation, similar to assert except that
it does not introduce additional hypotheses on the program state
-* Makefile [2019/03/07] Do not attempt to install .cmx on bytecode-only
architectures. Patch by M. Dogguy backported from Debian package
- Libc [2019/03/05] Better specs and removal of half-implemented ifdef
that tried to take various POSIX versions into account
-* Kernel [2019/03/05] Better detection of invalid goto in presence of VLA
(fixes #@499)
- GUI [2019/03/04] Compatibility with lablgtk3 and improved handling of
some widgets
- ACSL [2019/03/01] Clarifies which C variables are in scope under a
\at(·,L) (#@575)
- Libc [2019/02/26] Ask clang not to warn about unknown FRAMA_C_MODEL
attribute when pre-processing frama-c's libc
-* Obfuscator [2019/02/26] Obfuscate logic types and logic constructors.
-* Inout [2019/02/21] Fixes operational input on const local initialization
o RTE [2019/02/21] RTE has a static API
o Kernel [2019/02/18] When registering extended ACSL annotations, one
must now indicate whether they should have a status.
o Kernel [2019/02/05] Integer API moving closer to Zarith
- Eva [2019/01/19] New warning category for detecting loops without
'unroll' directive
- Eva [2019/01/31] Ignore annotations with "no_eva" tag
-* ACSL [2019/01/19] Accept C identifiers that happen to be ACSL keywords
in volatile and reads clauses
- Eva [2019/01/10] Improved precision on nested loops (by postponing
the widening on inner loops according to -eva-widening-period).
-* Aorai [2019/01/04] Fixes #@586: avoid removing the initial state
of the automaton
- Kernel [2019/01/03] Add attributes for loop statements to allow
distinguishing between for, while and dowhile loops.
-! Kernel [2019/01/03] Add statement attributes (sattr) to the AST. They
are not printed by default, use -kernel-msg-key printer:attrs
-! Kernel [2019/01/03] Improved precision of integer abstract bitwise
operators.
-* Eva [2018/12/17] Fixes -eva-split-return on uninitialized or escaping
function returns when -eva-warn-copy-indeterminate is disabled.
o Kernel [2018/12/11] New functions for retrieving major and minor version
-* Kernel [2018/12/04] Fixes AST integrity check wrt volatile accesses
-* Kernel [2018/11/21] Fixes #@553 - pretty-printing of basic asm template
################################
Open Source Release 18.0 (Argon)
################################
-! Kernel [2018/10/24] Log.error and Log.failure will eventually make
Frama-C exit with a non-zero status. Fixes #@552
- Kernel [2018/10/24] More ergonomic command-line options for governing
warning categories statuses.
- Eva [2018/10/24] Enable the memexec cache by default. It can be
disabled by option -eva-no-memexec.
- Eva [2018/10/22] Improved performances when the symbolic locations
domain and the memexec cache are enabled.
- Eva [2018/10/22] The memexec cache is now fully compatible with all
abstract domains provided by Eva. However, the binding to the
Apron domains disable memexec.
- Eva [2018/10/18] New experimental domain "numerors" inferring absolute
and relative errors of floating-point computations. Enabled by the
option -eva-numerors-domain. Does not handle loops for now.
-* Kernel [2018/10/18] Fixes parsing of compound initializers with anonymous
fields. Fixes #2384
-* Kernel [2018/10/16] Consider that asm can change content of pointers
used as inputs when generating assigns clauses. Fixes #@458
- Eva [2018/10/12] Remove option -obviously-terminates.
- Kernel [2018/10/05] New option -warn-invalid-bool, to warn when reading
trap representations of type _Bool.
- Eva [2018/10/04] ACSL predicates with a "no_eva" tag are now ignored.
- Eva [2018/10/03] Warn about currently unsupported specifications
of some libc functions.
- Eva [2018/10/02] Fix the gauges domain on weak bases.
- Eva [2018/10/02] Some fixes and improvements of the equality domain.
-* Kernel [2018/10/02] Rejects sizeof of an incomplete type. Fixes #@560.
-* Kernel [2018/09/26] Add attribute to allow writing into const lvals in
specific (aka C++ constructors and mutable fields) circumstances.
Fixes #2395.
- Kernel [2018/09/14] New warning (disabled by default) when multiple side
effects are unsequenced (CERT-EXP10-C recommandation).
Fixes #@492
- Eva [2018/09/13] Remove option -val-warn-left-shift-negative, and
comply with kernel option -warn-[left|right]-shift-negative.
- Kernel [2018/09/13] New options -warn-left-shift-negative (enabled by
default) and -warn-right-shift-negative (disabled by default),
to control the emission of alarms on shifts on negative integers.
o! Constant Propagation [2018/09/12] Removing Db API for Constant Propagation
plug-in. Calls to !Db.Constant_Propagation should be replaced by
calls to Constant_Propagation.Api.
- Eva [2018/09/12] Reduction of values leading to division by zero
alarms, when possible.
- Eva [2018/09/11] Better reduction of floating-point values cast into
integer types when an alarm is emitted.
- Metrics [2018/09/06] Add option -metrics-used-files, to help identify
unnecessary files given in the command line
- RTE [2018/09/05] Remove option -rte-precond.
- Eva [2018/08/31] Supports the ACSL functions \min and \max.
- Eva [2018/08/30] Fixes the alarms on subtractions and comparisons of
pointers on weak bases (created by allocations in loops).
-! ACSL [2018/08/28] Introduce extensions to global annotations and
better characterization of each extension kind.
See development guide for more information
- Eva [2018/08/28] All options of Eva start with -eva. Aliases to
previous option names preserve backward compatibility.
-! Eva [2018/08/28] Rename plug-in shortname from 'value' to 'eva'. Eva
is now properly named Eva in all logs, in the GUI, and as the
emitter of the alarms.
-! Kernel [2018/08/23] Introduce Filepath dataype for more consistent
normalization of filenames
-* Kernel [2018/08/23] Do not allow compound assignments to const variables
Fixes #@384
-! Kernel [2018/08/23] Remove option -const-writable: const globals are
unconditionally constants
-* Eva [2018/08/02] Deprecate option -val-warn-builtin-override in favor
of warning category builtins:override.
- Kernel [2018/07/26] Fix compilation on OpenBSD
patch contributed by madroach. Fixes #2379
- Kernel [2018/07/26] New option -remove-inlined to remove function(s)
after -inline-calls, add category @inline to refer to all
functions with inline attribute (for both options).
- Eva [2018/07/23] The debug category "garbled-mix" becomes a warning
category. Better track of garbled mix created by specification.
-* ACSL [2018/07/23] Avoid removing cast of void ptr used as
argument of function expecting a ptr with known size. Fixes #@432
o! Kernel [2018/07/23] Remove completely outdated module Dataflow.
Deprecated since 3+ years. Use Dataflow2 instead.
-* RTE [2018/07/23] Stop generating spurious \initialized alarms.
Fixes #@429
-* Kernel [2018/07/06] Respect relative order of labels and ACSL annots.
Fixes #@524
o* Ptests [2018/07/02] Do not keep oracles for empty stderr. Fixes #@402
-*! ACSL [2018/07/02] introduce ACSL operators \le_double, \ge_double, ...
in addition to \le_float, \ge_float, ... Remove overloading of
\le_float that made it accept double as arguments. Fixes #@502
- Eva [2018/06/28] New option -eva-report-red-statuses listing in
a csv file the properties invalid for some states of the analysis
(as in the "Red Alarms" panel of the GUI).
- Eva [2018/06/25] Release all builtins, including memset and memcpy,
as open-source.
- Eva [2018/06/15] When a cvalue builtin is used, other domains use the
frama-c libc specification to interpret the call without losing
too much information.
- Eva [2018/06/14] The variables from the frama-c libc are no longer
shown in the initial state print.
- Eva [2018/06/11] Improved precision of string builtins for strlen,
strchr and memchr.
- Eva [2018/04/25] Renamed option -wlevel into -eva-widening-delay. New
option -eva-widening-period to control the number of iterations
between two widenings.
- Eva [2018/04/25] New propagation strategy that allows unrolling loops
even when the slevel has been exceeded. Unroll the N first loop
iterations via the global option -eva-min-loop-unrolling N or via
specific code annotations /*@ loop unroll N; */. The new strategy
may affect analyses even without loop unrolling.
#####################################
Open Source Release Chlorine-20180502
#####################################
- Libc [2018/07/05] Fix C++ compatibility for Frama-Clang plug-in
#####################################
Open Source Release Chlorine-20180501
#####################################
- Eva [2018/04/25] Added scripts and templates to help automate case
studies (in $FRAMAC_SHARE/analysis-scripts)
-* Typing [2018/04/23] Stronger checks w.r.t. implicit conversions in
function pointers (must have compatible types) and assignments
(modifiable lvalues). Fixes #@479
- Kernel [2018/04/23] Added option -inline-calls for syntactic inlining
-* Kernel [2018/04/19] Avoid crash when re-declaring a function with
formals after it has been called without any. Fixes #@454
- Kernel [2018/04/13] Deprecate option -warn-decimal-float in favor of
warning category parser:decimal-float
- Kernel [2018/04/13] More possible statuses for warning categories.
Fixes #@486
o Kernel [2018/04/13] Change Cil.typeHasAttributeDeep into
Cil.typeHasAttributeMemoryBlock. Fixes #@489
o* Logic [2018/04/11] properly reset logic environment in case of typing
errors. Fixes #@326
- Eva [2018/04/10] Interpret the logic constants \pi and \e.
- Eva [2018/04/06] Initialization of volatile pointers now keeps the
base addresses of the pointer (with arbitrary offsets).
- Eva [2018/04/06] Fix the initialization of local volatile variables,
which can always have any value.
- Eva [2018/04/06] In the logic, interpret the ACSL function \sign and
the constructors \Positive and \Negative.
- Metrics [2018/04/05] When the value coverage is computed, also shows the
total number of statements by function in the filetree of the Gui.
- Gui [2018/04/04] Added Preferences menu (shortcut: Ctrl+P) to set
themes for property bullets and external source editor
o Lib [2018/03/30] New Rich_text module to create message with tags
o! Kernel [2018/03/30] Never or rarely used Log functions have been
removed or deprecated
- Eva [2018/03/15] Avoid enumeration on values with too many bases —
fixes a performance issue.
- Gui [2018/03/07] The preconditions of a function call can now be
displayed before the call statement itself (click on status
bullets with '+' or '-' to unfold/fold them)
- Typing [2018/03/02] Support for CERT EXP46-C
- Eva [2018/03/01] Fix a soundness bug in the equality domain: do not
infer incorrect equalities between incomparable pointers,
or between -0. and +0.
- Eva [2018/02/26] deprecate option -val-warn-on-alarms in favor of
warning category alarm
- Kernel [2018/02/26] deprecate option -continue-annot-error in favor of
warning category annot-error
-! Kernel [2018/02/26] introduce warning categories, with various
possible behaviors. Refactor management of debug categories
-* RTE [2018/02/23] Do not emit spurious 'idx < 0' assert
on gcc-style FAM. Fixes #@393
-* Kernel [2018/02/23] Handle anonymous struct/union init. Fixes #@376
- Eva [2018/02/22] Equalities can be propagated through function calls.
New options -eva-equality-through-calls[-function] to decide
(globally or by function) which ones are kept from the caller.
- Eva [2018/02/21] When an lvalue lv is assigned or leaves the scope,
the equality domain tries to replace lv by an equal term (if any)
in the expressions depending on lv (instead of removing them).
o! Occurrence [2018/02/20] Removing Db API for Occurrence plug-in. Calls to
!Db.Occurrence should be replaced by calls to Occurrence.Register.
o! Impact [2018/02/20] Removing Db API for Impact plug-in. Calls to
!Db.Impact should be replaced by calls to Impact.Register.
o! Users [2018/02/20] Removing Db API for Users plug-in. Calls to
!Db.Users should be replaced by calls to Users.Users_register.
- Eva [2018/02/13] Removed *_alloced_return base created for functions
without body that return pointers. Such bases were imprecise
and could be unsound in corner cases.
- Eva [2018/02/08] Shifts of addresses now create garbled mixes (as any
other arithmetic operation).
- Logic [2018/02/07] Ghost code now supports /@ ... @/ annotations
- Eva [2018/02/06] By default, do not emit pointer_comparable alarms for
non pointer operations. Always compute {0;1} for non pointer
comparisons involving incomparable addresses.
- Eva [2018/02/01] Warn about unsupported allocates clauses.
- Eva [2018/01/30] The subdivision of evaluations (through the option
-val-subdivide-non-linear) can subdivide the values of several
lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y).
- Kernel [2018/01/24] Better renaming of variables in case of name
collision.
o! Kernel [2018/01/24] Keep information about syntactic scope of local
static variables. Accessed through
Globals.Syntactic_search.find_in_scope.
-! Eva [2018/01/24] Renamed option -val-malloc-returns-null to
-val-alloc-returns-null, which also applies to realloc builtins.
- Kernel [2018/01/16] Added option -json-compilation-database to help with
preprocessing. Requires yojson during Frama-C compilation.
- Eva [2018/01/15] New function post_analysis in abstract domains,
called at the end of the analysis.
- Eva [2018/01/11] The Simple_memory functor lets builtins interpret C
functions from the value of arguments to the result value.
- Eva [2018/01/11] Evaluate the preconditions of the functions for which
a builtin is used; builtins do not emit alarms anymore.
-! Kernel [2018/01/11] Alarms Logic_memory_access and Valid_string, that
were only emitted by Eva builtins, are removed.
-* ACSL [2017/12/14] Reinforce rejection of void* pointer types in the
arguments of ACSL built-in constructs related to memory blocks
and pointer dereferencing.
-* ACSL [2017/12/14] Reinforce rejection of implicit casts from array
types to pointer types in the arguments of ACSL built-in
constructs related to memory blocks and pointer dereferencing.
-* Kernel [2017/12/13] Clean up typechecking environment when dropping
side-effects (in sizeof et al.). Fixes #@430
o! Kernel [2017/12/13] Old Cil.isCharType renamed as Cil.isAnyCharType.
New Cil.isCharType is now only true for plain char, neither signed
nor unsigned. Derived functions (isCharPtr et al.) also updated
- Eva [2017/12/12] Fix a crash when using -val-stop-at-nth-alarm.
- Eva [2017/12/07] Eva complies with option -warn-special-float, and
propagates or warns on NaN and infinite values accordingly.
-! Kernel [2017/12/07] Option -warn-not-finite-float renamed into
-warn-special-float and extended (accepts non-finite/nan/none).
- Kernel [2017/12/07] Make some typechecking warnings controllable with
-kernel-msg-key keys.
- Eva [2017/12/07] New option -val-skip-stdlib-specs, set by default.
When analyzing the body of a function from Frama-C's standard
library, specifications will be skipped.
- Eva [2017/11/28] New builtins for the single-precision mathematical
functions fmodf, cosf, sinf and atan2f.
-! Eva [2017/11/16] In the log, messages on preconditions are now
reported with the location of the call site.
o! Eva [2017/11/09] The Fval module now supports NaN and infinite values.
Major API changes in Fval, Ival and Cvalue.V (regarding casts,
mostly)
-o Eva [2017/11/09] Option -all-rounding-modes has been removed
-* Eva [2017/11/09] Fix bugs in builtins for cos and sin. The results
may be less precise than previously
- Eva [2017/11/09] Various improvements in the handling of
floating-point variables: evaluation of \is_finite, computation
of the bits of a floating-point range, etc
- Eva [2017/11/09] New panel "Red alarms" in the GUI that shows all red
statuses emitted for some states during the analysis. They are not
completely invalid, but should often be investigated first.
-* Eva [2017/10/27] Fix bug in the handling of non-explicitly volatile
fields inside volatile structs or unions
###################################
Open Source Release Sulfur-20171101
###################################
-* Eva [2017/10/27] Fix bugs when evaluating \ìnitialized, \dangling
and \separated on addresses of bitfields
-* Eva [2017/10/27] Fix bug in the handling of non-explicitly volatile
fields inside volatile structs or unions
- RTE [2017/10/27] add option -rte-initialized to generate assertions
over read accesses to potentially uninitialized locations.
-* RTE [2017/10/16] Fix bounds of alarms emitted when downcasting to
bitfields (issue #?2314)
o Makefile [2017/10/13] add gui-byte target to only build bytecode GUI
o Kernel [2017/10/11] sizeof() and alignof() applied to a function can now
be rejected when the compiler does not support this construct,
depending on the fields sizeof_fun and alignof_fun of the machdep
-* Kernel [2017/10/11] More thorough checks on l-values with function type.
Non-sensical expressions are now rejected at parsing type.
- Eva [2017/10/10] Uses assigns clauses to over-approximate the effects
of assembly statements. Warns if no assigns clause is provided.
-* Eva [2017/10/10] Fixes a performance issue in offsetmaps, that occured
when reading or copying values smaller than cells in large arrays.
- Eva [2017/10/10] The backward propagation tries to reduce integer
values by considering separately the bounds of their intervals.
-* Eva [2017/10/10] Fixes an optimization issue where the reduction by a
loop invariant just after widenings could impede the convergence.
-* Eva [2017/10/10] Fixes a soundness bug where a loop invariant could be
wrongly proved correct in some marginal cases.
+ Slicing [2017/10/05] File slicing_types/*.ml moved into slicing subdir.
- Gui [2017/09/13] In the filetree, the filter menu appears on a right
click on the header, while a left click sorts the tree.
- Metrics [2017/09/13] In the Gui, shows the percentage and the number of
dead statements (when computed) for each function of the filetree.
-! Callgraph [2017/09/01] Option -cg-init-roots replaced by -cg-service-roots
(almost equivalent); new options -cg-function-pointers (ignore
function pointers; unsound) and -cg-roots (compute subgraphs).
o! Eva [2017/09/01] In abstract domains, compute_using_specification is
replaced by logic_assign, that interprets one \assigns clause.
Complete specification are now interpreted through successive
calls to evaluate_predicate, reduce_by_predicate and logic_assign.
- Eva [2017/09/01] Various precision improvements in the interpretation
of the behaviors of a specification.
-* Kernel [2017/08/31] Fixes configure script on bytecode only architecture.
Initial version of the patch by Debian. Fixes #2325
-* Kernel [2017/08/31] Fix various typos in source code and user messages.
Patch by Debian. Fixes #2323
-! Sparecode [2017/08/31] Rename option -rm-unused-globals to
-sparecode-rm-unused-globals.
o! ACSL [2017/08/24] Refactor handling of logic labels in AST
-! Eva [2017/08/03] Fix soundness (resp. precision) bug on big-endian
(resp. little-endian) architectures. This bug triggered on
low-level code, typically when using bitfields
-* Kernel [2017/08/03] Strip bitfield attribute when performing integral
promotions on bitfields of size short or char. Fixes incorrect
attributes on the resulting expression.
-! ACSL [2017/08/03] Explicitely disallow /* and */ in ACSL annotations.
Allows to re-use logic parser for parsing annotations in external
files that can use /* ... */ as comments. As a consequence,
expressions like y/*p are thus rejected, but this was already the
case when -pp-annot is activated (default for .c files) and can
be fixed easily in y / *p (as it is pretty-printed)
-* Kernel [2017/07/29] Fix unmarshalling of save files that contain more
than 4Gb of uncompressed data. Patch from TIS-interpreter.
-* Eva [2017/07/27] Fix performance issue with the equality domain.
-! Kernel [2017/08/28] Fix invalid eids on code generated through loop
unrolling
-! Slicing [2017/08/28] Fix invalid eids on code generated through option
-slicing-level >= 2
-! Eva [2017/07/28] Fixed memory leak with option
-val-subdivide-non-linear
o! Slicing [2017/08/01] Removing Db API for Slicing plug-in. Calls to
!Db.Slicing should be replaced by calls to Slicing.Api.
-o! Slicing [2017/07/27] Removing deprecated '-slice-option' and related
!Db.Slicing.Projet.print_exported_project. Minor changes into
!Db.Slicing.Projet.extract.
o! Scope [2017/07/27] Removing Db API for Scope plug-in. Calls to
!Db.Scope should be replaced by calls to Scope.
o! Report [2017/07/24] Removing Db API for Report plug-in. Calls to
!Db.Report.print should be replaced by calls to
Report.Register.print.
- RTE [2017/07/17] Emits overflow alarms on unsigned left shift when
-warn-unsigned-overflow is enabled.
- Eva [2017/07/17] Emits overflow alarms on unsigned left shift when
-warn-unsigned-overflow is enabled.
- Kernel [2017/07/10] Composite types are now required to have equal tags
as per the C standard; no more support for isomorphic structs.
- Eva [2017/07/01] In the GUI, the "Values" panel displays the values
computed by using the properties inferred by all enabled domains.
-! Eva [2017/06/30] Better handling of function alloca(), via builtin
Frama_C_alloca.
-* Eva [2017/06/28] The cvalue states saved after each statement are now
properly deleted when an Eva parameter is changed in the GUI.
o Eva [2017/06/26] New functor in domains/simple_memory.ml to build a
complete domain from a value abstraction. The abstract states link
each scalar variable of a program to an abstract value.
- Eva [2017/06/26] New sign domain for demonstration purposes only.
-* Kernel [2017/06/09] Parser now handle mixed concatenation of
string and wstring. Fixes #@1467
- Eva [2017/06/07] The subdivision of the evaluation of non-linear
expressions (through the -val-subdivide-non-linear option) also
applies to the new evaluations requested by the equality domain.
-* Eva [2017/06/14] Fix a crash when downcasting pointer values with
the option -val-warn-signed-converted-downcast enabled.
-* Eva [2017/06/14] Fix missing alarms when downcasting pointer values.
-o Eva [2017/05/24] The argument ~with_alarms for functions of Db.Value
is now optional, and will be removed in a later version.
* Eva [2017/05/24] Fix soundness bug in string builtins where some
invalid offsets did not generate alarms.
- Eva [2017/05/22] Removes all effects of the special functions
Frama_C_[dump|show]_each on the analyses: no alarms are emitted
and the states are never reduced on these calls.
- Eva [2017/05/22] Frama_C_dump_each prints the state of each available
domain whose log category is enabled.
- Eva [2017/05/22] New directive Frama_C_domain_show_each prints the
internal properties about the arguments inferred by each available
domain whose log category is enabled.
o! Eva [2017/05/22] Abstract domains have to provide a log category and
a function show_expr that prints the internal properties inferred
about an expression.
- Kernel [2017/05/18] Added option -print-return to inline gotos to return
- RTE [2017/05/12] add -warn-not-finite-float for checking
that infinite and NaN floats are not produced.
-! Kernel [2017/05/17] qualifiers are dropped from the return type of
functions, as they make no real sense
-* Kernel [2017/04/27] stop removing const attribute on local variables.
Fixes #@301
o! Kernel [2017/04/27] Remove needless repetition of declared logic labels
in Tapp and Papp nodes. Fixes #@274
o! Kernel [2017/04/27] Completely separate types between Cil_types and
Logic_ptree, removing needless polymorphism
- Eva [2017/04/06] More precise evaluation of \initialized and
\dangling predicates.
#######################################
Open Source Release Phosphorus-20170501
#######################################
-* Eva [2017/05/08] Fix widening in the gauges domain, in particular with
nested loops and pointers that change base address through
iterations
-* Eva [2017/04/25] Perform widening in the symbolic locations domain.
-* Eva [2017/04/24] Fixes a crash when backward-propagating an imprecise
value on a 32-bits floating point addition. A non-single precision
value was erroneously returned.
-* Eva [2017/04/05] Fixes a crash with the -val-subdivide-non-linear
option, on subdivisions of evaluations involving pointer values.
-! Eva [2017/03/31] Renamed dynamic allocation builtins for
improved consistency. In particular, Frama_C_alloc_size
becomes Frama_C_malloc_fresh.
- Eva [2017/03/31] New option -val-builtins-list
-* Scope [2017/03/31] Fix bug in the functions of Db.Scope in presence of
alarms refering to volatile memory locations, or to variables
that leave scope. Also impacts Eva option -remove-redundant-alarms
- Eva [2017/03/31] Activate option -remove-redundant-alarms by default.
- Inout [2017/03/28] Option -inout-callwise is now always active, and will
be removed in a later version
-* Inout [2017/03/28] Prevent formal variables of functions with only a
specification from leaking into results
- Kernel [2017/03/28] Dynlink is now mandatory, no degraded static mode.
o! Eva [2017/03/17] Incompatible API changes in module Cvalue.Model.
Functions named 'unspecified' have been renamed into
'indeterminate', and some arguments have been removed.
o! Gui [2017/03/10] Signature change for constructor
Pretty_source.PVDecl
-! Kernel [2017/03/10] Explicit AST nodes to mark local variables
initialization.
-! Kernel [2017/03/10] Better handling of VLA (use explicit function calls
to mark deallocation of VLA at appropriate program points)
-* Callgraph [2017/03/10] Fixes inverted callers/callee in indirect calls
-! Eva [2017/03/09] Option -val-show-progress is now unset by default
-* Eva [2017/03/08] Fix bug #2277. The initial state of the analysis
now depends on all relevant options, including kernel options
-warn-...
-! Variadic [2017/03/08] Change of command line argument names for the
plugin Variadic. The new names are more expressive and avoid
confusions with the plugin Value. Use -variadic-translation or
-variadic-no-translation instead of -va or -no-va.
-! Value [2017/03/07] Support for the legacy value analysis has been
abandoned, Eva is now always active. Option -no-eva has been
removed.
-* Eva [2017/03/07] Unsound support for recursion, through option
-val-ignore-recursive-calls. The support of recursion through
the use of 'assigns' clauses, previously available in Value,
was unsound and has been removed
-! Kernel [2017/03/01] Zarith library is now required
-* Kernel [2017/02/24] Fix crash when loading a saved file without a plug-in
which has previously emitted a status with a tuning parameter.
- Eva [2017/02/06] New (internal) mechanism to handle C functions'
return values. Messages now mention \result<foo> for the
value returned by 'foo'.
- Variadic [2017/02/08] The plugin is now enabled by default. Use the
option -variadic-no-translation to keep the original behaviour.
The specification generated for the fprintf function family is
now more accurate.
- Kernel [2017/01/26] New option -print-libc, to expand include directives
for files in the Frama-C stdlib (no longer expanded by default).
-* Obfuscator [2017/01/19] Fix typo in help message (bts #2269).
- Kernel [2017/01/09] Bash completion for Frama-C options. See #@154.
-* Kernel [2016/12/09] Fixes oneret normalization in presence of
statement contract and absence of return. See #@255 and #2235.
- Kernel [2016/12/06] New option -print-machdep (help group).
- Rte [2016/11/25] Remove option -rte-all.
-* Cil [2016/11/20] Pointer subtractions with arguments of incompatible
types are now refused. The resulting expression is typed as
ptrdiff_t instead of int.
- Value [2016/11/18] Widen hints directives @widen_hints now accept
arbitrary l-values (evaluated at analysis time) in place of
variables.
-* Kernel [2016/11/17] Fixed some issues with #pragma pack() behavior,
in both GCC and MSVC machdeps. Also fixed some related issues
with __aligned__ and __packed__ attributes (including bts #2249).
-o Kernel [2016/11/17] Utility API for checking volatile attribute in Cil.
- Metrics [2016/11/17] Programmatic API for some functions via Metrics.mli.
- Kernel [2016/11/07] New option -no-autoload-plugins (equivalent to old
-no-dynlink); mostly for internal use.
-! Kernel [2016/10/19] Stricter verification for extern, static and inline
specifiers (support for CERT DCL-36-C coding rule)
o* Eva [2016/10/22] Functions Db.Value.fun_set_args and
Db.Value.globals_set_initial_state are now compatible with Eva.
######################################
Open Source Release Silicon-20161101
######################################
-*! Eva [2016/10/29] Fix soundness bug on statements with RTE or
programmatically-added user assertions (bts #2258). This
leads to minor changes in the way states are propagated when
all slevel has been consumed. Also, consolidated states now
return the abstraction before any reduction by assertions or
alarms.
-* Eva [2016/10/20] Fix bug in the bitwise domain, on some applications
of the & and | operators
- Value [2016/10/20] New (experimental) option -val-builtins-auto, to
automatically replace known C functions by builtins. Will
be set by default in Phosphorus.
-* Value [2016/10/19] Frama_C_cos and Frama_C_sin builtins are now
precise by default. The former Frama_C_cos / Frama_Csin_precise
have been removed
-* Kernel [2016/10/18] Fix bug when pretty printing an ACSL term
"divisor / *p" (bts #2250).
- Eva [2016/10/18] New experimental Gauges domain, that relates
integer variable to loop counters.
-! Kernel [2016/10/15] Fix major bug in the backward dataflow of module
Dataflows
-! Scope [2016/10/15] Fix bug that might lead to unsoundness and / or
looping in 'Datascope' functionality (#!235)
-* Eva [2016/10/11] Prevent incorrect reductions on memory locations
with volatile qualifier
-! Value [2016/10/11] Option -val-warn-copy-indeterminate is now set by
default. See command-line help if you want to deactivate it.
- Kernel [2016/10/07] Fix bug that may occur when modifying several times
command line-options taking functions as argument (issue #@109)
-! Libc [2016/10/07] Functions in share/libc.c have been inlined into
the proper .c files under share/libc
- Eva [2016/10/07] More systematic backward-propagation between
actual parameters and formals
- Nonterm [2016/10/05] overall increase in precision, especially on
compound statements (if, switch, loops...). Verbosity has been
decreased
- Nonterm [2016/10/05] New options -nonterm-ignore f1,..,fn (to
ignore calls to functions f1,..,fn) and -nonterm-dead-code
(to warn about syntactically dead code)
- Value [2016/09/23] Extended support for syntactic widening hints
(@widen_hints - see the Value user manual for more details)
- Value [2016/09/20] New builtins for string-related functions:
Frama_C_strlen, Frama_C_strchr, Frama_C_strnlen,
Frama_C_memchr and Frama_C_rawmemchr
- Value [2016/09/20] valid_string and valid_read_string predicates
are now evaluated by Value
-* Eva [2016/09/18] Fix bug in equality domain, after assignements
lv = e where the modified locations intersect those involved in
computing lv
-* Eva [2016/09/18] fix performance bug in the equality domain,
especially visible on programs with many local variables.
o! Kernel [2016/09/16] Rename some types of the logic AST for more coherence
- Kernel [2016/09/13] Support for C11 redefinition of typedefs
- Kernel [2016/09/06] Deprecated Pretty_utils.sfprintf,
use Format.asprintf instead.
-! Logic [2016/08/31] Refactoring of ACSL extensions + allow extensions
in loop annotations
-! Libc [2016/08/29] New file share/libc/string.c, with simple
implementations for C99 functions defined in string.h.
Duplicate implementations were removed from share/libc.c.
-* Kernel [2016/08/12] Fix bug #2239 about unsoundness of callgraph's
services computation (bug introduced in Frama-C Magnesium).
o! Kernel [2016/07/26] Suppress return_stmt field of kernel_function type.
Use Kernel_function.find_return instead.
-* Kernel [2016/07/31] Scripts that use Gtk can again be loaded using
option -load-script (bug report:
http://stackoverflow.com/questions/38677256/)
-! From [2016/07/28] Removed options -experimental-path-deps and
-experimental-mem-deps.
-! Value [2016/06/26] Do not compute the sizeof of a function when
evaluating a function call through a pointer. This avoids some
warnings in MSVC mode.
-! Value [2016/06/26] Option -val-show-time has been removed. Options
-val-show-perf or -val-flamegraph offer more information
- Value [2016/06/26] New option -val-flamegraph, to dump information about
analysis times as a Flamegraph
-* Value [2016/06/26] Option -val-show-perf now properly takes into
account the time taken by the main function itself (without its
callees)
-! Kernel [2016/06/14] OCamlGraph is no longer packaged within Frama-C,
and must be installed to build Frama-C from source
o! Kernel [2016/06/14] Remove class Filecheck.check from API.
Use Filecheck.check_ast that provides the correct encapsulation.
- Eva [2016/06/11] Various improvements to experimental Apron domain
- Value [2016/06/11] Pointers to functions with an incompatible type are
now handled in a more stringent manner. Previously, arguments
with incompatibles types but equal size were reported with an
orange status. Now, any mismatch (e.g. int/float or
signed/unsigned) causes a red alarm.
-* Eva [2016/06/06] Setting option -val-warn-copy-indeterminate now
forces lvalue copies to perform a full evaluation. This includes
converting the copied value to the proper type, and emitting
alarms if it is indeterminate. This option should not be set
for memcpy-like functions, or for functions that copy bits
of pointers
-! Value [2016/06/05] API changes in modules Lmap and Cvalue.Model. All
occurrences of `Map in returned value should be replaced by
`Value
-! Value [2016/06/03] Several warnings emitted by Value are now properly
prefixed by [value] instead of [kernel]
- Value [2016/05/31] New message key 'garbled-mix', to track garbled mix
generated during the analysis
-* Value [2016/05/30] Garbled mix created when analyzing assigns / from
clauses are now tagged as having "Library function" origin
- Value [2016/05/30] New option -val-warn-on-alarms, which governs
whether alarms are printed as warnings or text.
-* Kernel [2016/05/23] Side-effect free instructions such as 'e;' are now
translated as 'tmp = e;' instead of 'if (e) {}' (which was
incorrect when e did not have a scalar type)
- Eva [2016/05/27] Improvements to option -val-subdivide-non-linear for
high number of subdivisions
-* Value [2016/05/23] Option -val-show-initial-state has been removed.
Instead, -value-msg-key=-initial-state can be used
- Value [2016/05/23] New message key final-states, that can be used
to deactivate the printing of the abstract states at the end of
each function
o* Kernel [2016/05/18] Fixes merging of contract when using
Annotations.add_code_annot
- Rte [2016/05/15] New option -rte-pointer-call, to generate
annotations for calls through function pointers
-* Value [2016/05/15] Fix crash when extracting bits of a long double
value. (Issue 92 on TIS-interpreter, reported by ch3root.).
- Value [2016/05/14] Builtins are now available for malloc:
Frama_C_alloc_size (one new base each time, may diverge) and
Frama_C_alloc_by_stack (one base by stack, may end up performing
weak updates).
-! Cil [2016/05/12] Conversions between a bit-field lvalue and the
(integral) type of the bitfield are now always made explicit
through casts; the attribute FRAMA_C_BITFIELD_SIZE is present on
the type of the cast if needed.
- Libc [2016/05/03] Implementations of some functions of the standard
library are now available in share/libc/*.c
-* Makefile [2016/04/27] Fix compilation of plug-ins which depends on
another plug-ins when compiled outside Frama-C.
- Gui [2016/04/24] Different filters for user assertions and RTEs
are now available.
- Eva [2016/04/05] Improvements to option -val-subdivide-non-linear on
expressions such as x*x+y*y, or t[i*i].
- Eva [2016/04/01] Support for options -warn-signed-downcast and
-warn-unsigned-downcast.
-! Kernel [2016/03/31] OCaml version greater than or equal to 4.02.3 required.
o Makefile [2016/03/31] Warnings and warn-error are activated only if a file
.for_devel is present along side the Makefile (also for plugins)
o! Kernel [2016/03/29] Functions Integer.pgcd and Integer.ppcm are now
guaranteed to return a positive result.
######################################
Open Source Release Aluminium-20160502
######################################
- Value [2016/04/19] Support for evaluation of predicate
\valid_read_string on constant strings.
-* Sparecode [2016/04/11] Fix crash when an entire function becomes spare.
(issue #@157).
- Eva [2016/03/30] New experimental domain that improves precision on
bitwise operations, for example on pointers. Activated by option
-eva-bitwise-domain.
o! Value [2016/03/30] API change in functor Lmap.Make.
- LoopAnalysis [2016/03/29] New plug-in 'LoopAnalysis' which estimates loop
bounds and -slevel-function parameters. Invoked using option
-loop.
-* ACSL [2016/03/30] Fixes precedence uncompliance within ACSL Manual of
some bitwise operators and more aggressive checks of consistent
relation chains.
-* Metrics [2016/03/24] Fix list of undefined functions; functions that
are never called were not reported.
-* Metrics [2016/03/24] Fix option -metrics-value-cover when option
-metrics-libc is not set.
-! Metrics [2016/03/24] Global variables defined in Frama-C standard library
are no longer counted when option -metrics-libc is not set.
- Variadic [2016/03/17] New plug-in 'Variadic' which translates variadic
functions, calls and macros to allow analyses to handle them more
easily. Invoked using the -va option.
- Nonterm [2016/03/09] New plug-in 'nonterm' for detection of definite
non-termination based on Value.
!o Kernel [2016/02/29] Do not raise Invalid_arg and Failure exn but use
custom exceptions instead. Prevents warning 52 in OCaml 4.03.0
Functions raising new exceptions are:
- Db.From.find_deps_term_no_transitivity_state
- Db.Interp.*
- Kernel [2016/02/24] New option -<plugin>-log to copy the output of
plug-ins into one or several text files
(described in the User Manual).
-* ACSL [2016/02/23] Fixes implicit logic label generation on recursive
definitions. Fixes bug #2158.
- Eva [2016/02/22] Experimental domain dedicated to storing and
learning information from syntactic equalities
(option -eva-equality-domain).
- Eva [2016/02/22] Improvements to backward propagation, on memory
accsses and bitwise operations.
-* Value [2016/02/17] Fix handling of functions without a body that
return a pointer. The pointer was aligned on an incorrect
frontier.
-* Value [2016/02/17] Fix crashes when analysing a function (without a
body) that returns an empty struct, or a pointer to an empty
struct. Bugs reported by TrustInSoft.
- Kernel [2016/02/10] Registering twice the same machdep is now accepted.
- Cil [2016/02/10] Add proper support for empty aggregate initializers
in GCC mode.
- Cil [2016/02/08] Operator ! applied to constant expression is no
longer simplified when not required.
- Value [2016/02/05] Informative messages about inactive behaviors are
now emitted only at verbosity level 2.
- Value [2016/02/05] Messages on ACSL predicates with Unknown/Invalid
status are now emitted with a 'warning' severity, consistently
with the emission of alarms. 'True' statuses are hidden if option
-val-show-progress is unset.
- From [2016/02/03] Option -from-verify-assigns takes into account
direct and indirect dependencies.
- Value [2016/02/03] Distinguish direct and indirect dependencies in
'from' clauses to compute the effecst of an 'assigns/from' clause.
See section 7.2 of the manual.
-* Libc [2016/02/02] Fix specifications of memchr and strncpy.
-* ACSL [2016/01/27] Fixes example of logic label use. Fixes bug #2203.
-* Logic [2016/01/17] Meaningless assigns clauses are now rejected more
aggressively. Fixes bug #1790.
o Kernel [2016/01/08] Several incompatible changes in module Property.
- Kernel [2016/01/08] Automatic generation of assigns from GCC's extended
asm.
-* Value [2016/01/06] Evaluation of ACSL ranges takes into account option
-safe-arrays. In particular t[..] remains within the bounds
of t. Fixes bug #!1639.
-* Value [2016/01/05] Take into account 'volatile' qualifiers on struct
typedefs, which were previously ignored. Fixes issue #@102.
- Value [2016/01/03] Support for \valid_function predicate during
evaluation.
- ACSL [2016/01/03] New predicate \valid_function, requiring the
compatibility between the type of the pointer and the function
being pointed.
-* Eva [2016/01/01] Fixed some bugs related to 0. vs. -0. in conditions.
- Eva [2016/01/01] More aggressive reductions in complex conditions
such as if(a+3 < 10).
-*! Value [2016/01/01] Reimplementation of all the upper layers of the
plugin. Compatibility with the legacy version is almost complete,
save for some text messages and a few functions of the API.
Use option -no-eva to switch back to the legacy version.
Changelog entries labelled 'Eva' refer to this new version.
Entries labelled 'Value' apply to both versions.
o! Value [2015/12/02] Base.base_max_offset has been removed. Part of its
functionality is still available via Base.valid_range, whose
return type is now more expressive.
-* RTE [2015/12/09] Fix unsoundness for overflows on binary operations
when one or two operands were constant.
-* RTE [2015/12/09] Fix unsoundness on unary minus expressions when
option -rte-trivial-annotations is active.
-! Cil [2015/12/02] Changes in the handling of incomplete structs and
zero-length arrays. Initialization of incomplete (completely
undefined) structs is now duly rejected. Several compiler
extensions to the C99 standard (empty initializers,
zero-length arrays, etc.) now require a GCC or MSVC machdep
(e.g. -machdep gcc_x86_32).
-! Cil [2015/12/02] Better handling of C99 flexible array members (FAMs).
Static initialization of FAMs (a GCC extension) is no longer
supported.
o! Gui [2015/12/01] Refactor GUI Helpers.
(Toolbox and (partially) Gtk_helper moved
to Wutil,Widget, Wform, Wtext and Wtable).
-! Value [2015/11/26] Widening hints now includes signed and unsigned
limits for the bitsize of the value being widened, but does not
include arbitrary limits anymore. The convergence is generally
faster but results may be more or less precises depending on
the case.
-! Value [2015/11/26] Better propagation strategy for nested loops.
Results are usually much more predictable (and often more
precise) when the loops are not fully unrolled by slevel.
-! Makefile [2015/11/26] Target 'make rebuild' has been renamed into
'make clean-rebuild'.
-* Value [2015/11/24] The preconditions of functions overridden by builtins
no longer receive an 'Unreachable status for calls within dead
code: the specification is ignored everywhere. Fixes bug #!1956.
-! Cil [2015/11/23] Incorrect return statements (return void on non-void
functions and vice-versa) now generate errors instead of warnings.
- Value [2015/11/23] New option -val-warn-undefined-pointer-comparison.
- ACSL [2015/11/23] Add built-in operators for lists.
- ACSL [2015/11/23] Add notation '{ x, y, z }' for defining sets.
o Makefile [2015/11/19] New option PLUGIN_EXTRA_DIRS for multi-dir plugins.
-* Kernel [2015/11/18] do not crash when loading statuses depending from
non existing parameter. Fixes issue #!2181.
o! Makefile [2015/11/12] Get rid of FRAMAC_MAKE variable. Use FRAMAC_INTERNAL
instead for distinguishing internal and external mode.
- Kernel [2015/10/28] Option -collect-messages is obsolete and will be
removed in a future version; messages are now always collected.
o! Kernel [2015/10/19] Removed function State_selection.list_state_union.
Use State_selection.of_list or State_selection.list_union instead.
-* Kernel [2015/10/15] Avoid comment duplications on generated code.
-* Kernel [2015/10/15] Comments are preserved even when loops are unrolled.
Fixes issue #!2176.
-! Kernel [2015/10/15] Option -warn-undeclared-callee changed to
-implicit-function-declaration, which receives an argument
(ignore, warn or error) specifying what to do when an undeclared
function is called.
-! GUI [2015/10/15] Signature change for function
Design.register_source_highlighter; the first argument of the
callback has now type Design.reactive_buffer, which can be coerced
back to a GSourceView2.source_buffer using method buffer.
- Value [2015/10/13] During the evaluation of ACSL 'assert', intermediate
statuses (e.g. True, then Unknown, then True) are now reported
in the console.
o! Kernel [2015/12/09] API change for function Alarms.register. See .mli
for details.
- Cil [2015/10/09] Add support for parsing digraphs.
o! Cil [2015/10/09] Buggy record Cil.miscState has been removed.
Customization must be done directly in Cil_printer.state.
- Value [2015/09/30] Better precision for calls through function pointers
when multiple functions are possible. The abstract state now
contains the information of which function was called.
o! Value [2015/09/20] Functions filter_le_ge_lt_gt_* have been renamed
into backward_comp_*. Evaluation and reduction functions
for comparisons now use and return dedicated types, in
Abstract_interp.Comp.
- Cil [2015/09/20] Double pointer casts on the NULL pointer are now
simplified.
-! Cil [2015/09/20] Typing within comparisons is now more strict,
or made more explicit through casts.
- Kernel [2015/09/20] The untyped AST is no longer removed by basic program
transformations such as loop unrolling.
o Ptests [2015/07/29] New EXEC: directive.
- Kernel [2015/07/01] New options -then-last and -then-replace.
- Kernel [2015/07/01] New option -remove-projects.
- Kernel [2015/06/30] New option -set-project-as-default.
######################################
Open Source Release Magnesium-20151002
######################################
o! Kernel [2016/01/03] Modules Dataflow is deprecated, and will be removed
in Aluminium. Module Dataflow2 offers a very similar but simpler
API.
- Doc [2015/11/16] Fixed typo in the manual (Thx Mihaela Sighireanu).
-* Kernel [2015/10/12] Fix clearing of old statuses and hypotheses when a
new status is emitted or an annotation is removed.
-* Libc [2015/09/29] Removed obsolete file machine.h (along with other
similar files) from the Frama-C share folder. Fixes bug #2171
-! Kernel [2015/09/07] Removed support for OCaml 3.12.1
- Value [2015/09/03] Assertions containing \at(P, L), where L is a C
label, can now be evaluated. Evaluation is done once Value has
run; thus, it ignores option -slevel.
-* Value [2015/09/03] pointer_comparable alarms are now emitted with
arguments properly cast to void* or void (*)().
- Value [2015/08/10] The alarms raised when evaluating a global
initializer that leads to an undefined behavior are now marked
with an "Invalid" status.
- Report [2015/08/10] Reports in csv format now honor option
-report-specialized (previously, preconditions at a
callsite were always skipped).
-* Libc [2015/08/26] Fix bug in the specifications of readir, opendir,
closedir and fopen functions, that would cause incorrect analysis
in -lib-entry-mode.
- Gui [2015/08/14] When a call statement is selected, the statuses of
the preconditions of the called functions are displayed in the
'information' panel.
o! Gui [2015/08/14] Minor API changes regarding Design.reactive_buffer.
Some values that used to have an option type are now guaranteed
to be present.
- Gui [2015/08/12] Internal ids (for statements, code annotations, etc.)
are now hidden by default. Start the GUI in debug mode if you want
to see them.
-* Gui [2015/08/10] Filenames in the GUI file tree (top-left panel)
are now sorted correctly. Fixes bug #2173.
-! Value [2015/08/03] WIDEN_HINTS directive are now cumulative with
automatically inferred bounds. Fixes bug #876.
-* Cil [2015/08/03] Fix bug #1553, related to nested initialisations
of structures containing pointers.
-! Value [2015/08/03] All plugins that depend on Value, plus Value itself
are now dynamic. Custom plugins must specify in their Makefile the
plugins they depend on (e.g. PLUGIN_DEPENDENCIES:=Inout Value).
-* Cil [2015/07/29] Cil transformation can introduce assertion to ensure
that size expressions in an array declarations evaluated at
program execution time are positive and do not overflow.
o Ptests [2015/07/29] New LOG: directive.
- Value [2015/07/19] Garbled mix origins now include at most one source
location.
- Report [2015/07/19] New option -report-proven to control the display
of proven properties.
- Report [2015/07/19] New export format (.csv), through option -report-csv.
o! Callgraph [2015/07/16] Remove Cil.Callgraph, Db.Syntactic_callgraph and
Db.Semantic_callgraph which are all replaced by the single
plug-in Callgraph. See Changelog_detailled.md for further detail
about this change.
-! Callgraph [2015/07/16] New plug-in callgraph which merges the old
Syntactic_callgraph and Semantic_callgraph plug-ins (now
removed). Either this plug-in uses Value if already computed, or
computes the syntactic callgraph otherwise. This new plug-in