Crash when using wpo api get_result

ID0001779: This issue was created automatically from Mantis Issue 1779. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001779	Frama-C	Plug-in > wp	public	2014-05-19	2015-03-17

Reporter	jpinheiro	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	crash	Reproducibility	always
Platform	Neon-20140301	OS	mac-osx	OS Version	maveriks
Product Version	Frama-C Neon-20140301	Target Version	-	Fixed in Version	Frama-C Sodium

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))

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

Steps To Reproduce :

frama-c -load-script wp_script.ml condi.c