aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-03-17 10:21:41 +0100
committerPierre-Marie Pédrot2015-06-24 00:13:17 +0200
commite2e88741120332f9e97459852d7361e2d8939881 (patch)
tree9674a8785e31974fb73b96b840014d86d5e14b1b /stm
parenta2fa3dd1ec96cd70c817ff375d7b857924bb9825 (diff)
Splitting the library representation on disk in two.
The first part only contains the summary of the library, while the second one contains the effective content of it.
Diffstat (limited to 'stm')
-rw-r--r--stm/vio_checking.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index b207222117..4df9603dca 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,7 +10,7 @@ open Util
let check_vio (ts,f) =
Dumpglob.noglob ();
- let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
+ let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
@@ -30,7 +30,7 @@ let schedule_vio_checking j fs =
let f =
if Filename.check_suffix f ".vio" then Filename.chop_extension f
else f in
- let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
+ let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in