[Eva] Backward propagates reduction of builtins arguments.
During the interpretation of a function call, the possible values of formal parameters can be reduced — especially by the evaluation of the function preconditions. At the end of a function call, Eva backward propagates these reductions to the concrete arguments of the call. This commit also does this backward-propagation when a builtin is used to interpret the call. Also removes unused [builtin] field from call results (it was only used to avoid the backward propagation of argument reductions when a builtin was used).
Showing
- src/plugins/eva/engine/compute_functions.ml 4 additions, 5 deletionssrc/plugins/eva/engine/compute_functions.ml
- src/plugins/eva/engine/transfer_stmt.ml 2 additions, 11 deletionssrc/plugins/eva/engine/transfer_stmt.ml
- src/plugins/eva/engine/transfer_stmt.mli 0 additions, 1 deletionsrc/plugins/eva/engine/transfer_stmt.mli
Loading
Please register or sign in to comment