facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.83k stars 2k forks source link

[RacerD] Detecting races in objects contained in a Map #1701

Open manebarros opened 1 year ago

manebarros commented 1 year ago

Please include the following information:

I've been experimenting with RacerD with a simple Bank class, that stores Accounts in a Map. In this simple version, it fails to detect data races that might occur in concurrent accesses to the same account. Is this expected behaviour?

@ThreadSafe
public class Bank {
    private Map<Integer, Account> accounts;

    public class Account {
        int balance;

        public Account(int balance) {
            this.balance = balance;
        }

        public int balance() {
            return this.balance;
        }

        public void deposit(int quant) {
            balance += quant;
        }

        public boolean withdraw(int quant) {
            if (quant > balance)
                return false;
            balance -= quant;
            return true;
        }
    }

    public Bank(int n) {
        accounts = new HashMap<>();
        for (int i = 0; i < n; i++)
            accounts.put(i, new Account(0));
    }

    public int balance(int acc) {
        return this.accounts.get(acc).balance();
    }

    public void deposit(int acc, int quant) {
        this.accounts.get(acc).deposit(quant);
    }

    public boolean withdraw(int acc, int quant) {
        return this.accounts.get(acc).withdraw(quant);
    }
}