facebook / facebook/infer

Warning if modelled methods are called with null argument

Open
#191 1 comment 0 reactions 1 assignee Claimed by @jeremydubreil View on GitHub
question stale
Dominant language
OCaml
Stars
15.7k
Forks
2.1k
Avg merge
19h 36m
Merged PRs (30d)
13

Description

I have a question relating to modelling. I would like to model an api in order to check with infer that it is used correctly, i.e., that certain methods are called with non-null parameters. This seems to be done for java.lang.System.getProperty(String s) by de-referencing the parameter s by calling s.length() in the model of the method.

Below is a simple model of ArrayList (the purpose of the model is just to illustrate the problem). It uses the approach above for the add-method, but it doesn’t work. When running in debug mode, I get “SKIP_FUNCTION boolean ArrayList.add(Object)” in the generated html-file. However, the call to iterator() is not skipped and works correctly according to the model.

```Java
public abstract class ArrayList {

int size = 0;

public boolean add(T x){
Class c = x.getClass();
size = InferUndefined.int_undefined();
InferBuiltins.assume(size>0);
return true;
}

public java.util.Iterator iterator(){
Object val = InferUndefined.object_undefined();
//return (java.util.Iterator)val;
return null;
}

}
```

Do you have any advice for debugging this issue further? Is the model that I have even sufficient for infer to find the method add, since I have omitted the inherited classes and implemented interfaces (it doesn’t seem to make a difference)?

I’m using infer git-a7a332ea5147a2beb045dc6e996d951a3ccc0055 on Mac OSX Yosemite with Java 7

Thanks in advance

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.