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
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
(0004393)
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 ?
(0004394)
correnson (manager)
2014-01-09 15:50

Problem in Cil2Cfg
(0004397)
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... :-(
(0004406)
correnson (manager)
2014-01-13 10:25

Ok, not a problem.
(0004411)
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.
(0004412)
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...
(0004413)
yakobowski (manager)
2014-01-16 12:17

@Anne: the change you refer to was introduced in commit 1486f9cea38012a595b505ee179f11fc98400974
(0004414)
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"...
(0004415)
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.
(0004416)
Anne (reporter)
2014-01-16 12:53

@Loïc: thank you. Very useful !
(0004417)
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).
(0004418)
correnson (manager)
2014-01-16 16:10

Fix committed to master branch.
(0004420)
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.
(0004485)
correnson (manager)
2014-02-04 19:07

Fix committed to feature/bug_1598 branch.
(0004542)
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker