• Virgile Prevosto's avatar
    [kernel] add support in the AST to identify check-and-forget annotations · 3486b24d
    Virgile Prevosto authored
    this is a generalization of `check` vs. `assert` to other annotations. Not all
    annotations are relevant though. Currently, there are more annotation nodes in
    the AST that can have a flag `{ tp_only_check }` than was deemed useful in
    pub/frama-c#25, but said flag can in fact safely be ignored. Moreover, this
    commit only add this flag in the AST, but provides no further mean to set it to
    true except for the original `check` keyword (i.e. on `AAssert`). The parser
    and the behavior of the plugins that can handle the flag will be updated in
    subsequent commits
    3486b24d
cil_datatype.mli 11.7 KB