Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001779Frama-CPlug-in > wppublic2014-05-19 18:272015-03-17 22:17
Reporterjpinheiro 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformNeon-20140301OSmac-osxOS Versionmaveriks
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001779: Crash when using wpo api get_result
DescriptionWhen 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005109)
yakobowski (manager)
2014-05-19 22:37
edited on: 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 :-(
(0005126)
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.
(0005131)
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?
(0005136)
virgile (developer)
2014-05-23 17:19

 Fix committed to master branch.
(0005137)
signoles (manager)
2014-05-23 17:27

 The generation of the documentation is now fixed. Thanks for this report.

- Issue History
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 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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker