- Feb 07, 2020
-
-
David Bühler authored
Without using exceptions.
-
David Bühler authored
Avoids catching the exception in each case of the pattern matching, and simplifies the implementation.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
- Feb 05, 2020
-
-
David Bühler authored
- renames [eval_tlval] into [eval_term_as_lval], as it evaluates a term. - renames [eval_thost_toffset] into [eval_tlval], as it evaluates a term_lval, and uses it instead of the previous [eval_tlval] when evaluating a term_lval.
-
- Jan 30, 2020
-
-
David Bühler authored
-
- Jan 13, 2020
-
-
David Bühler authored
Exports 4 new functions in ival: - is_int and is_float - is_small_set and project_small_set
-
- Sep 27, 2019
-
-
- Sep 02, 2019
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
No need to declare known constants in [known_logic_funs], as they are direclty handled in [eval_terms] and not by [eval_known_logic_function].
-
David Bühler authored
-
David Bühler authored
In eval_terms, uses the forward comparison with positive and negative infinity to replace these functions.
-
David Bühler authored
These backward propagators takes a boolean argument [positive] that indicates whether the value to be reduced is finite (respectively NaN) or not. [backward_is_nan] replaces the two previous functions [backward_is_nan] and [backward_is_not_nan]. Implements the backward propagation [is_finite ~positive:false] that corresponds to !\is_finite(f).
-
François Bobot authored
Add \plus_infinity, \minus_infinity, \NaN Support in EVA
-
- Aug 20, 2019
-
-
David Bühler authored
-
- Jul 08, 2019
-
-
David Bühler authored
These operators are eq_float, ne_float, lt_float, le_float, gt_float, gt_float. And respectively for the double type. Required to compare infinite and NaN which do not exist in the real type.
-
David Bühler authored
-
David Bühler authored
As we want to use the latter in the former.
-
- Jun 28, 2019
-
-
- Apr 25, 2019
-
-
Virgile Prevosto authored
-
- Apr 24, 2019
-
-
David Bühler authored
-
David Bühler authored
The function Cvalue.V.cast_int_to_int is unsound here, as conversions to the _Bool type obey a different rule. This case never happens in the C AST, as conversions (_Bool)x are translated into (_Bool)(x != 0).
-
David Bühler authored
-
- Mar 28, 2019
-
-
David Bühler authored
- shares and moves the functions [reduce_offset_by_validity] of Locations and Precise_locs into base.ml. - replaces the boolean argument ~for_writing into the new type access, that represents Read, Write or No_access. Without any access, offsets must point into or just beyond the base validity. - fixes the support of accesses of size 0: they are now invalid: + in bases with Invalid validity; + one past a base validity unless the base ends with an empty struct.
-
- Feb 19, 2019
-
-
- Feb 05, 2019
-
-
Loïc Correnson authored
-
- Jan 21, 2019
-
-
Loïc Correnson authored
(blind make headers from specifications)
-
- Jan 14, 2019
-
-
Loïc Correnson authored
-
- Dec 12, 2018
-
-
Andre Maroneze authored
-
- Dec 04, 2018
-
-
Andre Maroneze authored
-
- Dec 03, 2018
-
-
Valentin Perrelle authored
- Fix Value/Value#5 - Fix Value/Value#14
-
- Nov 28, 2018
-
-
David Bühler authored
-
Andre Maroneze authored
Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
-