Changeset 2648 for driver/clightFromC.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:39 PM (7 years ago)
Author:
sacerdot
Message:

Back in sync with the extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/clightFromC.ml

    r2620 r2648  
    124124   throughout definitions, we'll use an imperative generator here. *)
    125125
    126 let idGenerator = ref (Extracted.Identifiers.new_universe symbolTag)
     126let idGenerator = ref (Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag)
    127127let idTable = Hashtbl.create 47
    128128let make_id s =
     
    130130    Hashtbl.find idTable s
    131131  with Not_found ->
    132     let { Extracted.Types.fst = id; Extracted.Types.snd = g} = Extracted.Identifiers.fresh symbolTag !idGenerator in
     132    let { Extracted.Types.fst = id; Extracted.Types.snd = g} = Extracted.Identifiers.fresh Extracted.PreIdentifiers.SymbolTag !idGenerator in
    133133    idGenerator := g;
    134134    Hashtbl.add idTable s id;
     
    857857let convertProgram (p:C.program) : clight_program option =
    858858  numErrors := 0;
    859   idGenerator := Extracted.Identifiers.new_universe symbolTag;
     859  idGenerator := Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag;
    860860  stringNum := 0;
    861861  Hashtbl.clear decl_atom;
Note: See TracChangeset for help on using the changeset viewer.