--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2011 ---
>> new->size = (int)next - (int)new - BLOCK_SIZE; > This is something that the value analysis handles perfectly, as you > can check on a small example, when next and new are in the same block. > It cannot handle it (because there is no good answer) when it has not > been able to determine that next and new point inside the same block. Actually, it occurs to me that we could emit an alarm stating that next and new *must* be in the same block for the subtraction to make sense, and then evaluate the result as the set of values that can be obtained under this condition. This would save user time for this example, but only if the program never subtracts two pointers to different blocks on purpose. If the program did this on purpose, this would make it impossible to analyze. Pascal