Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001588Frama-CPlug-in > wppublic2013-12-20 18:272014-03-13 15:57
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
PlatformOSOS Version
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 Filesc file icon wp.c [^] (259 bytes) 2013-12-20 18:27 [Show Content]

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

-  Notes
correnson (manager)
2014-01-09 15:50

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)
2014-01-09 15:50

Problem in Cil2Cfg
Anne (reporter)
2014-01-09 16:32

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)
2014-01-13 10:25

Ok, not a problem.
Anne (reporter)
2014-01-16 10:58

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)
2014-01-16 11:04

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)
2014-01-16 12:17

@Anne: the change you refer to was introduced in commit 1486f9cea38012a595b505ee179f11fc98400974
Anne (reporter)
2014-01-16 12:29

Thanks Boris: not sure why I did that, but I guess it was to have fewer "special cases"...
correnson (manager)
2014-01-16 12:46

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)
2014-01-16 12:53

@Loïc: thank you. Very useful !
Anne (reporter)
2014-01-16 14:19

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)
2014-01-16 16:10

Fix committed to master branch.
correnson (manager)
2014-01-16 16:14

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)
2014-02-04 19:07

Fix committed to feature/bug_1598 branch.
correnson (manager)
2014-02-12 16:57

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 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 Note Added: 0004485
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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker