2021-01-15 15:13 CET
  

View Issue Details [ Jump to Notes ] [ 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
+Relationships

-Notes

~0005109

yakobowski (manager)

2014-05-19 22:37

Last edited: 2014-05-19 22:38

View 2 revisions

 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.
+Notes

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