Check for function formal argument with frama_c_init_obj attribute.
- 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).
Showing
- src/kernel_internals/typing/cabs2cil.ml 10 additions, 1 deletionsrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_services/ast_queries/cil.ml 25 additions, 10 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/cil.mli 4 additions, 0 deletionssrc/kernel_services/ast_queries/cil.mli
- tests/syntax/const-assignments.c 18 additions, 1 deletiontests/syntax/const-assignments.c
- tests/syntax/oracle/const-assignments.0.res.oracle 20 additions, 2 deletionstests/syntax/oracle/const-assignments.0.res.oracle
- tests/syntax/oracle/const-assignments.7.res.oracle 20 additions, 2 deletionstests/syntax/oracle/const-assignments.7.res.oracle
- tests/syntax/oracle/const-assignments.8.res.oracle 20 additions, 2 deletionstests/syntax/oracle/const-assignments.8.res.oracle
- tests/syntax/oracle/const-assignments.9.res.oracle 3 additions, 1 deletiontests/syntax/oracle/const-assignments.9.res.oracle
Loading
Please register or sign in to comment