Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001110Frama-CKernelpublic2012-03-02 14:352014-02-12 16:58
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFrama-C Oxygen-20120901Fixed in VersionFrama-C Oxygen-20120901 
Summary0001110: Using Filter without Value
DescriptionWhen using Filter to build a new project, if the visited old project has a [code_annotation], and the value analysis is not computed, [vcode_annot] crashes on [Db.Value.is_reachable_stmt] because of the assert :
    assert (is_computed ()); (* this assertion fails during value analysis *)
in [Db.Value.get_stmt_state].

Either [Db.Value.is_reachable] should return true when the value analysis is not computed, or at least, Filter should call it only if it has been computed.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002746)
yakobowski (manager)
2012-03-05 13:01

I think using Db.Value in filter is a bad idea in general, as the argument of the functor is supposed to give all the needed information. Would the following patch be ok for you?

--- filter.ml (revision 17440)
+++ filter.ml (working copy)
@@ -421,8 +421,8 @@
       in
       debug1 "[annotation] stmt %d : %a @."
         stmt.sid !Ast_printer.d_code_annotation v;
- if Db.Value.is_reachable_stmt stmt &&
- Info.annotation_visible (self#get_finfo ()) stmt v
+ let f = self#get_finfo () in
+ if Info.annotation_visible f stmt v && Info.inst_visible f stmt
       then begin
         self#add_stmt_keep stmt;
         ChangeDoChildrenPost (v,Logic_const.refresh_code_annotation)

There is also an occurrence of Db.Value.condition_truth_value that we should get rid of, but this will require a signature change.
(0002747)
Anne (reporter)
2012-03-05 14:34

For [Db.Value.condition_truth_value], it is ok to use it because it can lead to an optimization if Value is computed, and is also ok if not.

For your patch, I am not sure about the [Info.inst_visible f] part...
Imagine in a linear sequence, you can have :

//@ assert bla;
x = ... ; // <-- invisibel
y = ...; // <-- visible

and you can still have [Info.annotation_visible], can't you ?

I think [Info.annotation_visible] should provide all the information itself...
(0002748)
yakobowski (manager)
2012-03-05 14:39

Regarding Db.Value.condition_truth_value, an equivalent function should be asked by the functor. If someone devises an entirely new analysis that uses Filter, and launches Value simultaneously, the results will be incorrect.

Concerning Info.annotation_visible, your example is quite interesting, and I agree that annotation_visible should provide a definitive answer by itself. Thus we will probably remove the call to Db.Value.is_reachable altogether, and update the modules that call Filter accordingly.
(0002749)
Anne (reporter)
2012-03-05 15:04

Great. Thanks.
(0002940)
yakobowski (manager)
2012-04-18 22:10

I'm amazed that 0001110:0002747 works (before any change), but it does. This visitor does great magic indeed :-) The final API will reflect what was decided in 0001110:0002748.
(0004696)
yakobowski (manager)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-03-02 14:35 Anne New Issue
2012-03-05 09:50 signoles Status new => assigned
2012-03-05 09:50 signoles Assigned To => virgile
2012-03-05 13:01 yakobowski Note Added: 0002746
2012-03-05 14:34 Anne Note Added: 0002747
2012-03-05 14:39 yakobowski Note Added: 0002748
2012-03-05 15:04 Anne Note Added: 0002749
2012-04-05 00:55 yakobowski Assigned To virgile => yakobowski
2012-04-08 00:06 yakobowski Target Version => Frama-C Oxygen-2012xx01
2012-04-18 22:10 yakobowski Note Added: 0002940
2012-04-18 22:18 svn Checkin
2012-04-18 22:18 svn Status assigned => resolved
2012-04-18 22:18 svn 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
2014-02-12 16:58 yakobowski Note Added: 0004696
2014-02-12 16:58 yakobowski Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker