Package org.sosy_lab.common.configuration

Annotation Interface Option

@Documented @Retention(RUNTIME) @Target({FIELD,METHOD}) public @interface Option
An annotation to mark fields or methods which should get configuration values injected. Such a field or method must be contained in a class annotated with Options.

While it is possible to mark final fields with this annotation, the java documentation says that the behavior of setting final fields will be undetermined. It might happen that some parts of the code do not see the new value.

It is possible to mark private fields with this annotation, all access modifiers will be ignored when setting the value.

If a method is marked with this annotation, it has to have exactly one parameter. An result value would be ignored, so the method should by of type void. If the method throws an IllegalArgumentException, the configuration will be rejected as invalid. If the method throws any other exception, the behavior is undefined (so it should not throw any other exception!).

If an option is not present in the configuration file, the corresponding field is not touched. Similarly, a corresponding method is not called.

It is possible to specify one option more than once, both for fields and methods. All of the fields will be set and all of the methods will be called.

See Also:

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String
    description
    A text that describes the current option (this will be part of the user documentation).

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    String
    deprecatedName
    When the option needs to be renamed, often it is desirable to maintain the backwards compatibility with the previous config.
    String
    name
    An optional name for the option as it appears in the configuration file.
    String
    regexp
    If regexp is specified, the value of this option (prior to conversion to the correct type) will be checked against this regular expression.
    boolean
    required
    An optional flag if this option needs to be specified in the configuration file.
    boolean
    secure
    An optional flag that this configuration option is secure, i.e., setting it to an arbitrary attacker-controlled value may not allow any harm (like abitrary code execution).
    boolean
    toUppercase
    An optional flag that specifies if a configuration value should be converted to upper case after it was read.
    String[]
    values
    If values is non-empty, the value of this option (prior to conversion to the correct type) will be checked if it is listed in this array.

  • Element Details

    • description

      String description
      A text that describes the current option (this will be part of the user documentation).

    • name

      String name
      An optional name for the option as it appears in the configuration file. If not specified, the name of the field will be used. In both cases it will be prefixed with the prefix specified in the Options annotation (if given).
      Default:
      ""

    • deprecatedName

      String deprecatedName
      When the option needs to be renamed, often it is desirable to maintain the backwards compatibility with the previous config. In that case, the previous name can be moved to the field deprecatedName. Both normal and deprecated name would work, with latter printing the deprecation warning.

      Note that this field only works if the Options annotations on the class defines a Options.deprecatedPrefix() and only with that deprecated prefix. The combination of the current prefix and the deprecated option name will not work.

      Furthermore, if a deprecated option name is defined, only the combinations "current prefix + current option name" and "deprecated prefix + deprecated option name" will work.

      Summary what works if Options.deprecatedPrefix() is set:

      • If deprecated option name is set, then "current prefix + current option name" and "deprecated prefix + deprecated option name" work.
      • If deprecated option name is not set, then "current prefix + current option name" and "deprecated prefix + current option name" work.
      Default:
      ""

    • secure

      boolean secure
      An optional flag that this configuration option is secure, i.e., setting it to an arbitrary attacker-controlled value may not allow any harm (like abitrary code execution).
      Default:
      false

    • required

      boolean required
      An optional flag if this option needs to be specified in the configuration file. The default is false. If set to true, an exception will be thrown if the option is not in the file.
      Default:
      false

    • toUppercase

      boolean toUppercase
      An optional flag that specifies if a configuration value should be converted to upper case after it was read. For options with enum types, this flag is always assumed to be true.
      Default:
      false

    • regexp

      String regexp
      If regexp is specified, the value of this option (prior to conversion to the correct type) will be checked against this regular expression. If it does not match, an exception will be thrown.
      Default:
      ""

    • values

      String[] values
      If values is non-empty, the value of this option (prior to conversion to the correct type) will be checked if it is listed in this array. If it is not contained, an exception will be thrown.
      Default:
      {}