Warning if modelled methods are called with null argument
- 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
Assessment
This issue has not been assessed yet.