inversed patch

svn path=/nixpkgs/trunk/; revision=4560

1 files changed, 511 insertions, 511 deletions

diff --git a/pkgs/development/libraries/cil-aterm/cil-aterm-1.3.4.patch b/pkgs/development/libraries/cil-aterm/cil-aterm-1.3.4.patch
index c64ae441a6d6..a48be67518f7 100644
--- a/pkgs/development/libraries/cil-aterm/cil-aterm-1.3.4.patch
+++ b/pkgs/development/libraries/cil-aterm/cil-aterm-1.3.4.patch
@@ -1,535 +1,535 @@
-diff -urN cil/Makefile.cil.in cil.orig/Makefile.cil.in
---- cil/Makefile.cil.in	2006-01-16 13:33:41.000000000 +0100
-+++ cil.orig/Makefile.cil.in	2005-11-22 06:34:41.000000000 +0100
-@@ -78,7 +78,6 @@
+diff -urN cil.orig/Makefile.cil.in cil/Makefile.cil.in
+--- cil.orig/Makefile.cil.in	2005-11-22 06:34:41.000000000 +0100
++++ cil/Makefile.cil.in	2006-01-16 13:33:41.000000000 +0100
+@@ -78,6 +78,7 @@
                canonicalize heap oneret partial simplemem simplify \
  	      dataslicing \
                testcil \
--              atermprinter \
++              atermprinter \
  	      $(CILLY_FEATURES) \
  	      feature_config
  # ww: we don't want "maincil" in an external cil library (cil.cma),
-@@ -537,8 +536,6 @@
+@@ -536,6 +537,8 @@
  
  prefix = @prefix@
  exec_prefix = @exec_prefix@
--bindir = @prefix@/bin
--objdir = @prefix@/$(OBJDIR)
++bindir = @prefix@/bin
++objdir = @prefix@/$(OBJDIR)
  libdir = @libdir@
  pkglibdir = $(libdir)/cil
  datadir = @datadir@
-@@ -557,10 +554,6 @@
+@@ -554,6 +557,10 @@
  	$(INSTALL_DATA) $(install_lib) $(DESTDIR)$(pkglibdir)
  	$(INSTALL) -d $(DESTDIR)$(pkgdatadir)
  	$(INSTALL_DATA) $(addprefix lib/, $(filter %.pm, $(DISTRIB_LIB))) $(DESTDIR)$(pkgdatadir)
--	$(INSTALL) -d $(bindir)
--	$(INSTALL) -d $(objdir)
--	$(INSTALL) bin/* $(bindir)
--	$(INSTALL) $(OBJDIR)/*.exe $(objdir)
++	$(INSTALL) -d $(bindir)
++	$(INSTALL) -d $(objdir)
++	$(INSTALL) bin/* $(bindir)
++	$(INSTALL) $(OBJDIR)/*.exe $(objdir)
  
  cil.spec: cil.spec.in
  	./config.status $@
-diff -urN cil/src/ext/atermprinter.ml cil.orig/src/ext/atermprinter.ml
---- cil/src/ext/atermprinter.ml	2006-01-16 10:36:29.000000000 +0100
-+++ cil.orig/src/ext/atermprinter.ml	1970-01-01 01:00:00.000000000 +0100
-@@ -1,489 +0,0 @@
--open Cil
--open Pretty
--open List
--open String
--open Printf
--module S = String 
--module E = Errormsg
--module H = Hashtbl
--module IH = Inthash
--
--let outputfilename = ref "cil.aterm"
--let trace p = eprintf "%s" (p ^ "\n") ; flush stderr
--let invalidStmt = mkStmt (Instr [])
--let id = fun x -> x 
--let compose f g x = (f (g x))
--let (@) = compose
--let pSpace            = text " "
--let foldl1 op ls      = match ls with
--			| (x::xs) -> fold_left op x xs
--                        | _       -> raise (Invalid_argument "foldl1 should not take an empty list")
--let pPacked d l r     = l ++ d ++ r
--let pParens d         = pPacked d (text "(") (text ")")
--let pBraced d         = pPacked d (text "{") (text "}")
--let pSquared d        = pPacked d (text "[") (text "]")
--let pSpaced d         = pPacked d pSpace pSpace
--let pBool b           = (pSpaced @ text @ S.capitalize @ string_of_bool) b
--let pInt64 i          = text (Int64.to_string i)
--let pSeqSep sep xs    = match xs with
--			| [] -> nil
--                        | _  -> foldl1 (pPacked sep) xs
--let pCommaSep xs      = pSeqSep (text ",") xs
--let pPair (a,b)       = (pSpaced @ pParens @ pCommaSep) [a;b]
--let pTriplet (a,b,c)  = (pSpaced @ pParens @ pCommaSep) [a;b;c]
--let pSemiColSep xs    = pSeqSep (text ";") xs
--let pTriple f g h (a,b,c) = (f a, g b, h c)
--let pDouble f g (a,b) = (f a, g b)
--let pOption p m  = match m with
--	         | None   -> text "None()"
--                 | Some v -> text "Some" ++ pParens( p v )
--let pSpParens = pSpaced @ pParens
--let pQuoted str = pPacked (text(escaped str)) (text "\"") (text "\"")
--let pList   = pSpaced @ pSquared @ pCommaSep
--let pRecord = pSpaced @ pBraced  @ pCommaSep
--
--class atermPrinter : cilPrinter  = 
--object (self)
--  inherit defaultCilPrinterClass
--
--  (* printing variable declarations; just store the varinfo *)
--  method pVDecl () (vinfo:varinfo) : doc = if !E.verboseFlag then trace "pVDecl"
--                                         ; self#pp_varinfo vinfo
--  (* printing variable uses; same as declarations; store the varinfo *)
--  method pVar (vinfo:varinfo) : doc = if !E.verboseFlag then trace "pVar" ;
--    self#pp_varinfo vinfo
--
--  method pLval () ((lh, off):lval) : doc = if !E.verboseFlag then trace "pLvalue" ;
--    text "Lvalue" ++ (pParens @ pCommaSep) [ self#pp_lhost lh ; self#pOffset nil off ] 
--
--  (** we are not using the first argument which represents the base from which we are
--      offsetting, because we just want to generate a tree view of the CIL tree. For a tree view
--      this base case is not necessary **)
--  method pOffset (d:doc) (o:offset) : doc = if !E.verboseFlag then trace "pOffset" ;
--    match o with
--    | NoOffset           -> text "Offset_NoOffset() "
--    | Field (finfo, off) -> text "Offset_Field" ++ (pParens @ pCommaSep) [ (self#pFieldDecl ()) finfo ; self#pOffset nil off ]
--    | Index (e, off)     -> text "Offset_Index" ++ (pParens @ pCommaSep) [ self#pExp () e ; self#pOffset nil off ]
--  
--  (*** INSTRUCTIONS ***)
--  method pInstr () (i:instr) : doc = if !E.verboseFlag then trace "pInstr" ;
--    match i with
--    | Set (lv,e,l) -> text "Set" ++ (pParens @ pCommaSep) [ 
--	self#pLval () lv ;
--	self#pExp () e ;
--	self#pp_location l ]
--    | Call (olv,e, elst, l) -> text "Call" ++ (pParens @ pCommaSep) [
--	pOption (self#pLval ()) olv ;
--	self#pExp () e ;
--	pList (map (self#pExp ()) elst) ;
--	self#pp_location l]
--    | Asm (attr, slst1, slvlst, selst, slst2, l) -> text "Asm" ++ (pParens @ pCommaSep) [
--	self#pAttrs () attr ;
--	(pList  @ map pQuoted) slst1 ;
--	pList (map (pPair @ pDouble pQuoted (self#pLval ())) slvlst) ;
--	pList (map (pPair @ pDouble pQuoted (self#pExp ())) selst) ;
--	(pList  @ map pQuoted) slst2 ;
--	self#pp_location l]
--
--  (* a statement itself is just a record of info about the statement
--     the different kinds of statements can be found at pStmtKind *) 
--  method pStmt () (s:stmt) : doc = if !E.verboseFlag then trace "pStmt" ;
--    self#pp_stmtinfo s
--  method dStmt (out:out_channel) (i:int) (s:stmt) : unit = fprint out i (self#pStmt () s)
--
--  (* a block is just a record of info about the block of interest.
--     the real block is a stmtkind (see pStmtKind) *)
--  method dBlock (out:out_channel) (i:int) (b:block) : unit = fprint out i (self#pBlock () b)
--  method pBlock () (b:block) : doc = if !E.verboseFlag then trace "pBlock" ;
--    self#pp_blockinfo b
--
--  (*** GLOBALS ***)
--  method pGlobal () (g:global) : doc = if !E.verboseFlag then trace "pGlobal" ;      (* global (vars, types, etc.) *)
--    match g with 
--    | GType        (typ , l) -> text "GlobalType" ++ (pParens @ pCommaSep) [ self#pp_typeinfo typ ; self#pp_location l ]
--    | GCompTag     (comp, l) -> text "GlobalCompTag" ++ (pParens @ pCommaSep) [ self#pp_compinfo comp ; self#pp_location l ]
--    | GCompTagDecl (comp, l) -> text "GlobalCompTagDecl" ++ (pParens @ pCommaSep) [ self#pp_compinfo comp ; self#pp_location l ]
--    | GEnumTag     (enum, l) -> text "GlobalEnumTag" ++ (pParens @ pCommaSep) [ self#pp_enuminfo enum ; self#pp_location l ]
--    | GEnumTagDecl (enum, l) -> text "GlobalEnumTagDecl" ++ (pParens @ pCommaSep) [ self#pp_enuminfo enum ; self#pp_location l ]
--    | GVarDecl     (vinf, l) -> text "GlobalVarDecl" ++ (pParens @ pCommaSep) [ self#pp_varinfo vinf ; self#pp_location l ]
--    | GVar   (vinf, iinf, l) -> text "GlobalVar" ++ (pParens @ pCommaSep) [ self#pp_varinfo vinf ; self#pp_initinfo iinf ; self#pp_location l ]
--    | GFun         (fdec, l) -> text "GlobalFun" ++ (pParens @ pCommaSep) [ self#pp_fundec fdec ; self#pp_location l ]
--    | GAsm         (str , l) -> text "GlobalAsm"  ++ (pParens @ pCommaSep) [ pQuoted str ; self#pp_location l ]
--    | GPragma      (attr, l) -> text "GlobalPragma" ++ (pParens @ pCommaSep) [ (fun (doc1, bool1) -> doc1) (self#pAttr attr)
--                                                        ; self#pp_location l
--                                        ]
--    | GText str -> text "GlobalText" ++ pParens( pQuoted str)
--  method dGlobal (out:out_channel) (g:global) : unit = fprint out 80 (self#pGlobal () g)
--
--  (* a fielddecl is just a record containing info about the decl *)
--  method pFieldDecl () : fieldinfo -> doc = if !E.verboseFlag then trace "pFieldDecl" ;
--    self#pp_fieldinfo
--
--  (*** TYPES ***)
--  method pType (nameOpt: doc option) (* Whether we are declaring a name or 
--                                      * we are just printing a type *)
--               () (t:typ) =  if !E.verboseFlag then trace "pType" ;     (* use of some type *)
--    match t with
--    | TVoid  attr         -> text "TVoid" ++ pParens( self#pAttrs () attr)
--    | TInt   (ikin, attr) -> text "TInt" ++ (pParens @ pCommaSep) [ self#pp_ikind ikin ; self#pAttrs () attr ]
--    | TFloat (fkin, attr) -> text "TFloat" ++ (pParens @ pCommaSep) [ self#pp_fkind fkin ; self#pAttrs () attr ]
--    | TPtr   (t   , attr) -> text "TPtr" ++ (pParens @ pCommaSep) [ self#pType None () t ; self#pAttrs () attr ]
--    | TArray (t, e, attr) -> text "TArray" ++ (pParens @ pCommaSep) [ self#pType None () t ;
--	pOption (self#pExp ()) e ; self#pAttrs () attr ]
--    | TFun (t, olst, b, attr) -> text "TFun" ++ (pParens @ pCommaSep) [ 
--        self#pType None () t ;
--	pOption (pList @ (map ( pTriplet
--                              @ (pTriple (pQuoted) (self#pType None ()) (self#pAttrs ()))
--                              )     
--                         )
--                )
--                olst ;
--	pBool b ;
--	self#pAttrs () attr]
--    | TNamed (tinfo, attr) -> text "TNamed" ++ (pParens @ pCommaSep) [ self#pp_typeinfo tinfo ; self#pAttrs () attr ]
--    | TComp  (cinfo, attr) -> text "TComp" ++ (pParens @ pCommaSep) [ (text @ string_of_int) cinfo.ckey ;
--                                                           self#pAttrs () attr]
--    | TEnum  (einfo, attr) -> text "TEnum" ++ (pParens @ pCommaSep) [ self#pp_enuminfo einfo ; self#pAttrs () attr ]
--    | TBuiltin_va_list (attr) -> text "TBuiltin_va_list" ++ pParens( self#pAttrs () attr)
--  
--  (*** ATTRIBUTES ***)
--  method pAttr (Attr(an, args) : attribute) : (doc * bool) = if !E.verboseFlag then trace "pAttr" ;
--    ( text "Attr" ++ (pParens @ pCommaSep) [ pQuoted an ; pList (map (self#pAttrParam ()) args) ]
--    , false
--    )
--
--  method pAttrParam () (p:attrparam) : doc = if !E.verboseFlag then trace "pAttrParam" ;
--    match p with
--    | AInt      (i)               -> text "AInt" ++ pParens( pQuoted (string_of_int i))
--    | AStr      (s)               -> text "AStr" ++ pParens( pQuoted s)
--    | ACons     (s, args)         -> text "ACons" ++ (pParens @ pCommaSep) [ pQuoted s ; pList (map (self#pAttrParam ()) args) ]
--    | ASizeOf   (t)               -> text "ASizeOf" ++ pParens( self#pType None () t)
--    | ASizeOfE  (arg)             -> text "ASizeOfE" ++ pParens( self#pAttrParam () arg)
--    | ASizeOfS  (tsig)            -> text "ASizeOfS" ++ pParens( self#pp_typsig tsig)
--    | AAlignOf  (t)               -> text "AAlignOf" ++ pParens( self#pType None () t)
--    | AAlignOfE (arg)             -> text "AAlignOfE" ++ pParens( self#pAttrParam () arg)
--    | AAlignOfS (tsig)            -> text "AAlignOfS" ++ pParens( self#pp_typsig tsig)
--    | AUnOp     (uop, arg)        -> text "AUnOp" ++ (pParens @ pCommaSep) [ self#pp_unop uop ; self#pAttrParam () arg ]
--    | ABinOp    (bop, arg1, arg2) -> text "ABinOp" ++ (pParens @ pCommaSep) [ self#pp_binop bop 
--                                                                ; self#pAttrParam () arg1
--                                                                ; self#pAttrParam () arg2 ]
--    | ADot      (arg, s)          -> text "ADot" ++ (pParens @ pCommaSep) [ self#pAttrParam () arg ; pQuoted s]
--
--  method pAttrs () (attr:attributes) : doc = if !E.verboseFlag then trace "pAttrs" ;
--    text "Attributes" ++ pParens( 
--               pList (map (fst @ self#pAttr) attr)
--              )
--  
--  (*** LABELS ***)
--  method pLabel () (l:label) : doc = if !E.verboseFlag then trace "pLabel" ;
--    match l with
--    | Label   (s,l,b) -> text "Label" ++ (pParens @ pCommaSep) [
--	pQuoted s ;
--	self#pp_location l ;
--	pBool b ]
--    | Case    (e,l)   -> text "Case" ++ (pParens @ pCommaSep) [ 
--	self#pExp () e ;
--	self#pp_location l ]
--    | Default (l)     -> text "Default" ++ pParens( self#pp_location l)
--
--  (*** printing out locations as line directives is not necessary
--       because we are printing the tree structure and locations are
--       present everywhere ***)
--  method pLineDirective : ?forcefile:bool -> location -> doc = fun ?forcefile _ -> nil
--
--  (*** STATEMENT KINDS ***)
--  method pStmtKind s () (sk:stmtkind) : doc = if !E.verboseFlag then trace "pStmtKind" ;
--    match sk with
--    | Instr      (ilst)          -> text "Instr" ++ pParens( pList (map (self#pInstr ()) ilst))
--    | Return     (oe, l)         -> text "Return" ++ (pParens @ pCommaSep) [ pOption (self#pExp ()) oe ; self#pp_location l ]
--    | Goto       (stmtref, l)    -> text "Goto" ++ (pParens @ pCommaSep) [ self#pStmt () !stmtref ; self#pp_location l ]
--    | Break      (l)             -> text "Break" ++ pParens( self#pp_location l)
--    | Continue   (l)             -> text "Continue" ++ pParens( self#pp_location l)
--    | If         (e, b1, b2, l)  -> text "If" ++ (pParens @ pCommaSep) [ 
--	self#pExp () e ;
--	self#pBlock () b1 ;
--	self#pBlock () b2 ;
--	self#pp_location l ]
--    | Switch     (e,b,stlst,l)   -> text "Switch" ++ (pParens @ pCommaSep) [ 
--	self#pExp () e ;
--	self#pBlock () b ;
--	pList (map (self#pStmt ()) stlst) ;
--	self#pp_location l ]
--    | Loop       (b,l,os1, os2)  -> text "Loop" ++ (pParens @ pCommaSep) [
--	self#pBlock () b ;
--	self#pp_location l ;
--	pOption (self#pStmt ()) os1 ;
--	pOption (self#pStmt ()) os2 ]
--    | Block      (b)             -> text "Block" ++ pParens( self#pBlock () b)
--    | TryFinally (b1,b2,l)       -> text "TryFinally" ++ (pParens @ pCommaSep) [ 
--	self#pBlock () b1 ;
--	self#pBlock () b2 ;
--	self#pp_location l ]
--    | TryExcept  (b1, pr, b2, l) -> text "TryExcept" ++ (pParens @ pCommaSep) [ 
--	self#pBlock () b1 ;
--	(  pPair
--         @ pDouble (pList @ map (self#pInstr ())) 
--                   (self#pExp ())
--        ) pr ;
--	self#pBlock () b2 ;
--	self#pp_location l ]
--
--  (*** EXPRESSIONS ***)
--
--  method pExp () (e:exp) : doc = if !E.verboseFlag then trace "pExp" ;
--    match e with
--    | Const     (c)              -> text "Constant" ++ pParens( self#pp_constant c)
--    | Lval      (lh,off)         -> text "Lvalue" ++ (pParens @ pCommaSep)  [self#pp_lhost lh ; self#pOffset nil off ]
--    | SizeOf    (t)              -> text "SizeOfType" ++ pParens( self#pType None () t)
--    | SizeOfE   (e)              -> text "SizeOfExp" ++ pParens( self#pExp () e)
--    | SizeOfStr (s)              -> text "SizeOfString" ++ pParens( pQuoted s)
--    | AlignOf   (t)              -> text "AlignOfType" ++ pParens( self#pType None () t)
--    | AlignOfE  (e)              -> text "AlignOfExp" ++ pParens( self#pExp () e)
--    | UnOp      (uop, e, t)      -> text "UnOp" ++ (pParens @ pCommaSep) [ 
--					self#pp_unop uop ; 
--                                        self#pExp () e ; 
--	                                self#pType None () t ]
--    | BinOp     (bop, e1, e2, t) -> text "BinOp" ++ (pParens @ pCommaSep) [ 
--                                        self#pp_binop bop ;
--                                        self#pExp () e1 ;
--                                        self#pExp () e2 ;
--                                        self#pType None () t ]
--    | CastE     (t,e)            -> text "Cast" ++ (pParens @ pCommaSep) [ self#pType None () t ; self#pExp () e]
--    | AddrOf    (lv)             -> text "AddressOf" ++ pParens( self#pLval () lv)
--    | StartOf   (lv)             -> text "StartOf" ++ pParens( self#pLval () lv)
--
--  (*** INITIALIZERS ***)
--  method pInit () (i:init) : doc = if !E.verboseFlag then trace "pInit" ;
--    match i with
--    | SingleInit   (e)        -> text "SingleInit" ++ pParens( self#pExp () e)
--    | CompoundInit (t, oilst) -> text "CompoundInit" ++ (pParens @ pCommaSep) [ self#pType None () t ;
--				    pList (map (  pPair
--			                        @ pDouble (self#pOffset nil) (self#pInit ())
--			                       ) 
--			                       oilst
--			                  ) ]
--  method dInit (out:out_channel) (i:int) (init1:init) : unit = fprint out i (self#pInit () init1)
--
--  (*** auxiliary methods ***)
--  (* Mart: hmmmm *)
--  method private pp_storage (s:storage) : doc =
--    let tok = match s with
--	      | NoStorage -> "NoStorage"
--	      | Static    -> "Static"
--	      | Register  -> "Register"
--	      | Extern	  -> "Extern"
--    in pQuoted ("Storage" ^ tok)
--
--  method private pp_typeinfo (tinfo:typeinfo) : doc = if !E.verboseFlag then trace "pp_typeinfo" ;
--    text "Typeinfo" ++ (pParens @ pCommaSep) [   
--    pQuoted tinfo.tname ;
--    self#pType None () tinfo.ttype ;
--    pBool tinfo.treferenced ]
--
--  method private pp_fieldinfo (finfo:fieldinfo) : doc = if !E.verboseFlag then trace "pp_fieldinfo" ;
--    text "Fieldinfo" ++ (pParens @ pCommaSep) [ 
--    pQuoted finfo.fname ;
--    self#pType None () finfo.ftype ;
--    pOption (pQuoted @ string_of_int) finfo.fbitfield ;
--    self#pAttrs () finfo.fattr ;
--    self#pp_location finfo.floc ]
--
--  method private pp_compinfo (cinfo:compinfo) : doc = if !E.verboseFlag then trace "pp_compinfo" ;
--    text "Compinfo" ++ (pParens @ pCommaSep) [ 
--    pBool cinfo.cstruct ;
--    pQuoted cinfo.cname ;
--    text (string_of_int cinfo.ckey) ;
--    pList (map (self#pFieldDecl ()) cinfo.cfields) ;
--    self#pAttrs () cinfo.cattr ;
--    pBool cinfo.cdefined ;
--    pBool cinfo.creferenced ]
--
--  method private pp_enuminfo (einfo:enuminfo) : doc = if !E.verboseFlag then trace "pp_enuminfo" ;
--    text "Enuminfo" ++ (pParens @ pCommaSep) [
--    pQuoted einfo.ename ;
--    pList (map (  pTriplet
--                @ (pTriple pQuoted (self#pExp ()) self#pp_location)
--               )
--               einfo.eitems) ;
--    self#pAttrs () einfo.eattr ;
--    pBool einfo.ereferenced ]
--
--  method private pp_location (loc:location) : doc = if !E.verboseFlag then trace "pp_location" ;
--    text "Location" ++ (pParens @ pCommaSep) [
--    text (string_of_int loc.line) ;
--    pQuoted loc.file ;
--    text (string_of_int loc.byte) ]
--
--  method private pp_varinfo (vinfo:varinfo) : doc = if !E.verboseFlag then trace "pp_varinfo" ;
--    text "Varinfo" ++ (pParens @ pCommaSep) [
--    pQuoted vinfo.vname ;
--    self#pType None () vinfo.vtype ;
--    self#pAttrs () vinfo.vattr ;
--    self#pp_storage vinfo.vstorage ;
--    pBool vinfo.vglob ;
--    pBool vinfo.vinline ;
--    self#pp_location vinfo.vdecl ;
--    text (string_of_int vinfo.vid) ;
--    pBool vinfo.vaddrof ;
--    pBool vinfo.vreferenced ]
--
--  method private pp_initinfo (iinfo:initinfo) : doc = if !E.verboseFlag then trace "pp_initinfo" ;
--    text "Initinfo" ++ pParens( 
--    pOption (self#pInit ()) iinfo.init)
--
--  method private pp_fundec (fdec:fundec) : doc = if !E.verboseFlag then trace "pp_fundec" ;
--    text "Fundec" ++ (pParens @ pCommaSep) [
--    self#pp_varinfo fdec.svar ;
--    pList (map self#pp_varinfo fdec.sformals) ;
--    pList (map self#pp_varinfo fdec.slocals) ;
--    text (string_of_int fdec.smaxid) ;
--    self#pBlock () fdec.sbody ;
--    pOption (pSpParens @ text @ string_of_int) fdec.smaxstmtid ;
--    pList (map (self#pStmt ()) fdec.sallstmts) ]
--
--  method private pp_ikind (ikin:ikind) : doc =
--    let tok = match ikin with
--              | IChar  -> "IChar"
--	      | ISChar -> "ISChar"
--	      | IUChar -> "IUChar"
--	      | IInt   -> "IInt"
--	      | IUInt  -> "IUInt"
--	      | IShort -> "IShort"
--	      | IUShort -> "IUShort"
--	      | ILong  -> "ILong"
--	      | IULong -> "IULong"
--	      | ILongLong -> "ILongLong"
--	      | IULongLong -> "IULongLong"
--    in  pQuoted ("Ikind" ^ tok)
--
--  method private pp_fkind (fkin:fkind) : doc =
--    let tok = match fkin with
--	      | FFloat -> "FFloat"
--	      | FDouble -> "FDouble"
--	      | FLongDouble -> "FLongDouble"
--    in pQuoted ("Fkind" ^ tok)
--
--  method private pp_typsig (tsig:typsig) : doc = if !E.verboseFlag then trace "pp_typsig" ;
--    match tsig with
--    | TSArray (tsig2, oe, attr)         -> text "TSArray" ++ (pParens @ pCommaSep) [
--					      self#pp_typsig tsig2 ;
--					      pOption pInt64 oe ;
--					      self#pAttrs () attr ]
--    | TSPtr   (tsig2, attr)             -> text "TSPtr" ++ (pParens @ pCommaSep) [
--					      self#pp_typsig tsig2 ;
--					      self#pAttrs () attr ]	
--    | TSComp  (b, s, attr)              -> text "TSComp" ++ (pParens @ pCommaSep) [
--					      pBool b ;
--					      pQuoted s ;
--					      self#pAttrs () attr ]
--    | TSFun   (tsig2, tsiglst, b, attr) -> text "TSFun" ++ (pParens @ pCommaSep) [
--					      self#pp_typsig tsig2 ;
--					      pList (map self#pp_typsig tsiglst) ;
--					      pBool b ;
--					      self#pAttrs () attr ]
--    | TSEnum  (s, attr)                 -> text "TSEnum" ++ (pParens @ pCommaSep) [
--					      pQuoted s ;
--					      self#pAttrs () attr ]
--    | TSBase  (t)                       -> text "TSBase" ++ pParens( self#pType None () t)
--     
--
--  method private pp_unop (uop:unop) : doc =
--    let tok = match uop with
--	      | Neg -> "Neg"
--	      | BNot -> "BNot"
--	      | LNot -> "LNot"
--    in pQuoted ("UnOp" ^ tok)
--
--  method private pp_binop (bop:binop) : doc = 
--    let tok = match bop with
--              | PlusA -> "PlusA"
--	      | PlusPI -> "PlusPI"
--	      | IndexPI -> "IndexPI"
--	      | MinusA -> "MinusA"
--	      | MinusPI -> "MinusPI"
--	      | MinusPP -> "MinusPP"
--	      | Mult -> "Mult"
--	      | Div -> "Div"
--	      | Mod -> "Mod"
--	      | Shiftlt -> "Shiftlt"
--	      | Shiftrt -> "Shiftrt"
--	      | Lt -> "Lt"
--	      | Gt -> "Gt"
--	      | Le -> "Le"
--	      | Ge -> "Ge"
--	      | Eq -> "Eq"
--	      | Ne -> "Ne"
--	      | BAnd -> "BAnd"
--	      | BXor -> "BXor"
--	      | BOr -> "BOr"
--	      | LAnd -> "LAnd"
--	      | LOr -> "LOr"
--    in pQuoted ("BinOp" ^ tok )
--
--  method private pp_constant (c:constant) : doc = if !E.verboseFlag then trace "pp_constant" ;
--    match c with
--    | CInt64 (i, ikin, os) -> text "CInt64" ++ (pParens @ pCommaSep) [  
--                                  pQuoted (Int64.to_string i)  ;
--				  self#pp_ikind ikin ;
--				  pOption pQuoted os ]
--    | CStr   (s)           -> text "CStr" ++ pParens( pQuoted s)
--    | CWStr  (ilist)       -> text "CWStr" ++ pParens( pList (map ( text @ Int64.to_string) ilist))
--    | CChr   (c)           -> text "CChr" ++ pParens( text "\"" ++ text (Char.escaped c) ++ text "\"")
--    | CReal  (f, fkin, os) -> text "CReal" ++ (pParens @ pCommaSep) [  pQuoted (sprintf "%f0" f) ;
--				  self#pp_fkind fkin ;
--				  pOption pQuoted os ]
--
--  method private pp_lhost (lh:lhost) : doc = if !E.verboseFlag then trace "pp_lhost" ;
--    match lh with
--    | Var (vinfo) -> text "Var" ++ pParens( self#pp_varinfo vinfo)
--    | Mem (e)     -> text "Mem" ++ pParens( self#pExp () e)
--
--  method private pp_blockinfo (b:block) : doc = if !E.verboseFlag then trace "pp_blockinfo" ;
--    text "Block" ++ (pParens @ pCommaSep) [
--    self#pAttrs () b.battrs ;
--    pList (map (self#pStmt ()) b.bstmts) ]
--
--  method private pp_stmtinfo (sinfo:stmt) : doc = if !E.verboseFlag then trace "pp_stmtinfo" ;
--    text "Stmt" ++ (pParens @ pCommaSep) [
--    pList (map (self#pLabel ()) sinfo.labels) ;
--    self#pStmtKind invalidStmt () sinfo.skind ;
--    text (string_of_int sinfo.sid) ;
--    pList (map self#pp_stmtinfo sinfo.succs) ;
--    pList (map self#pp_stmtinfo sinfo.preds) ]
--end
--
--let ppFile (f:file) (pp:cilPrinter) : doc = if !E.verboseFlag then trace "ppFile" ;
--  text "File" ++ (pParens @ pCommaSep) [ 
--  pQuoted f.fileName ;
--  pList (map (pp#pGlobal ()) f.globals) ]
--
--(* we need a different more flexible mapGlobals
--   we only visit globals and not global init;
--   use mapGlobinits *)
--let mapGlobals2 (fl: file) 
--                (doone: global -> 'a) : 'a list = 
--  List.map doone fl.globals
--
--(* We redefine dumpFile because we don't want a header in our
--   file telling us it was generated with CIL blabla *)
--let dumpFile (pp: cilPrinter) (out : out_channel) file =
--  printDepth := 99999;  
--  Pretty.fastMode := true;
--  if !E.verboseFlag then ignore (E.log "printing file %s\n" file.fileName);
--  let file_doc = ppFile file pp in
--  fprint out 80 file_doc;
--  flush out
--
--let feature : featureDescr =
--  { fd_name = "printaterm";
--    fd_enabled = ref false;
--    fd_description = "printing the current CIL AST to an ATerm";
--    fd_extraopt = [("--atermfile", Arg.String (fun s -> outputfilename := s), "=<filename>: writes the ATerm to <filename>");];
--    fd_doit = (function (f: file) ->        
--        let channel = open_out !outputfilename in 
--        let printer = new atermPrinter
--	in dumpFile printer channel f
--         ; close_out channel
--    );
--    fd_post_check = false;
--  }
-diff -urN cil/src/maincil.ml cil.orig/src/maincil.ml
---- cil/src/maincil.ml	2006-01-16 10:37:24.000000000 +0100
-+++ cil.orig/src/maincil.ml	2005-11-22 06:34:41.000000000 +0100
-@@ -105,7 +105,6 @@
+diff -urN cil.orig/src/ext/atermprinter.ml cil/src/ext/atermprinter.ml
+--- cil.orig/src/ext/atermprinter.ml	1970-01-01 01:00:00.000000000 +0100
++++ cil/src/ext/atermprinter.ml	2006-01-16 10:36:29.000000000 +0100
+@@ -0,0 +1,489 @@
++open Cil
++open Pretty
++open List
++open String
++open Printf
++module S = String 
++module E = Errormsg
++module H = Hashtbl
++module IH = Inthash
++
++let outputfilename = ref "cil.aterm"
++let trace p = eprintf "%s" (p ^ "\n") ; flush stderr
++let invalidStmt = mkStmt (Instr [])
++let id = fun x -> x 
++let compose f g x = (f (g x))
++let (@) = compose
++let pSpace            = text " "
++let foldl1 op ls      = match ls with
++			| (x::xs) -> fold_left op x xs
++                        | _       -> raise (Invalid_argument "foldl1 should not take an empty list")
++let pPacked d l r     = l ++ d ++ r
++let pParens d         = pPacked d (text "(") (text ")")
++let pBraced d         = pPacked d (text "{") (text "}")
++let pSquared d        = pPacked d (text "[") (text "]")
++let pSpaced d         = pPacked d pSpace pSpace
++let pBool b           = (pSpaced @ text @ S.capitalize @ string_of_bool) b
++let pInt64 i          = text (Int64.to_string i)
++let pSeqSep sep xs    = match xs with
++			| [] -> nil
++                        | _  -> foldl1 (pPacked sep) xs
++let pCommaSep xs      = pSeqSep (text ",") xs
++let pPair (a,b)       = (pSpaced @ pParens @ pCommaSep) [a;b]
++let pTriplet (a,b,c)  = (pSpaced @ pParens @ pCommaSep) [a;b;c]
++let pSemiColSep xs    = pSeqSep (text ";") xs
++let pTriple f g h (a,b,c) = (f a, g b, h c)
++let pDouble f g (a,b) = (f a, g b)
++let pOption p m  = match m with
++	         | None   -> text "None()"
++                 | Some v -> text "Some" ++ pParens( p v )
++let pSpParens = pSpaced @ pParens
++let pQuoted str = pPacked (text(escaped str)) (text "\"") (text "\"")
++let pList   = pSpaced @ pSquared @ pCommaSep
++let pRecord = pSpaced @ pBraced  @ pCommaSep
++
++class atermPrinter : cilPrinter  = 
++object (self)
++  inherit defaultCilPrinterClass
++
++  (* printing variable declarations; just store the varinfo *)
++  method pVDecl () (vinfo:varinfo) : doc = if !E.verboseFlag then trace "pVDecl"
++                                         ; self#pp_varinfo vinfo
++  (* printing variable uses; same as declarations; store the varinfo *)
++  method pVar (vinfo:varinfo) : doc = if !E.verboseFlag then trace "pVar" ;
++    self#pp_varinfo vinfo
++
++  method pLval () ((lh, off):lval) : doc = if !E.verboseFlag then trace "pLvalue" ;
++    text "Lvalue" ++ (pParens @ pCommaSep) [ self#pp_lhost lh ; self#pOffset nil off ] 
++
++  (** we are not using the first argument which represents the base from which we are
++      offsetting, because we just want to generate a tree view of the CIL tree. For a tree view
++      this base case is not necessary **)
++  method pOffset (d:doc) (o:offset) : doc = if !E.verboseFlag then trace "pOffset" ;
++    match o with
++    | NoOffset           -> text "Offset_NoOffset() "
++    | Field (finfo, off) -> text "Offset_Field" ++ (pParens @ pCommaSep) [ (self#pFieldDecl ()) finfo ; self#pOffset nil off ]
++    | Index (e, off)     -> text "Offset_Index" ++ (pParens @ pCommaSep) [ self#pExp () e ; self#pOffset nil off ]
++  
++  (*** INSTRUCTIONS ***)
++  method pInstr () (i:instr) : doc = if !E.verboseFlag then trace "pInstr" ;
++    match i with
++    | Set (lv,e,l) -> text "Set" ++ (pParens @ pCommaSep) [ 
++	self#pLval () lv ;
++	self#pExp () e ;
++	self#pp_location l ]
++    | Call (olv,e, elst, l) -> text "Call" ++ (pParens @ pCommaSep) [
++	pOption (self#pLval ()) olv ;
++	self#pExp () e ;
++	pList (map (self#pExp ()) elst) ;
++	self#pp_location l]
++    | Asm (attr, slst1, slvlst, selst, slst2, l) -> text "Asm" ++ (pParens @ pCommaSep) [
++	self#pAttrs () attr ;
++	(pList  @ map pQuoted) slst1 ;
++	pList (map (pPair @ pDouble pQuoted (self#pLval ())) slvlst) ;
++	pList (map (pPair @ pDouble pQuoted (self#pExp ())) selst) ;
++	(pList  @ map pQuoted) slst2 ;
++	self#pp_location l]
++
++  (* a statement itself is just a record of info about the statement
++     the different kinds of statements can be found at pStmtKind *) 
++  method pStmt () (s:stmt) : doc = if !E.verboseFlag then trace "pStmt" ;
++    self#pp_stmtinfo s
++  method dStmt (out:out_channel) (i:int) (s:stmt) : unit = fprint out i (self#pStmt () s)
++
++  (* a block is just a record of info about the block of interest.
++     the real block is a stmtkind (see pStmtKind) *)
++  method dBlock (out:out_channel) (i:int) (b:block) : unit = fprint out i (self#pBlock () b)
++  method pBlock () (b:block) : doc = if !E.verboseFlag then trace "pBlock" ;
++    self#pp_blockinfo b
++
++  (*** GLOBALS ***)
++  method pGlobal () (g:global) : doc = if !E.verboseFlag then trace "pGlobal" ;      (* global (vars, types, etc.) *)
++    match g with 
++    | GType        (typ , l) -> text "GlobalType" ++ (pParens @ pCommaSep) [ self#pp_typeinfo typ ; self#pp_location l ]
++    | GCompTag     (comp, l) -> text "GlobalCompTag" ++ (pParens @ pCommaSep) [ self#pp_compinfo comp ; self#pp_location l ]
++    | GCompTagDecl (comp, l) -> text "GlobalCompTagDecl" ++ (pParens @ pCommaSep) [ self#pp_compinfo comp ; self#pp_location l ]
++    | GEnumTag     (enum, l) -> text "GlobalEnumTag" ++ (pParens @ pCommaSep) [ self#pp_enuminfo enum ; self#pp_location l ]
++    | GEnumTagDecl (enum, l) -> text "GlobalEnumTagDecl" ++ (pParens @ pCommaSep) [ self#pp_enuminfo enum ; self#pp_location l ]
++    | GVarDecl     (vinf, l) -> text "GlobalVarDecl" ++ (pParens @ pCommaSep) [ self#pp_varinfo vinf ; self#pp_location l ]
++    | GVar   (vinf, iinf, l) -> text "GlobalVar" ++ (pParens @ pCommaSep) [ self#pp_varinfo vinf ; self#pp_initinfo iinf ; self#pp_location l ]
++    | GFun         (fdec, l) -> text "GlobalFun" ++ (pParens @ pCommaSep) [ self#pp_fundec fdec ; self#pp_location l ]
++    | GAsm         (str , l) -> text "GlobalAsm"  ++ (pParens @ pCommaSep) [ pQuoted str ; self#pp_location l ]
++    | GPragma      (attr, l) -> text "GlobalPragma" ++ (pParens @ pCommaSep) [ (fun (doc1, bool1) -> doc1) (self#pAttr attr)
++                                                        ; self#pp_location l
++                                        ]
++    | GText str -> text "GlobalText" ++ pParens( pQuoted str)
++  method dGlobal (out:out_channel) (g:global) : unit = fprint out 80 (self#pGlobal () g)
++
++  (* a fielddecl is just a record containing info about the decl *)
++  method pFieldDecl () : fieldinfo -> doc = if !E.verboseFlag then trace "pFieldDecl" ;
++    self#pp_fieldinfo
++
++  (*** TYPES ***)
++  method pType (nameOpt: doc option) (* Whether we are declaring a name or 
++                                      * we are just printing a type *)
++               () (t:typ) =  if !E.verboseFlag then trace "pType" ;     (* use of some type *)
++    match t with
++    | TVoid  attr         -> text "TVoid" ++ pParens( self#pAttrs () attr)
++    | TInt   (ikin, attr) -> text "TInt" ++ (pParens @ pCommaSep) [ self#pp_ikind ikin ; self#pAttrs () attr ]
++    | TFloat (fkin, attr) -> text "TFloat" ++ (pParens @ pCommaSep) [ self#pp_fkind fkin ; self#pAttrs () attr ]
++    | TPtr   (t   , attr) -> text "TPtr" ++ (pParens @ pCommaSep) [ self#pType None () t ; self#pAttrs () attr ]
++    | TArray (t, e, attr) -> text "TArray" ++ (pParens @ pCommaSep) [ self#pType None () t ;
++	pOption (self#pExp ()) e ; self#pAttrs () attr ]
++    | TFun (t, olst, b, attr) -> text "TFun" ++ (pParens @ pCommaSep) [ 
++        self#pType None () t ;
++	pOption (pList @ (map ( pTriplet
++                              @ (pTriple (pQuoted) (self#pType None ()) (self#pAttrs ()))
++                              )     
++                         )
++                )
++                olst ;
++	pBool b ;
++	self#pAttrs () attr]
++    | TNamed (tinfo, attr) -> text "TNamed" ++ (pParens @ pCommaSep) [ self#pp_typeinfo tinfo ; self#pAttrs () attr ]
++    | TComp  (cinfo, attr) -> text "TComp" ++ (pParens @ pCommaSep) [ (text @ string_of_int) cinfo.ckey ;
++                                                           self#pAttrs () attr]
++    | TEnum  (einfo, attr) -> text "TEnum" ++ (pParens @ pCommaSep) [ self#pp_enuminfo einfo ; self#pAttrs () attr ]
++    | TBuiltin_va_list (attr) -> text "TBuiltin_va_list" ++ pParens( self#pAttrs () attr)
++  
++  (*** ATTRIBUTES ***)
++  method pAttr (Attr(an, args) : attribute) : (doc * bool) = if !E.verboseFlag then trace "pAttr" ;
++    ( text "Attr" ++ (pParens @ pCommaSep) [ pQuoted an ; pList (map (self#pAttrParam ()) args) ]
++    , false
++    )
++
++  method pAttrParam () (p:attrparam) : doc = if !E.verboseFlag then trace "pAttrParam" ;
++    match p with
++    | AInt      (i)               -> text "AInt" ++ pParens( pQuoted (string_of_int i))
++    | AStr      (s)               -> text "AStr" ++ pParens( pQuoted s)
++    | ACons     (s, args)         -> text "ACons" ++ (pParens @ pCommaSep) [ pQuoted s ; pList (map (self#pAttrParam ()) args) ]
++    | ASizeOf   (t)               -> text "ASizeOf" ++ pParens( self#pType None () t)
++    | ASizeOfE  (arg)             -> text "ASizeOfE" ++ pParens( self#pAttrParam () arg)
++    | ASizeOfS  (tsig)            -> text "ASizeOfS" ++ pParens( self#pp_typsig tsig)
++    | AAlignOf  (t)               -> text "AAlignOf" ++ pParens( self#pType None () t)
++    | AAlignOfE (arg)             -> text "AAlignOfE" ++ pParens( self#pAttrParam () arg)
++    | AAlignOfS (tsig)            -> text "AAlignOfS" ++ pParens( self#pp_typsig tsig)
++    | AUnOp     (uop, arg)        -> text "AUnOp" ++ (pParens @ pCommaSep) [ self#pp_unop uop ; self#pAttrParam () arg ]
++    | ABinOp    (bop, arg1, arg2) -> text "ABinOp" ++ (pParens @ pCommaSep) [ self#pp_binop bop 
++                                                                ; self#pAttrParam () arg1
++                                                                ; self#pAttrParam () arg2 ]
++    | ADot      (arg, s)          -> text "ADot" ++ (pParens @ pCommaSep) [ self#pAttrParam () arg ; pQuoted s]
++
++  method pAttrs () (attr:attributes) : doc = if !E.verboseFlag then trace "pAttrs" ;
++    text "Attributes" ++ pParens( 
++               pList (map (fst @ self#pAttr) attr)
++              )
++  
++  (*** LABELS ***)
++  method pLabel () (l:label) : doc = if !E.verboseFlag then trace "pLabel" ;
++    match l with
++    | Label   (s,l,b) -> text "Label" ++ (pParens @ pCommaSep) [
++	pQuoted s ;
++	self#pp_location l ;
++	pBool b ]
++    | Case    (e,l)   -> text "Case" ++ (pParens @ pCommaSep) [ 
++	self#pExp () e ;
++	self#pp_location l ]
++    | Default (l)     -> text "Default" ++ pParens( self#pp_location l)
++
++  (*** printing out locations as line directives is not necessary
++       because we are printing the tree structure and locations are
++       present everywhere ***)
++  method pLineDirective : ?forcefile:bool -> location -> doc = fun ?forcefile _ -> nil
++
++  (*** STATEMENT KINDS ***)
++  method pStmtKind s () (sk:stmtkind) : doc = if !E.verboseFlag then trace "pStmtKind" ;
++    match sk with
++    | Instr      (ilst)          -> text "Instr" ++ pParens( pList (map (self#pInstr ()) ilst))
++    | Return     (oe, l)         -> text "Return" ++ (pParens @ pCommaSep) [ pOption (self#pExp ()) oe ; self#pp_location l ]
++    | Goto       (stmtref, l)    -> text "Goto" ++ (pParens @ pCommaSep) [ self#pStmt () !stmtref ; self#pp_location l ]
++    | Break      (l)             -> text "Break" ++ pParens( self#pp_location l)
++    | Continue   (l)             -> text "Continue" ++ pParens( self#pp_location l)
++    | If         (e, b1, b2, l)  -> text "If" ++ (pParens @ pCommaSep) [ 
++	self#pExp () e ;
++	self#pBlock () b1 ;
++	self#pBlock () b2 ;
++	self#pp_location l ]
++    | Switch     (e,b,stlst,l)   -> text "Switch" ++ (pParens @ pCommaSep) [ 
++	self#pExp () e ;
++	self#pBlock () b ;
++	pList (map (self#pStmt ()) stlst) ;
++	self#pp_location l ]
++    | Loop       (b,l,os1, os2)  -> text "Loop" ++ (pParens @ pCommaSep) [
++	self#pBlock () b ;
++	self#pp_location l ;
++	pOption (self#pStmt ()) os1 ;
++	pOption (self#pStmt ()) os2 ]
++    | Block      (b)             -> text "Block" ++ pParens( self#pBlock () b)
++    | TryFinally (b1,b2,l)       -> text "TryFinally" ++ (pParens @ pCommaSep) [ 
++	self#pBlock () b1 ;
++	self#pBlock () b2 ;
++	self#pp_location l ]
++    | TryExcept  (b1, pr, b2, l) -> text "TryExcept" ++ (pParens @ pCommaSep) [ 
++	self#pBlock () b1 ;
++	(  pPair
++         @ pDouble (pList @ map (self#pInstr ())) 
++                   (self#pExp ())
++        ) pr ;
++	self#pBlock () b2 ;
++	self#pp_location l ]
++
++  (*** EXPRESSIONS ***)
++
++  method pExp () (e:exp) : doc = if !E.verboseFlag then trace "pExp" ;
++    match e with
++    | Const     (c)              -> text "Constant" ++ pParens( self#pp_constant c)
++    | Lval      (lh,off)         -> text "Lvalue" ++ (pParens @ pCommaSep)  [self#pp_lhost lh ; self#pOffset nil off ]
++    | SizeOf    (t)              -> text "SizeOfType" ++ pParens( self#pType None () t)
++    | SizeOfE   (e)              -> text "SizeOfExp" ++ pParens( self#pExp () e)
++    | SizeOfStr (s)              -> text "SizeOfString" ++ pParens( pQuoted s)
++    | AlignOf   (t)              -> text "AlignOfType" ++ pParens( self#pType None () t)
++    | AlignOfE  (e)              -> text "AlignOfExp" ++ pParens( self#pExp () e)
++    | UnOp      (uop, e, t)      -> text "UnOp" ++ (pParens @ pCommaSep) [ 
++					self#pp_unop uop ; 
++                                        self#pExp () e ; 
++	                                self#pType None () t ]
++    | BinOp     (bop, e1, e2, t) -> text "BinOp" ++ (pParens @ pCommaSep) [ 
++                                        self#pp_binop bop ;
++                                        self#pExp () e1 ;
++                                        self#pExp () e2 ;
++                                        self#pType None () t ]
++    | CastE     (t,e)            -> text "Cast" ++ (pParens @ pCommaSep) [ self#pType None () t ; self#pExp () e]
++    | AddrOf    (lv)             -> text "AddressOf" ++ pParens( self#pLval () lv)
++    | StartOf   (lv)             -> text "StartOf" ++ pParens( self#pLval () lv)
++
++  (*** INITIALIZERS ***)
++  method pInit () (i:init) : doc = if !E.verboseFlag then trace "pInit" ;
++    match i with
++    | SingleInit   (e)        -> text "SingleInit" ++ pParens( self#pExp () e)
++    | CompoundInit (t, oilst) -> text "CompoundInit" ++ (pParens @ pCommaSep) [ self#pType None () t ;
++				    pList (map (  pPair
++			                        @ pDouble (self#pOffset nil) (self#pInit ())
++			                       ) 
++			                       oilst
++			                  ) ]
++  method dInit (out:out_channel) (i:int) (init1:init) : unit = fprint out i (self#pInit () init1)
++
++  (*** auxiliary methods ***)
++  (* Mart: hmmmm *)
++  method private pp_storage (s:storage) : doc =
++    let tok = match s with
++	      | NoStorage -> "NoStorage"
++	      | Static    -> "Static"
++	      | Register  -> "Register"
++	      | Extern	  -> "Extern"
++    in pQuoted ("Storage" ^ tok)
++
++  method private pp_typeinfo (tinfo:typeinfo) : doc = if !E.verboseFlag then trace "pp_typeinfo" ;
++    text "Typeinfo" ++ (pParens @ pCommaSep) [   
++    pQuoted tinfo.tname ;
++    self#pType None () tinfo.ttype ;
++    pBool tinfo.treferenced ]
++
++  method private pp_fieldinfo (finfo:fieldinfo) : doc = if !E.verboseFlag then trace "pp_fieldinfo" ;
++    text "Fieldinfo" ++ (pParens @ pCommaSep) [ 
++    pQuoted finfo.fname ;
++    self#pType None () finfo.ftype ;
++    pOption (pQuoted @ string_of_int) finfo.fbitfield ;
++    self#pAttrs () finfo.fattr ;
++    self#pp_location finfo.floc ]
++
++  method private pp_compinfo (cinfo:compinfo) : doc = if !E.verboseFlag then trace "pp_compinfo" ;
++    text "Compinfo" ++ (pParens @ pCommaSep) [ 
++    pBool cinfo.cstruct ;
++    pQuoted cinfo.cname ;
++    text (string_of_int cinfo.ckey) ;
++    pList (map (self#pFieldDecl ()) cinfo.cfields) ;
++    self#pAttrs () cinfo.cattr ;
++    pBool cinfo.cdefined ;
++    pBool cinfo.creferenced ]
++
++  method private pp_enuminfo (einfo:enuminfo) : doc = if !E.verboseFlag then trace "pp_enuminfo" ;
++    text "Enuminfo" ++ (pParens @ pCommaSep) [
++    pQuoted einfo.ename ;
++    pList (map (  pTriplet
++                @ (pTriple pQuoted (self#pExp ()) self#pp_location)
++               )
++               einfo.eitems) ;
++    self#pAttrs () einfo.eattr ;
++    pBool einfo.ereferenced ]
++
++  method private pp_location (loc:location) : doc = if !E.verboseFlag then trace "pp_location" ;
++    text "Location" ++ (pParens @ pCommaSep) [
++    text (string_of_int loc.line) ;
++    pQuoted loc.file ;
++    text (string_of_int loc.byte) ]
++
++  method private pp_varinfo (vinfo:varinfo) : doc = if !E.verboseFlag then trace "pp_varinfo" ;
++    text "Varinfo" ++ (pParens @ pCommaSep) [
++    pQuoted vinfo.vname ;
++    self#pType None () vinfo.vtype ;
++    self#pAttrs () vinfo.vattr ;
++    self#pp_storage vinfo.vstorage ;
++    pBool vinfo.vglob ;
++    pBool vinfo.vinline ;
++    self#pp_location vinfo.vdecl ;
++    text (string_of_int vinfo.vid) ;
++    pBool vinfo.vaddrof ;
++    pBool vinfo.vreferenced ]
++
++  method private pp_initinfo (iinfo:initinfo) : doc = if !E.verboseFlag then trace "pp_initinfo" ;
++    text "Initinfo" ++ pParens( 
++    pOption (self#pInit ()) iinfo.init)
++
++  method private pp_fundec (fdec:fundec) : doc = if !E.verboseFlag then trace "pp_fundec" ;
++    text "Fundec" ++ (pParens @ pCommaSep) [
++    self#pp_varinfo fdec.svar ;
++    pList (map self#pp_varinfo fdec.sformals) ;
++    pList (map self#pp_varinfo fdec.slocals) ;
++    text (string_of_int fdec.smaxid) ;
++    self#pBlock () fdec.sbody ;
++    pOption (pSpParens @ text @ string_of_int) fdec.smaxstmtid ;
++    pList (map (self#pStmt ()) fdec.sallstmts) ]
++
++  method private pp_ikind (ikin:ikind) : doc =
++    let tok = match ikin with
++              | IChar  -> "IChar"
++	      | ISChar -> "ISChar"
++	      | IUChar -> "IUChar"
++	      | IInt   -> "IInt"
++	      | IUInt  -> "IUInt"
++	      | IShort -> "IShort"
++	      | IUShort -> "IUShort"
++	      | ILong  -> "ILong"
++	      | IULong -> "IULong"
++	      | ILongLong -> "ILongLong"
++	      | IULongLong -> "IULongLong"
++    in  pQuoted ("Ikind" ^ tok)
++
++  method private pp_fkind (fkin:fkind) : doc =
++    let tok = match fkin with
++	      | FFloat -> "FFloat"
++	      | FDouble -> "FDouble"
++	      | FLongDouble -> "FLongDouble"
++    in pQuoted ("Fkind" ^ tok)
++
++  method private pp_typsig (tsig:typsig) : doc = if !E.verboseFlag then trace "pp_typsig" ;
++    match tsig with
++    | TSArray (tsig2, oe, attr)         -> text "TSArray" ++ (pParens @ pCommaSep) [
++					      self#pp_typsig tsig2 ;
++					      pOption pInt64 oe ;
++					      self#pAttrs () attr ]
++    | TSPtr   (tsig2, attr)             -> text "TSPtr" ++ (pParens @ pCommaSep) [
++					      self#pp_typsig tsig2 ;
++					      self#pAttrs () attr ]	
++    | TSComp  (b, s, attr)              -> text "TSComp" ++ (pParens @ pCommaSep) [
++					      pBool b ;
++					      pQuoted s ;
++					      self#pAttrs () attr ]
++    | TSFun   (tsig2, tsiglst, b, attr) -> text "TSFun" ++ (pParens @ pCommaSep) [
++					      self#pp_typsig tsig2 ;
++					      pList (map self#pp_typsig tsiglst) ;
++					      pBool b ;
++					      self#pAttrs () attr ]
++    | TSEnum  (s, attr)                 -> text "TSEnum" ++ (pParens @ pCommaSep) [
++					      pQuoted s ;
++					      self#pAttrs () attr ]
++    | TSBase  (t)                       -> text "TSBase" ++ pParens( self#pType None () t)
++     
++
++  method private pp_unop (uop:unop) : doc =
++    let tok = match uop with
++	      | Neg -> "Neg"
++	      | BNot -> "BNot"
++	      | LNot -> "LNot"
++    in pQuoted ("UnOp" ^ tok)
++
++  method private pp_binop (bop:binop) : doc = 
++    let tok = match bop with
++              | PlusA -> "PlusA"
++	      | PlusPI -> "PlusPI"
++	      | IndexPI -> "IndexPI"
++	      | MinusA -> "MinusA"
++	      | MinusPI -> "MinusPI"
++	      | MinusPP -> "MinusPP"
++	      | Mult -> "Mult"
++	      | Div -> "Div"
++	      | Mod -> "Mod"
++	      | Shiftlt -> "Shiftlt"
++	      | Shiftrt -> "Shiftrt"
++	      | Lt -> "Lt"
++	      | Gt -> "Gt"
++	      | Le -> "Le"
++	      | Ge -> "Ge"
++	      | Eq -> "Eq"
++	      | Ne -> "Ne"
++	      | BAnd -> "BAnd"
++	      | BXor -> "BXor"
++	      | BOr -> "BOr"
++	      | LAnd -> "LAnd"
++	      | LOr -> "LOr"
++    in pQuoted ("BinOp" ^ tok )
++
++  method private pp_constant (c:constant) : doc = if !E.verboseFlag then trace "pp_constant" ;
++    match c with
++    | CInt64 (i, ikin, os) -> text "CInt64" ++ (pParens @ pCommaSep) [  
++                                  pQuoted (Int64.to_string i)  ;
++				  self#pp_ikind ikin ;
++				  pOption pQuoted os ]
++    | CStr   (s)           -> text "CStr" ++ pParens( pQuoted s)
++    | CWStr  (ilist)       -> text "CWStr" ++ pParens( pList (map ( text @ Int64.to_string) ilist))
++    | CChr   (c)           -> text "CChr" ++ pParens( text "\"" ++ text (Char.escaped c) ++ text "\"")
++    | CReal  (f, fkin, os) -> text "CReal" ++ (pParens @ pCommaSep) [  pQuoted (sprintf "%f0" f) ;
++				  self#pp_fkind fkin ;
++				  pOption pQuoted os ]
++
++  method private pp_lhost (lh:lhost) : doc = if !E.verboseFlag then trace "pp_lhost" ;
++    match lh with
++    | Var (vinfo) -> text "Var" ++ pParens( self#pp_varinfo vinfo)
++    | Mem (e)     -> text "Mem" ++ pParens( self#pExp () e)
++
++  method private pp_blockinfo (b:block) : doc = if !E.verboseFlag then trace "pp_blockinfo" ;
++    text "Block" ++ (pParens @ pCommaSep) [
++    self#pAttrs () b.battrs ;
++    pList (map (self#pStmt ()) b.bstmts) ]
++
++  method private pp_stmtinfo (sinfo:stmt) : doc = if !E.verboseFlag then trace "pp_stmtinfo" ;
++    text "Stmt" ++ (pParens @ pCommaSep) [
++    pList (map (self#pLabel ()) sinfo.labels) ;
++    self#pStmtKind invalidStmt () sinfo.skind ;
++    text (string_of_int sinfo.sid) ;
++    pList (map self#pp_stmtinfo sinfo.succs) ;
++    pList (map self#pp_stmtinfo sinfo.preds) ]
++end
++
++let ppFile (f:file) (pp:cilPrinter) : doc = if !E.verboseFlag then trace "ppFile" ;
++  text "File" ++ (pParens @ pCommaSep) [ 
++  pQuoted f.fileName ;
++  pList (map (pp#pGlobal ()) f.globals) ]
++
++(* we need a different more flexible mapGlobals
++   we only visit globals and not global init;
++   use mapGlobinits *)
++let mapGlobals2 (fl: file) 
++                (doone: global -> 'a) : 'a list = 
++  List.map doone fl.globals
++
++(* We redefine dumpFile because we don't want a header in our
++   file telling us it was generated with CIL blabla *)
++let dumpFile (pp: cilPrinter) (out : out_channel) file =
++  printDepth := 99999;  
++  Pretty.fastMode := true;
++  if !E.verboseFlag then ignore (E.log "printing file %s\n" file.fileName);
++  let file_doc = ppFile file pp in
++  fprint out 80 file_doc;
++  flush out
++
++let feature : featureDescr =
++  { fd_name = "printaterm";
++    fd_enabled = ref false;
++    fd_description = "printing the current CIL AST to an ATerm";
++    fd_extraopt = [("--atermfile", Arg.String (fun s -> outputfilename := s), "=<filename>: writes the ATerm to <filename>");];
++    fd_doit = (function (f: file) ->        
++        let channel = open_out !outputfilename in 
++        let printer = new atermPrinter
++	in dumpFile printer channel f
++         ; close_out channel
++    );
++    fd_post_check = false;
++  }
+diff -urN cil.orig/src/maincil.ml cil/src/maincil.ml
+--- cil.orig/src/maincil.ml	2005-11-22 06:34:41.000000000 +0100
++++ cil/src/maincil.ml	2006-01-16 10:37:24.000000000 +0100
+@@ -105,6 +105,7 @@
      Simplemem.feature;
      Simplify.feature;
      Dataslicing.feature;
--    Atermprinter.feature;
++    Atermprinter.feature;
    ] 
    @ Feature_config.features