2021-03-02 03:27 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001588Frama-CPlug-in > wppublic2014-03-13 15:57
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001588: WP ignores some goal
DescriptionOn this example, WP ignore some of the goals. There should be 3 goals, but :

[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_loop_inv_l1_2_established : Valid

Loop invariant preservation and assertion are ignore.
Steps To Reproduceframa-c wp.c -wp
Additional InformationI simplified the example as much as possible, but it seems that the number of statements is important to reproduce the problem 8-/
TagsNo tags attached.
Attached Files
  • c file icon wp.c (259 bytes) 2013-12-20 18:27 -
    void f (int n, int *d ) {
      int i = 0, z = 0;
      //@ loop invariant l1_2: d == \at(d,Pre) + i;
      while (i < n)
        //@ assert a1: d == \at(d,Pre) + i; 
      while (z != 0) {
    c file icon wp.c (259 bytes) 2013-12-20 18:27 +

related to 0001601closedcorrenson WP Plugin with Alt-Ergo - unable to prove? 



correnson (manager)

Seems that both the number of ';' and the second loop are necessary to reproduce the test.
Workaround is:

frama-c -print wp.c -ocode wp2.c
frama-c -wp wp2.c

It seems that the internal CFG is broken into two pieces.
@Anne: as the primary author of Cil2Cfg, do you have any idea of how to fix the problem ?


correnson (manager)

Problem in Cil2Cfg


Anne (reporter)

I am not sure to understand what you mean by "broken into two pieces".
When I export the graph to dot, I don't see it broken...

The problem happens very often, and it would be great if I could find a simpler example !

Sorry, but I don't have much time to look at the problem now... :-(


correnson (manager)

Ok, not a problem.


Anne (reporter)

On an other example, it also happens that -ocode solve the problem.
I don't understand how the AST used by WP can be different
since wp2.c should precisely represent the internal form of the analyzed code. Could it be a problem in the internal representation ?

I also tested: frama-c -print wp2.c -ocode wp3.c
and confirm that wp2.c and wp3.c are the same.


Anne (reporter)

There is at least a problem with the management of empty blocks...
De-commenting the 3 lines that ignore empty blocks in Cil2cfg.cfg_block
solves many problems (but unfortunately not the example of this task...)

I guess there must be another reason why those lines where commented out...


yakobowski (manager)

@Anne: the change you refer to was introduced in commit 1486f9cea38012a595b505ee179f11fc98400974


Anne (reporter)

Thanks Boris: not sure why I did that, but I guess it was to have fewer "special cases"...


correnson (manager)

Remark: for debugging the internal Cil2Cfg representation and how it interfere with WP calculus, one may use the "Dump" memory model :

frama-c -wp foo.i -wp-model Dump -wp-out cfg

This outputs in cfg directory DOT and PDF files representing CFG of WP operations.


Anne (reporter)

@Loïc: thank you. Very useful !


Anne (reporter)

I found it ! But I am VERY surprised that this hasn't been detected before !

The modification in note:4412 was not a fix and worked purely by chance on my example. Forget it.

Now I am a bit embarrassed to have to explain the bug :-/ (so horrible !)

In Cil2cfg, nodes are identifier by a [node_id] composed of 2 integers (a, b) where 'a' is a number from 0 to 14, and 'b' is most of the time an sid.
Quite ugly, isn't it ?

Now, worse, VL.hash was computed as (a*17 + b) !!! (don't ask...)
so for instance node (2,3) was mixed up with node (1,20) !!!

I changed it to (b*100 + a), and every thing works better (of course).


correnson (manager)

Fix committed to master branch.


correnson (manager)

Great !
Many thanks to Anne for pointing to me the solution.
I have refactored a bit Cil2cfg nodes and edges identification during the process.
This solves many issues like this one.


correnson (manager)

Fix committed to feature/bug_1598 branch.


correnson (manager)

Fix committed to stable/neon branch.

-Issue History
Date Modified Username Field Change
2013-12-20 18:27 Anne New Issue
2013-12-20 18:27 Anne Status new => assigned
2013-12-20 18:27 Anne Assigned To => correnson
2013-12-20 18:27 Anne File Added: wp.c
2014-01-09 15:50 correnson Note Added: 0004393
2014-01-09 15:50 correnson Note Added: 0004394
2014-01-09 15:50 correnson Status assigned => confirmed
2014-01-09 16:32 Anne Note Added: 0004397
2014-01-13 10:25 correnson Note Added: 0004406
2014-01-16 10:58 Anne Note Added: 0004411
2014-01-16 11:04 Anne Note Added: 0004412
2014-01-16 12:17 yakobowski Note Added: 0004413
2014-01-16 12:29 Anne Note Added: 0004414
2014-01-16 12:46 correnson Note Added: 0004415
2014-01-16 12:53 Anne Note Added: 0004416
2014-01-16 14:19 Anne Note Added: 0004417
2014-01-16 16:02 correnson Relationship added related to 0001601
2014-01-16 16:10 correnson Source_changeset_attached => framac master bb43d1d9
2014-01-16 16:10 correnson Note Added: 0004418
2014-01-16 16:10 correnson Status confirmed => resolved
2014-01-16 16:10 correnson Resolution open => fixed
2014-01-16 16:14 correnson Note Added: 0004420
2014-02-04 19:07 correnson Source_changeset_attached => framac feature/bug_1598 7f7b24cb
2014-02-04 19:07 correnson Note Added: 0004485
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon bb43d1d9
2014-02-12 16:57 correnson Note Added: 0004542
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History