Frama-C Bug Tracking System - Frama-C
View Issue Details
0000392Frama-CPlug-in > Evapublic2010-02-03 15:502010-04-13 15:33
djs52 
pascal 
normalcrashalways
closedfixed 
Frama-C Beryllium-20090902 
Frama-C Boron-20100401 
0000392: Failure("Function 'From.find_deps_no_transitivity' not registered yet")
Attempting 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"))
No tags attached.
Issue History
2010-02-03 15:50djs52New Issue
2010-02-03 15:50djs52Statusnew => assigned
2010-02-03 15:50djs52Assigned To => pascal
2010-02-03 15:57pascalNote Added: 0000664
2010-02-03 16:12djs52Note Added: 0000665
2010-02-03 16:15pascalStatusassigned => resolved
2010-02-03 16:15pascalFixed in Version => Frama-C svn, precise the release id
2010-02-03 16:15pascalResolutionopen => fixed
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in VersionFrama-C svn, precise the release id => Frama-C Boron
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0000664)
pascal   
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   
2010-02-03 16:12   
Yes, that's fixed it. Thanks for the quick response.