- Plugins fields in the AST are used to find the right extension
- A plugin still cannot register twice an extension
- If plugin is not given, can throw ambiguity error
- Kernel extensions are an exception, a plugin cannot register an
extension with the name name than the kernel

- Cil_types.acsl_extension
- Logic_ptree.extension & global_extension

Thibault Martin authored 1 year ago and Allan Blanchard committed 1 year ago

Use "\plugin::ext" instead of "ext"
  - allows for better warning messages
  - Ignored if plugin is not loaded / ext is not registered
  - raise an error if ext comes from a different plugin

- full_identifier accepts non-c keywords (list to be completed)
- logic_type rule is parameterized by the kind of typenames we accept
  (either only typenames or typenames + identifiers for rt_type
- on the other hand, logic_attributes cannot have the same name as
  an ACSL keyword.

Fixes #2638