Package org.sosy_lab.common.configuration

Annotation Type 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:
    Configuration

    • 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 Detail

      • 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:
        {}