Changeset 2648

Timestamp:

Feb 7, 2013, 10:43:39 PM (8 years ago)

Author:

sacerdot

Message:

Back in sync with the extracted code.

File:

• driver/clightFromC.ml (modified) (3 diffs)

driver/clightFromC.ml

@@ -124 +124 @@
    throughout definitions, we'll use an imperative generator here. *)
 
-let idGenerator = ref (Extracted.Identifiers.new_universe symbolTag)
+let idGenerator = ref (Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag)
 let idTable = Hashtbl.create 47
 let make_id s =
@@ -130 +130 @@
     Hashtbl.find idTable s
   with Not_found ->
-    let { Extracted.Types.fst = id; Extracted.Types.snd = g} = Extracted.Identifiers.fresh symbolTag !idGenerator in
+    let { Extracted.Types.fst = id; Extracted.Types.snd = g} = Extracted.Identifiers.fresh Extracted.PreIdentifiers.SymbolTag !idGenerator in
     idGenerator := g;
     Hashtbl.add idTable s id;
@@ -857 +857 @@
 let convertProgram (p:C.program) : clight_program option =
   numErrors := 0;
-  idGenerator := Extracted.Identifiers.new_universe symbolTag;
+  idGenerator := Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag;
   stringNum := 0;
   Hashtbl.clear decl_atom;