From 7bc09b8f2f1d562847116074e59b864080269d4f Mon Sep 17 00:00:00 2001 From: Mart Kolthof Date: Mon, 16 Jan 2006 13:13:43 +0000 Subject: [PATCH] inversed patch svn path=/nixpkgs/trunk/; revision=4560 --- .../libraries/cil-aterm/cil-aterm-1.3.4.patch | 1022 ++++++++--------- 1 file 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), "=: writes the ATerm to ");]; -- 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), "=: writes the ATerm to ");]; ++ 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