Ignore:
Timestamp:
Oct 7, 2011, 1:48:26 PM (9 years ago)
Author:
tranquil
Message:

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

    r1297 r1319  
    9999      let s2' = add_starting_cost_label ind cost_universe s2' in
    100100      Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
    101   | Swhile (e,s) ->
     101  | Swhile (i,e,s) ->
     102                  let ind = match i with
     103                                | None -> ind
     104                                | Some _ -> CostLabel.add_id_indexing ind in
    102105      let s' = add_cost_labels_st ind cost_universe s in
    103106      let s' = add_starting_cost_label ind cost_universe s' in
    104107      add_ending_cost_label ind cost_universe
    105         (Swhile (add_cost_labels_e ind cost_universe e, s'))
    106   | Sdowhile (e,s) ->
    107       let s1 = add_cost_labels_st ind cost_universe s in
    108       let s2 = add_cost_labels_st ind cost_universe s in
    109       let s2' = add_starting_cost_label ind cost_universe s2 in
     108        (Swhile (i,add_cost_labels_e ind cost_universe e, s'))
     109  | Sdowhile (i,e,s) ->
     110      let ind = match i with
     111        | None -> ind
     112        | Some _ -> CostLabel.add_id_indexing ind in
     113      let s' = add_cost_labels_st ind cost_universe s in
     114      let s' = add_starting_cost_label ind cost_universe s' in
    110115      add_ending_cost_label ind cost_universe
    111         (Ssequence (s1, Swhile (add_cost_labels_e ind cost_universe e, s2')))
    112   | Sfor (s1,e,s2,s3) ->
     116        (Sdowhile (i,add_cost_labels_e ind cost_universe e, s'))
     117  | Sfor (i,s1,e,s2,s3) ->
    113118      let s1' = add_cost_labels_st ind cost_universe s1 in
     119      let ind = match i with
     120        | None -> ind
     121        | Some _ -> CostLabel.add_id_indexing ind in
    114122      let s2' = add_cost_labels_st ind cost_universe s2 in
    115123      let s3' = add_cost_labels_st ind cost_universe s3 in
    116124      let s3' = add_starting_cost_label ind cost_universe s3' in
    117125      add_ending_cost_label ind cost_universe
    118         (Sfor (s1', add_cost_labels_e ind cost_universe e, s2', s3'))
     126        (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3'))
    119127  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
    120128  | Sswitch (e,ls) ->
     
    162170  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
    163171  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
    164         let ind = CostLabel.id_indexing 0 in
     172        let ind = CostLabel.empty_indexing in
    165173  {
    166174    prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct;
Note: See TracChangeset for help on using the changeset viewer.