Skip to content
Snippets Groups Projects
  • David Bühler's avatar
    d80e4a34
    [Eva] Emits indeterminate alarms on call arguments to builtins. · d80e4a34
    David Bühler authored
    'Indeterminate' alarms are alarms about uninitialized memory, escaping pointers
    and special floating-point values (infinite and NaN).
    
    These alarms are emitted for functions specified by -eva-warn-copy-indeterminate
    option, which is @all by default. These alarms can be disabled for some function
    by -eva-warn-copy-indeterminate=-f, in which case they are also disabled for
    the argument expressions of calls to [f].
    
    However:
    - the @all default value did not include functions without definition
      (for which a specification or a builtin is used).
    - 'indeterminate' alarms were emitted anyway for the arguments of calls to
      functions without definition, except for builtins.
    So no indeterminate alarms were emitted for the argument expressions of calls
    to builtins (unless their definitions were included).
    
    This commit fixes this behavior:
    the @all default of -eva-warn-copy-indeterminate option include all functions
    and special case for functions without definition or builtins are removed.
    
    It still avoids to emit surch alarms on Eva directives such as Frama_C_show_each.
    d80e4a34
    History
    [Eva] Emits indeterminate alarms on call arguments to builtins.
    David Bühler authored
    'Indeterminate' alarms are alarms about uninitialized memory, escaping pointers
    and special floating-point values (infinite and NaN).
    
    These alarms are emitted for functions specified by -eva-warn-copy-indeterminate
    option, which is @all by default. These alarms can be disabled for some function
    by -eva-warn-copy-indeterminate=-f, in which case they are also disabled for
    the argument expressions of calls to [f].
    
    However:
    - the @all default value did not include functions without definition
      (for which a specification or a builtin is used).
    - 'indeterminate' alarms were emitted anyway for the arguments of calls to
      functions without definition, except for builtins.
    So no indeterminate alarms were emitted for the argument expressions of calls
    to builtins (unless their definitions were included).
    
    This commit fixes this behavior:
    the @all default of -eva-warn-copy-indeterminate option include all functions
    and special case for functions without definition or builtins are removed.
    
    It still avoids to emit surch alarms on Eva directives such as Frama_C_show_each.