Project

General

Profile

Revision 861f327f

View differences:

src/causality.ml
331 331
       then ESet.add expr (get_expr_calls prednode e)
332 332
       else (get_expr_calls prednode e)
333 333

  
334
  let get_eexpr_calls prednode ee =
335
    get_expr_calls prednode ee.eexpr_qfexpr
336
    
334 337
  let get_callee expr =
335 338
    match expr.expr_desc with
336 339
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
337 340
    | _ -> None
338 341

  
339
  let get_calls prednode nd =
340
    let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl in
341
    let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in
342
    let rec get_stmt_calls s =
343
      match s with Eq eq -> get_eq_calls eq | Aut aut -> get_aut_calls aut 
344
    and get_aut_calls aut =
345
      let get_handler_calls h =
346
	let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in
347
	let until = get_cond_calls h.hand_until in
348
	let unless = get_cond_calls h.hand_unless in
349
	let calls = ESet.union until unless in 
350
	let calls = accu get_stmt_calls calls h.hand_stmts in
351
	let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in
352
	(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)
353
	calls
354
      in
355
      accu get_handler_calls ESet.empty aut.aut_handlers
342
  let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl 
343

  
344
  let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs
345
                      
346
  let rec get_stmt_calls prednode s =
347
    match s with Eq eq -> get_eq_calls prednode eq | Aut aut -> get_aut_calls prednode aut 
348
  and get_aut_calls prednode aut =
349
    let get_handler_calls prednode h =
350
      let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in
351
      let until = get_cond_calls h.hand_until in
352
      let unless = get_cond_calls h.hand_unless in
353
      let calls = ESet.union until unless in 
354
      let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in
355
      let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in
356
      (* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)
357
      calls
356 358
    in
359
    accu (get_handler_calls prednode) ESet.empty aut.aut_handlers
360
    
361
  let get_calls prednode nd =
357 362
    let eqs, auts = get_node_eqs nd in
358
    let deps = accu get_eq_calls ESet.empty eqs in
359
    let deps = accu get_aut_calls deps auts in
363
    let deps = accu (get_eq_calls prednode) ESet.empty eqs in
364
    let deps = accu (get_aut_calls prednode) deps auts in
360 365
    ESet.elements deps
361 366

  
367
  let get_contract_calls prednode c =
368
    let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in
369
    let deps = accu (get_eexpr_calls prednode) deps ( c.assume @ c.guarantees @ (List.fold_left (fun accu m -> accu @ m.require @ m.ensure ) [] c.modes)) in
370
    let id_deps = List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps) in  
371
    let id_deps = (List.fold_left (fun accu imp -> imp.import_nodeid::accu) [] c.imports) @ id_deps in  
372
    id_deps
373
    
362 374
  let dependence_graph prog =
363 375
    let g = new_graph () in
364 376
    let g = List.fold_right 
......
387 399
           let deps_spec = match nd.node_spec with
388 400
             | None -> []
389 401
             | Some (NodeSpec id) -> [id]
390
             | Some (Contract c) -> []
402
             | Some (Contract c) -> get_contract_calls (fun _ -> true) c
403
                                  
391 404
           in
392 405
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
393 406
	   add_edges [nd.node_id] (deps@deps_asserts@deps_spec) accu
src/sortProg.ml
45 45
    Causality.pp_error Format.err_formatter err;
46 46
    raise exc
47 47
  in
48
  
48 49
  Log.report ~level:3 
49 50
    (fun fmt -> Format.fprintf fmt "Ordered list of declarations:@.%a@.@?" (Utils.fprintf_list ~sep:"@." Printers.pp_short_decl) sorted);
50 51
  	  not_nodes@sorted

Also available in: Unified diff