[MC] Add a separate type inference pass
Inria Forge bug #17110: https://gforge.inria.fr/tracker/index.php?func=detail&aid=17110&group_id=12&atid=165
From: Gabriel Corona
Date: 17/03/2014 14:34
We would like to have the inferred type of the different memory regions before starting the state compaison. For this, we would have to add a phase of type inference before the state comparison phase.
In fact, instead of infering the types for all state pairs we could do it for each state and reduce the complexity of this part from n^2 to n where n number of visited states.
We might want to use this to handle more correctly advanced cases such as :
- subtyping (p is a cat and p is a vehicle -> p is car) ;
- "has a" relation (p is a car and p is a wheel -> p is a car) with [1] ;
- handle conflicting inferred types (and infer dangling pointers ?).
[1]
struct car {
wheel wheels[4];
// ...
}