Merge branch 'feature/bdesloges/eva/error-for-assigns-nothing' into 'master'
[Eva] Warning message for missing assigns or from are now an error by default See merge request frama-c/frama-c!4883
Showing
- Changelog 5 additions, 0 deletionsChangelog
- src/libraries/utils/pretty_utils.ml 0 additions, 9 deletionssrc/libraries/utils/pretty_utils.ml
- src/libraries/utils/pretty_utils.mli 0 additions, 3 deletionssrc/libraries/utils/pretty_utils.mli
- src/plugins/aorai/tests/ya/floats.i 1 addition, 1 deletionsrc/plugins/aorai/tests/ya/floats.i
- src/plugins/aorai/tests/ya/oracle/floats.res.oracle 4 additions, 3 deletionssrc/plugins/aorai/tests/ya/oracle/floats.res.oracle
- src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle 4 additions, 3 deletionssrc/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
- src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle 2 additions, 2 deletionssrc/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
- src/plugins/eva/engine/compute_functions.ml 10 additions, 7 deletionssrc/plugins/eva/engine/compute_functions.ml
- src/plugins/eva/engine/recursion.ml 4 additions, 4 deletionssrc/plugins/eva/engine/recursion.ml
- src/plugins/eva/engine/transfer_specification.ml 20 additions, 8 deletionssrc/plugins/eva/engine/transfer_specification.ml
- src/plugins/eva/self.ml 4 additions, 1 deletionsrc/plugins/eva/self.ml
- src/plugins/eva/self.mli 2 additions, 0 deletionssrc/plugins/eva/self.mli
- src/plugins/variadic/tests/known/oracle/exec.res.oracle 1 addition, 1 deletionsrc/plugins/variadic/tests/known/oracle/exec.res.oracle
- src/plugins/variadic/tests/known/oracle/ioctl.res.oracle 1 addition, 1 deletionsrc/plugins/variadic/tests/known/oracle/ioctl.res.oracle
- src/plugins/variadic/tests/known/oracle/printf.res.oracle 1 addition, 1 deletionsrc/plugins/variadic/tests/known/oracle/printf.res.oracle
- tests/builtins/oracle/from_result.res.oracle 1 addition, 1 deletiontests/builtins/oracle/from_result.res.oracle
- tests/builtins/oracle/imprecise.res.oracle 1 addition, 1 deletiontests/builtins/oracle/imprecise.res.oracle
- tests/fc_script/make-wrapper.t/run.t 4 additions, 6 deletionstests/fc_script/make-wrapper.t/run.t
- tests/float/oracle/logic.0.res.oracle 1 addition, 1 deletiontests/float/oracle/logic.0.res.oracle
- tests/float/oracle/logic.1.res.oracle 1 addition, 1 deletiontests/float/oracle/logic.1.res.oracle
Loading
Please register or sign in to comment