WP output of loop variant's goal doesn't have location of loop variant

ID0002190: This issue was created automatically from Mantis Issue 2190. Further discussion may take place here.

Id	Project	Category	View	Due Date	Updated
ID0002190	Frama-C	Plug-in > wp	public	2015-12-03	2016-01-26


Reporter	gaggarwal	Assigned To	correnson	Resolution	won't fix
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Sodium	Target Version	-	Fixed in Version	-

Description :

Consider the following example:

void main() {
```
int i;
```
```
/*@ loop invariant 0 <= i <= 5;
```
```
  @ loop variant 5-i;
```
```
  @*/
```
```
for(i=0;i<5;i++);
```
}

Output generated by wp for loop variant is following:

Goal Decreasing of Loop variant at loop (file /SpecDemo/src/test6.c, line 6): Assume { (* Domain *)
...... Prove: true. Prover Qed returns Valid

Goal Positivity of Loop variant at loop (file /SpecDemo/src/test6.c, line 6): Assume { (* Domain *) ....... Prove: true. Prover Qed returns Valid

Notice that both goals have location of loop i.e. (file /SpecDemo/src/test6.c, line 6) and not of loop variant. Even though a loop can have only one loop variant and it is not very hard to figure out which loop variant it is, it will be really helpful if we can include location of loop variant too.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information