View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001779 | Frama-C | Plug-in > wp | public | 2014-05-19 18:27 | 2015-03-17 22:17 | ||||
Reporter | jpinheiro | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | Neon-20140301 | OS | mac-osx | OS Version | maveriks | ||||
Product Version | Frama-C Neon-20140301 | ||||||||
Target Version | Fixed in Version | Frama-C Sodium | |||||||
Summary | 0001779: Crash when using wpo api get_result | ||||||||
Description | When using wp and wpo api, if i invoke wpo api get_result it crashes and tells me to report it. Example code: let () = Dynamic.load_module "Wp" module Wpo = Type.Abstract(struct let name = "Wpo.po" end) let get_result = Dynamic.get ~plugin:"Wp" "Wpo.get_result" (Datatype.func Wpo.ty (Datatype.func Wpo.ty Wpo.ty)) | ||||||||
Steps To Reproduce | frama-c -load-script wp_script.ml condi.c | ||||||||
Additional Information | [kernel] failure: unexpected exception "Type.Make_tbl(Key)(Info).Incompatible_type(\"Wp.Wpo.get_result has type Wpo.po -> Wpo.prover -> Wpo.result but is used with type Wpo.po -> Wpo.po -> Wpo.po.\")" [kernel] Current source was: :0 The full backtrace is: Raised at file "src/kernel/log.ml", line 524, characters 30-31 Called from file "src/kernel/log.ml", line 518, characters 9-16 Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 Called from file "list.ml", line 73, characters 12-15 Called from file "src/kernel/dynamic.ml", line 322, characters 4-154 Called from file "src/kernel/dynamic.ml", line 355, characters 6-57 Called from file "src/kernel/dynamic.ml", line 391, characters 6-22 Called from file "src/lib/FCSet.ml", line 327, characters 38-41 Called from file "queue.ml", line 134, characters 6-20 Called from file "list.ml", line 73, characters 12-15 Called from file "src/kernel/cmdline.ml", line 292, characters 10-56 Called from file "src/kernel/cmdline.ml", line 319, characters 8-51 Called from file "src/kernel/cmdline.ml", line 328, characters 49-69 Called from file "src/kernel/cmdline.ml", line 566, characters 6-137 Called from file "src/kernel/cmdline.ml", line 749, characters 4-33 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8 Frama-C aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Neon-20140301. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2014-05-19 22:37 Last edited: 2014-05-19 22:38 |
The problem is actually partially in your code. You're supposed to supply the proper type for Wpo.get_result to Dynamic.get. (Datatype.func Wpo.ty (Datatype.func Wpo.ty Wpo.ty)) corresponds to Wpo.ty -> Wpo.ty -> Wpo.ty, i.e. the second part of the error message ("but is used with type Wpo.po -> Wpo.po -> Wpo.po."). You should have written something that corresponds to "Wpo.po -> Wpo.prover -> Wpo.result" instead. Unfortunately, I think the Frama-C datatypes for Wpo.prover and Wpo.result are not exported, so this function probably can't be called dynamically :-( |
signoles (manager) 2014-05-22 14:08 |
Boris is right: the type that you provided is wrong. But Boris is also wrong ;-): this function can be dynamically called as follows: ===== module Po = Type.Abstract(struct let name = "Wpo.po" end) module Prover = Type.Abstract(struct let name = "Wpo.prover" end) module Result = Type.Abstract(struct let name = "Wpo.result" end) let get_result = Dynamic.get ~plugin:"Wp" "Wpo.get_result" (Datatype.func2 Po.ty Prover.ty Result.ty) ===== Every time the Frama-C kernel or a plug-in crashes, the name of the exception, a backtrace and an invitation to report the bug are printed. But, when you are yourself a plug-in developer, you have to verify first that the issue does not come from your own plug-in: Frama-C has no automatic way to know where the error comes from. |
jpinheiro (reporter) 2014-05-22 15:42 |
Well, i used the type provided by frama-c wpo api documentation: val get_result : po -> prover -> result Access it by Dynamic.get ~plugin:"Wp" "Wpo.get_result" (Datatype.func Wpo.ty (Datatype.func Wpo.ty Wpo.ty)) I can understand why it is wrong, but it is strange that the api gives the wrong datatype. So i can assume that the function goals_of_property type is also wrong: val goals_of_property : Property.t -> po list Access it by Dynamic.get ~plugin:"Wp" "Wpo.goals_of_property" (Datatype.func Property.ty (Datatype.list Wpo.ty)) And the type should be: (Datatype.func Property.ty (Datatype.list Po.ty)) correct? |
virgile (developer) 2014-05-23 17:19 |
Fix committed to master branch. |
signoles (manager) 2014-05-23 17:27 |
The generation of the documentation is now fixed. Thanks for this report. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-05-19 18:27 | jpinheiro | New Issue | |
2014-05-19 18:27 | jpinheiro | Status | new => assigned |
2014-05-19 18:27 | jpinheiro | Assigned To | => correnson |
2014-05-19 22:37 | yakobowski | Note Added: 0005109 | |
2014-05-19 22:38 | yakobowski | Note Edited: 0005109 | View Revisions |
2014-05-22 14:08 | signoles | Note Added: 0005126 | |
2014-05-22 14:20 | signoles | Assigned To | correnson => signoles |
2014-05-22 15:42 | jpinheiro | Note Added: 0005131 | |
2014-05-23 17:19 | virgile | Source_changeset_attached | => framac master 6d56afe2 |
2014-05-23 17:19 | virgile | Note Added: 0005136 | |
2014-05-23 17:19 | virgile | Assigned To | signoles => virgile |
2014-05-23 17:19 | virgile | Status | assigned => resolved |
2014-05-23 17:19 | virgile | Resolution | open => fixed |
2014-05-23 17:27 | signoles | Note Added: 0005137 | |
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
2015-03-17 22:17 | signoles | Status | resolved => closed |