Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (9 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r818 r1462  
    130130  let Clight.Expr (e, t) = e in
    131131  match e with
    132     | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 ->
     132    | Clight.Ecost (lbl, e)
     133        when CostLabel.Map.mem lbl cost_mapping &&
     134             CostLabel.Map.find lbl cost_mapping = 0 ->
    133135        e
    134136    | _ ->
     
    300302  (cost_incr, Clight.Internal cfun)
    301303
     304(* Create a fresh uninitialized cost variable for each external function. This
     305   will be used by the Cost plug-in of the Frama-C platform. *)
     306
     307let extern_cost_variables make_unique functs =
     308  let prefix = "_cost_of_" in
     309  let f (decls, map) (_, def) = match def with
     310    | Clight.Internal _ -> (decls, map)
     311    | Clight.External (id, _, _) ->
     312      let new_var = make_unique (prefix ^ id) in
     313      (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in
     314  List.fold_left f ([], StringTools.Map.empty) functs
     315
    302316let save_tmp tmp_file s =
    303317  let cout = open_out tmp_file in
     
    316330  (* Create a fresh 'cost' variable. *)
    317331  let names = names p in
    318   let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
     332  let make_unique = StringTools.make_unique names in
     333  let cost_id = make_unique cost_id_prefix in
    319334  let cost_decl = cost_decl cost_id in
     335
     336  (* Create a fresh uninitialized global variable for each extern function. *)
     337  let (extern_cost_decls, extern_cost_variables) =
     338    extern_cost_variables make_unique p.Clight.prog_funct in
    320339
    321340  (* Define an increment function for the cost variable. *)
     
    330349
    331350  (* Glue all this together. *)
    332   let prog_vars = cost_decl :: p.Clight.prog_vars in
     351  let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in
    333352  let prog_funct = cost_incr_def :: prog_funct in
    334353  let p' =
     
    343362  let res = ClightParser.process tmp_file in
    344363  Misc.SysExt.safe_remove tmp_file ;
    345   (res, cost_id, cost_incr)
     364  (res, cost_id, cost_incr, extern_cost_variables)
Note: See TracChangeset for help on using the changeset viewer.