diff options
author | Mart Kolthof <skolthof@cs.uu.nl> | 2006-01-02 14:24:36 +0000 |
---|---|---|
committer | Mart Kolthof <skolthof@cs.uu.nl> | 2006-01-02 14:24:36 +0000 |
commit | 0ab104df8d546ce150f33c023b202dd33cc863db (patch) | |
tree | 0d21ecb2bad997f1b155abfd95d0416ec8e60fbf /pkgs/development/libraries/cil-aterm | |
parent | 6d5762168dfa1b965b4fdaeb70895a2f38e58deb (diff) |
added cil-aterm to nixpkgs
svn path=/nixpkgs/trunk/; revision=4482
Diffstat (limited to 'pkgs/development/libraries/cil-aterm')
-rw-r--r-- | pkgs/development/libraries/cil-aterm/atermprinter.patch | 515 | ||||
-rw-r--r-- | pkgs/development/libraries/cil-aterm/default.nix | 11 |
2 files changed, 526 insertions, 0 deletions
diff --git a/pkgs/development/libraries/cil-aterm/atermprinter.patch b/pkgs/development/libraries/cil-aterm/atermprinter.patch new file mode 100644 index 0000000000000..16761898e1939 --- /dev/null +++ b/pkgs/development/libraries/cil-aterm/atermprinter.patch @@ -0,0 +1,515 @@ +diff -urN cil.orig/Makefile.cil.in cil/Makefile.cil.in +--- cil.orig/Makefile.cil.in 2005-06-01 14:37:13.000000000 +0200 ++++ cil/Makefile.cil.in 2005-11-21 10:45:48.000000000 +0100 +@@ -75,6 +75,7 @@ + canonicalize heap oneret partial simplemem simplify \ + dataslicing \ + testcil \ ++ atermprinter \ + $(CILLY_FEATURES) \ + feature_config + # ww: we don't want "maincil" in an external cil library (cil.cma), +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 2005-11-21 11:14:44.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-06-01 14:37:13.000000000 +0200 ++++ cil/src/maincil.ml 2005-11-21 10:45:34.000000000 +0100 +@@ -105,6 +105,7 @@ + Simplemem.feature; + Simplify.feature; + Dataslicing.feature; ++ Atermprinter.feature; + ] + @ Feature_config.features + diff --git a/pkgs/development/libraries/cil-aterm/default.nix b/pkgs/development/libraries/cil-aterm/default.nix new file mode 100644 index 0000000000000..0fc5564a5f4a9 --- /dev/null +++ b/pkgs/development/libraries/cil-aterm/default.nix @@ -0,0 +1,11 @@ +{ stdenv, fetchurl, ocaml, perl }: + +stdenv.mkDerivation { + name = "cil-aterm-1.3.3"; + src = fetchurl { + url = http://manju.cs.berkeley.edu/cil/distrib/cil-1.3.3.tar.gz; + md5 = "dafd350c154990728efb35a7073ca81a"; + }; + patches = [./atermprinter.patch]; + inherit ocaml perl; +} |