536 lines
24 KiB
Diff
536 lines
24 KiB
Diff
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 @@
|
|
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),
|
|
@@ -537,8 +536,6 @@
|
|
|
|
prefix = @prefix@
|
|
exec_prefix = @exec_prefix@
|
|
-bindir = @prefix@/bin
|
|
-objdir = @prefix@/$(OBJDIR)
|
|
libdir = @libdir@
|
|
pkglibdir = $(libdir)/cil
|
|
datadir = @datadir@
|
|
@@ -557,10 +554,6 @@
|
|
$(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)
|
|
|
|
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 @@
|
|
Simplemem.feature;
|
|
Simplify.feature;
|
|
Dataslicing.feature;
|
|
- Atermprinter.feature;
|
|
]
|
|
@ Feature_config.features
|
|
|