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.