source: extracted/PROBLEMS @ 2736

Last change on this file since 2736 was 2736, checked in by sacerdot, 6 years ago

Untrusted fixpoint computation branched in.

File size: 1.3 KB
Line 
1================
2EXTRACTION BUGS:
3================
4
51. ASM.subaddressing_modeel__o__mk_subaddressing_mode not extracted
6  val subaddressing_modeel__o__mk_subaddressing_mode:
7 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode_tag Vector.vector -> addressing_mode -> addressing_mode
8
92. File "monad.ml", line 1, characters 0-1:
10Error: The implementation monad.ml does not match the interface monad.cmi:
11       Type declarations do not match:
12         type monad0 = Preamble.__
13       is not included in
14         type 'a monad0
15       They have different arities.
16
17Error: The implementation smallstepExec.ml
18       does not match the interface smallstepExec.cmi:
19       Type declarations do not match:
20         type global = Preamble.__
21       is not included in
22         type ('a, 'b) global
23       They have different arities.
24
25=========================
26AXIOMS TO BE IMPLEMENTED:
27=========================
28
29a) two in compiler.ml (the backend and the compiler itself)
30   - file Fix.ml taken from the untrusted prototype and modified to
31     redefine a few functions from OCaml's List due to module name shadowing
32   - file compute_fixpoints.ml to adapt Fix.ml to the rest
33b) set_adt currently implemented by cut&paste from OCaml's set.ml, but
34   using Pervasives.compare: the equality function taken in input is ignored!
Note: See TracBrowser for help on using the repository browser.