Changeset 2736 for extracted

Timestamp:

Feb 26, 2013, 6:18:59 PM (8 years ago)

Author:

sacerdot

Message:

Untrusted fixpoint computation branched in.

Location:

extracted

Files:

• Fix.ml (added)
• Fix.mli (added)
• PROBLEMS (modified) (1 diff)
• compiler.ml (modified) (1 diff)
• compute_fixpoints.ml (added)
• compute_fixpoints.mli (added)

extracted/PROBLEMS

@@ -28 +28 @@
 
 a) two in compiler.ml (the backend and the compiler itself)
+   - file Fix.ml taken from the untrusted prototype and modified to
+     redefine a few functions from OCaml's List due to module name shadowing
+   - file compute_fixpoints.ml to adapt Fix.ml to the rest
 b) set_adt currently implemented by cut&paste from OCaml's set.ml, but
    using Pervasives.compare: the equality function taken in input is ignored!

extracted/compiler.ml

@@ -271 +271 @@
 
 (** val compute_fixpoint : Fixpoints.fixpoint_computer **)
-let compute_fixpoint _ =
-  failwith "AXIOM TO BE REALIZED"
+let compute_fixpoint = Compute_fixpoints.compute_fixpoint
 
 (** val colour_graph : Interference.coloured_graph_computer **)