Merge branch 'feature/eva/arccos-arcsin' into 'master'
[Eva] New builtins for trigonometric functions acos, asin and atan See merge request frama-c/frama-c!2678
Showing
- share/libc/math.h 13 additions, 60 deletionsshare/libc/math.h
- src/kernel_services/abstract_interp/fc_float.ml 3 additions, 0 deletionssrc/kernel_services/abstract_interp/fc_float.ml
- src/kernel_services/abstract_interp/float_interval.ml 26 additions, 0 deletionssrc/kernel_services/abstract_interp/float_interval.ml
- src/kernel_services/abstract_interp/float_interval_sig.mli 3 additions, 0 deletionssrc/kernel_services/abstract_interp/float_interval_sig.mli
- src/kernel_services/abstract_interp/float_sig.mli 3 additions, 0 deletionssrc/kernel_services/abstract_interp/float_sig.mli
- src/libraries/utils/c_bindings.c 30 additions, 20 deletionssrc/libraries/utils/c_bindings.c
- src/libraries/utils/floating_point.ml 3 additions, 0 deletionssrc/libraries/utils/floating_point.ml
- src/libraries/utils/floating_point.mli 3 additions, 0 deletionssrc/libraries/utils/floating_point.mli
- src/plugins/report/tests/report/oracle/csv.csv 1 addition, 1 deletionsrc/plugins/report/tests/report/oracle/csv.csv
- src/plugins/value/domains/cvalue/builtins_float.ml 6 additions, 0 deletionssrc/plugins/value/domains/cvalue/builtins_float.ml
- tests/float/math_builtins.c 73 additions, 0 deletionstests/float/math_builtins.c
- tests/float/oracle/math_builtins.res.oracle 1255 additions, 964 deletionstests/float/oracle/math_builtins.res.oracle
- tests/idct/oracle/ieee_1180_1990.res.oracle 94 additions, 256 deletionstests/idct/oracle/ieee_1180_1990.res.oracle
- tests/libc/oracle/fc_libc.1.res.oracle 18 additions, 108 deletionstests/libc/oracle/fc_libc.1.res.oracle
- tests/libc/oracle/math_h.res.oracle 36 additions, 74 deletionstests/libc/oracle/math_h.res.oracle
Loading
Please register or sign in to comment