Skip to content
Snippets Groups Projects
  • David Bühler's avatar
    b62c4e33
    [Inout] Records Inout results on all function calls for Eva. · b62c4e33
    David Bühler authored
    Eva relies on the inout plugin to ensure that a function call has not modified
    the values of its concrete arguments, meaning that at the end of the call, the
    values of formal parameters can be backward propagated to the corresponding
    concrete arguments. This is useful when the values of some parameters have been
    reduced by the call, for instance by some preconditions.
    
    To this end, Eva uses the Inout callback Record_Inout_Callbacks from Db, but
    this callback was only applied by Inout for functions whose body is analyzed.
    
    This commit modifies Inout to also record its result through this callback
    on functions interpreted by a builtin or a specification, thus allowing a
    precise backward propagation of the values of formal parameters to concrete
    arguments in all cases.
    b62c4e33
    History
    [Inout] Records Inout results on all function calls for Eva.
    David Bühler authored
    Eva relies on the inout plugin to ensure that a function call has not modified
    the values of its concrete arguments, meaning that at the end of the call, the
    values of formal parameters can be backward propagated to the corresponding
    concrete arguments. This is useful when the values of some parameters have been
    reduced by the call, for instance by some preconditions.
    
    To this end, Eva uses the Inout callback Record_Inout_Callbacks from Db, but
    this callback was only applied by Inout for functions whose body is analyzed.
    
    This commit modifies Inout to also record its result through this callback
    on functions interpreted by a builtin or a specification, thus allowing a
    precise backward propagation of the values of formal parameters to concrete
    arguments in all cases.