Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000392Frama-CPlug-in > Evapublic2010-02-03 15:502010-04-13 15:33
Reporterdjs52 
Assigned Topascal 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000392: Failure("Function 'From.find_deps_no_transitivity' not registered yet")
DescriptionAttempting value analysis on a large code base, using -mem-exec to exclude some difficult functions. Running frama-c -val -mem-exec ... seems to complete without error; frama-c-gui with the same options fails with

Unexpected error (Failure("Function 'From.find_deps_no_transitivity' not registered yet"))
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000664)
pascal (reporter)
2010-02-03 15:57

This looks very much like a bug that was fixed in the development version recently. Could you confirm if the patch below fixes your problem?

The patch was as follows:

Index: src/inout/context.ml
===================================================================
--- src/inout/context.ml (revision 7446)
+++ src/inout/context.ml (revision 7448)
@@ -62,10 +62,6 @@
   Stack.create ()
     (* Stack of function being processed *)
 
-let find_deps_no_transitivity = !From.find_deps_no_transitivity
- (* The value of the expression [expr], just before executing the statement [instr],
- is a function of the values of the returned zones. *)
-
 module Computer (REACH:sig
                    val stmt_can_reach : stmt -> stmt -> bool
                  end) = struct
@@ -111,7 +107,7 @@
           (* update [over_inputs] using the [exp] condition:
              I+ = I+ \/+ (D+(exp) /+ O-)
           *)
- let inputs = find_deps_no_transitivity (Kstmt s) exp in
+ let inputs = !From.find_deps_no_transitivity (Kstmt s) exp in
             {data with
                over_inputs =
                 Zone.join data.over_inputs
@@ -177,7 +173,7 @@
           (fun state ->
 
              let exp_inputs_deps =
- find_deps_no_transitivity kinstr exp
+ !From.find_deps_no_transitivity kinstr exp
              in
              add_with_additional_var
                lv
@@ -203,7 +199,7 @@
                  (* inputs used by [funcexp], inputs for the evaluation of [funcexp] and its [argl] *)
                  List.fold_right
            (fun arg inputs ->
- let arg_inputs = find_deps_no_transitivity kinstr arg
+ let arg_inputs = !From.find_deps_no_transitivity kinstr arg
               in Zone.join inputs arg_inputs)
            argl
                    acc_funcexp_inputs
(0000665)
djs52 (reporter)
2010-02-03 16:12

Yes, that's fixed it. Thanks for the quick response.

- Issue History
Date Modified Username Field Change
2010-02-03 15:50 djs52 New Issue
2010-02-03 15:50 djs52 Status new => assigned
2010-02-03 15:50 djs52 Assigned To => pascal
2010-02-03 15:57 pascal Note Added: 0000664
2010-02-03 16:12 djs52 Note Added: 0000665
2010-02-03 16:15 pascal Status assigned => resolved
2010-02-03 16:15 pascal Fixed in Version => Frama-C svn, precise the release id
2010-02-03 16:15 pascal Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version Frama-C svn, precise the release id => Frama-C Boron
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker