2021-02-27 10:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001274Frama-CKernelpublic2014-02-12 16:53
Assigned Toyakobowski 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001274: Things get mixed-up between project
DescriptionI do some computation on a first project, then I close it (Project.remove).
Then I work on another new project, and it seems that I get some information from the first project. I don't use any load/save feature.

I suspect that it comes from PDG, but I am not sure. Anyway, it is very strange that I can still print statements from the first project.

Moreover, when I use the debug mode, the problem disappear !!!

I known that you probably can do nothing with this very imprecise description,
but any hints are warmly welcome !
TagsNo tags attached.
Attached Files




yakobowski (manager)

Hi Anne,

This is indeed a bit imprecise... What do you mean by "I can still print statements from the first project"? (By this question, I mean "where do you find those statements?": in a table of the kernel, in a reference, in a data-structure of a plugin, etc.)

Notice also that statements, expressions, etc can share the same id between two projects if the second one is created by a copy of the first.


Anne (reporter)

Hi Boris, thanks for your answer.

The statements are found in PDG nodes, that is why I suspect the PDG, and also because the PDG plug-in has been written before the "project" system, so maybe something is stored outside the project, and then not cleared.

There is no copy between the two projects, and they are not even based on the same C files. The only things that are stored don't have Frama-C datatypes...

I don't have time to work on that this morning, but I hope to investigate this afternoon.

What has finished to desperate me yesterday, is that the behavior changes according to the debug mode ! It often happens in C programs, but I think that it is the first time that I see this with a ocaml program :-(


yakobowski (manager)

I have dabbled quite a bit in the PDG recently, and I did not notice a projectification problem. However, I have not read everything in detail.
FYI, Oxygen will probably be released next week. If the bug is not urgent, waiting a bit may spare you a debugging session, and will make things easier for us (no need to search for a bug in Nitrogen).


Anne (reporter)

Ok. I'll try a little, and wait for Oxygen if I don't find anything today. Anyway, I didn't expect you to search or fix things in Nitrogen : I was only expecting some hints to help me ;-)

The Oxygen release is a very good news :-)


signoles (manager)

My 2 cents... For me, the only possibility is that someone (PDG?) keeps some stmts in some global unprojectified states. But, as Boris said, the projectification of PDG looks ok until now.

Also, from time to time, the Frama-C behavior is unfortunatly not the same in debug mode and standard mode, since that is not exactly the same code which is executed in both cases. For instance, in debug mode, the AST is always computed and pretty-printed with sid first. It may lead to obscure differences.


yakobowski (manager)

After a second look, there is a suspicious looking semi-global varinfo-indexed hash table in pdg/marks.ml, called "empty". There is probably a signature misfeature, as empty should have type unit -> foobar and not just foobar if foobar is imperative. Anne, if you use marks, this may be your culprit.


Anne (reporter)

Thanks Julien.

I began to look again at the problem, and it seems that my suspicions about PDG were right since at the moment, I am trying to find nodes in a PDG that seems ok (at least when printing it), but the nodes in the result don't belong to that PDG ! I continue and keep you inform since unfortunately, I think that PDG will be quiet the same in Oxygen than in Nitrogen...


Anne (reporter)

Thanks Boris.

I don't use marks, but I have seem the same problem in pdg_state, and I was wondering if this can be a problem. But if it is, how can it usually work ???


yakobowski (manager)

In pdg_state, the datastructure behind empty is purely functional. The value for empty does not contain references to the current project, so this one should be ok.


Anne (reporter)

This is what I found so far :

In a PDG, there are states that are mapped to the program points.
A state is :
module LocInfo = Lmap_bitwise.Make_bitwise (NodeSetLattice)
that maps Locations.Zone to PDG nodes.
In my PDG, the state I am looking seems ok, but only the node numbers are printed by LocInfo.pretty. When I am getting the nodes mapped to a location in that state, I get the node 30 for instance, but when I am printing the node, I find the OLD node 30 (from the first project), not the new one.
I will continue my investigations this afternoon.

Have a nice lunch.


Anne (reporter)

Last edited: 2012-09-12 12:25

Boris, you said :
  In pdg_state, the datastructure behind empty is purely functional

but when following how LocInfo is built, I found some suspicious things in Rangemap.Make. Do you thing there can be a problem with :
   let x_table = Weak.create size
   let d_table = Weak.create size

This doesn't seems functional, does it ?


yakobowski (manager)

Anne, can you try changing the occurrence of State_builder.Counter in pdgTypes.ml by State_builder.SharedCounter?


Anne (reporter)

I am first trying to change Pdg_state.empty, and then, I 'll try to change the counter.


Anne (reporter)

The Pdg_state.empty () changed nothing :-(

I try with the counter : I suspect that it will work, but doesn't it mean that there is a problem somewhere ?...


yakobowski (manager)

Regardind note 3456: if the problem does not disappear, or FC starts crashing, this will probably mean that the bug is in your code :-) If the problem disappears the problem is probably in Frama-C.

Regarding note 3453: the weak hash tables have been removed from Rangemap in Oxygen. There was at least one unrelated bug, and the caches did not improve performance.


Anne (reporter)

The problem disappeared :-) Thanks!!!

I realized that changing Pdg_state.empty was nonsense since Lmap_bitwise.Location_map_bitwise.empty is a constant anyway...

From what you say, if the weak hash tables have been removed from Rangemap in Oxygen, maybe the problem also disappeared... I'll try as soon as I will have Oxygen on my computer ;-)

Many thanks again.


Anne (reporter)

I managed to build a small example. Shall I send it to you by e-mail Boris ?


yakobowski (manager)

Yes please! Thanks.


yakobowski (manager)

Problem is no longer present in Oxygen, even without the fix of note 3454. We must has tightened some dependencies at some point.

-Issue History
Date Modified Username Field Change
2012-09-11 17:25 Anne New Issue
2012-09-11 23:01 yakobowski Note Added: 0003442
2012-09-12 08:41 Anne Note Added: 0003443
2012-09-12 09:45 yakobowski Note Added: 0003444
2012-09-12 10:10 Anne Note Added: 0003445
2012-09-12 10:41 signoles Status new => assigned
2012-09-12 10:41 signoles Assigned To => signoles
2012-09-12 10:48 signoles Note Added: 0003446
2012-09-12 11:04 yakobowski Note Added: 0003447
2012-09-12 11:07 Anne Note Added: 0003448
2012-09-12 11:16 svn
2012-09-12 11:19 Anne Note Added: 0003450
2012-09-12 11:26 yakobowski Note Added: 0003451
2012-09-12 11:53 Anne Note Added: 0003452
2012-09-12 12:24 Anne Note Added: 0003453
2012-09-12 12:25 Anne Note Edited: 0003453
2012-09-12 12:25 Anne Note Edited: 0003453
2012-09-12 12:28 yakobowski Note Added: 0003454
2012-09-12 12:29 Anne Note Added: 0003455
2012-09-12 12:38 Anne Note Added: 0003456
2012-09-12 12:45 yakobowski Note Added: 0003457
2012-09-12 12:50 Anne Note Added: 0003458
2012-09-12 13:21 yakobowski Assigned To signoles => yakobowski
2012-09-12 13:26 Anne Note Added: 0003459
2012-09-12 13:26 yakobowski Note Added: 0003460
2012-09-12 13:44 yakobowski Note Added: 0003461
2012-09-12 13:44 yakobowski Status assigned => resolved
2012-09-12 13:44 yakobowski Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master f9145d5f
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon f9145d5f
+Issue History