FormatMethod: how to forward their arguments to another format method?

Question

I don't understand why I get an error related to @FormatMethod.

Here's a very simple example, that fails:

import org.checkerframework.checker.formatter.qual.FormatMethod;
import java.util.Locale;

public class FormatExample {

    public void example() {
        String ex1 = String.format(Locale.ENGLISH, "%s %d", "cost", 12);
        log("%d", 0);
    }

    @FormatMethod
    static void log(String format, Object... args) {
        String ex1 = String.format(Locale.ENGLISH, format, args);
        // The line above causes the error (see below)
    }
}

It fails with the following error-message:

FormatExample.java:13: error: 
    [format.string.invalid] invalid format string (is a @Format annotation missing?)
                String ex1 = String.format(Locale.ENGLISH, format, args);

What am I missing?
I am using version: javac 1.8.0-jsr308-2.1.14

What I try to do is very similar to the example in the docs: 10.5 @FormatMethod:

Your project may contain methods that forward their arguments to a format method. Consider for example the following log method:

@FormatMethod
void log(String format, Object... args) {
    if (enabled) {
        logfile.print(indent_str);
        logfile.printf(format , args);
    }
}

You should annotate such a method with the @FormatMethod annotation. This instructs the Format String Checker to check every invocation of the method. This check is analogous to the check done on every invocation of built-in format methods like String.format.

Hint:
you can easily reproduce the issue in the Checker Framework Live Demo.

• don't forget to change Choose a type system: to Format String Checker
• keep in mind that the online-tool uses an older version of the Checker Framework (2.1.10 @ 08.09.2017)

Answer 1

The @FormatMethod annotation was working as documented, but not as you wanted -- and your interpretation was a reasonable one.

The manual and the @FormatMethod documentation say that @FormatMethod causes calls to the annotated method to be checked, but they make no promises about calls within the annotated method.

However, this bug has been recently fixed. You can build the Checker Framework from source or wait for the next release.