tests/syntax/oracle/const-assignments.7.res.oracle · ae7067eea7869563a3e596eeb88b2e63b14673c7 · pub / frama-c

2 years ago

Check for function formal argument with frama_c_init_obj attribute. · ae7067ee

Michele Alberti authored 2 years ago

- Extend checking to more than just left-values.
- Add function in Cil to check only for frama_c_init_obj attribute (as formals
  should not be annotated with frama_c_mutable one).

ae7067ee

History

Check for function formal argument with frama_c_init_obj attribute.

Michele Alberti authored 2 years ago

- Extend checking to more than just left-values.
- Add function in Cil to check only for frama_c_init_obj attribute (as formals
  should not be annotated with frama_c_mutable one).