-
David Bühler authored
- [cacheable] is given at the registration of a builtin, and not separately for each result of the builtin. - Removes the offsetmap for the arguments: no builtin were using it anyway. - Returns a Cvalue.V.t for the result instead of an offsetmap. - Builtins can also return: + only the value of the result, in which case the post-state from the interpretation of the specification is used with the resulting value computed by the builtin. + only the post-states for functions with no froms dependency (other than the result and arguments) and no write of local variable addresses. Simplifies some builtins accordingly.
David Bühler authored- [cacheable] is given at the registration of a builtin, and not separately for each result of the builtin. - Removes the offsetmap for the arguments: no builtin were using it anyway. - Returns a Cvalue.V.t for the result instead of an offsetmap. - Builtins can also return: + only the value of the result, in which case the post-state from the interpretation of the specification is used with the resulting value computed by the builtin. + only the post-states for functions with no froms dependency (other than the result and arguments) and no write of local variable addresses. Simplifies some builtins accordingly.