7c765159ba
Fixed the CilConfig.pm.in to use the prefix instead of the cilhome, which is for whatever reason set to the pwd. Yeah. These CIL guys could use some deployment help. svn path=/nixpkgs/trunk/; revision=6516
593 lines
26 KiB
Diff
593 lines
26 KiB
Diff
diff -urN cil-old/bin/CilConfig.pm.in cil-new/bin/CilConfig.pm.in
|
|
--- cil-old/bin/CilConfig.pm.in 2005-11-22 06:34:41.000000000 +0100
|
|
+++ cil-new/bin/CilConfig.pm.in 2006-09-13 13:52:44.000000000 +0200
|
|
@@ -1,7 +1,7 @@
|
|
|
|
-use lib "@CILHOME@/lib"; # The libraries are in the lib directory
|
|
+use lib "@prefix@/lib"; # The libraries are in the lib directory
|
|
$::archos = "@ARCHOS@";
|
|
$::cc = "@CC@";
|
|
-$::cilhome = "@CILHOME@";
|
|
+$::cilhome = "@prefix@";
|
|
$::default_mode = "@DEFAULT_CIL_MODE@";
|
|
|
|
diff -urN cil-old/Makefile.cil.in cil-new/Makefile.cil.in
|
|
--- cil-old/Makefile.cil.in 2005-11-22 06:34:41.000000000 +0100
|
|
+++ cil-new/Makefile.cil.in 2006-09-13 13:52:09.000000000 +0200
|
|
@@ -78,6 +78,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),
|
|
@@ -536,6 +537,8 @@
|
|
|
|
prefix = @prefix@
|
|
exec_prefix = @exec_prefix@
|
|
+bindir = @prefix@/bin
|
|
+objdir = @prefix@/$(OBJDIR)
|
|
libdir = @libdir@
|
|
pkglibdir = $(libdir)/cil
|
|
datadir = @datadir@
|
|
@@ -554,6 +557,11 @@
|
|
$(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_DATA) lib/* $(bindir)
|
|
+ $(INSTALL) $(OBJDIR)/*.exe $(objdir)
|
|
|
|
cil.spec: cil.spec.in
|
|
./config.status $@
|
|
diff -urN cil-old/ocamlutil/Makefile.ocaml cil-new/ocamlutil/Makefile.ocaml
|
|
--- cil-old/ocamlutil/Makefile.ocaml 2005-11-22 06:34:41.000000000 +0100
|
|
+++ cil-new/ocamlutil/Makefile.ocaml 2006-09-13 13:52:09.000000000 +0200
|
|
@@ -135,6 +135,7 @@
|
|
|
|
CAMLFLAGS =$(OPT_FLAGS) -I $(OBJDIR)
|
|
|
|
+
|
|
# sm: two styles for echoing compilation progress:
|
|
# style 1, by George:
|
|
# - print English descriptions of what's happening
|
|
@@ -152,20 +153,12 @@
|
|
# $(AT) - put this before shell commands which are to be executed,
|
|
# and also printed in style 2
|
|
# $(ECHO) - use in place of '@' for things not printed in either style
|
|
-ifdef ECHOSTYLE_SCOTT
|
|
- # 'true' silently consumes its arguments, whereas 'echo' prints them
|
|
- NARRATIVE := true
|
|
- COMMAND := echo
|
|
- AT :=
|
|
- ECHO := @
|
|
-else
|
|
- NARRATIVE := echo
|
|
- COMMAND := true
|
|
- # change these next two definitions to <empty> to echo everything,
|
|
- # or leave as @ to suppress echoing
|
|
- AT := @
|
|
- ECHO := @
|
|
-endif
|
|
+
|
|
+# 'true' silently consumes its arguments, whereas 'echo' prints them
|
|
+NARRATIVE := true
|
|
+COMMAND := echo
|
|
+AT :=
|
|
+ECHO := @
|
|
|
|
ifdef PREPROC
|
|
COMPILEFLAGS += -pp "$(PREPROC)$"
|
|
@@ -361,4 +354,4 @@
|
|
endif
|
|
|
|
listmodules:
|
|
- @echo $(MODULES)
|
|
\ No newline at end of file
|
|
+ @echo $(MODULES)
|
|
diff -urN cil-old/src/ext/atermprinter.ml cil-new/src/ext/atermprinter.ml
|
|
--- cil-old/src/ext/atermprinter.ml 1970-01-01 01:00:00.000000000 +0100
|
|
+++ cil-new/src/ext/atermprinter.ml 2006-09-13 13:52:09.000000000 +0200
|
|
@@ -0,0 +1,488 @@
|
|
+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 ***)
|
|
+ method private pp_storage (s:storage) : doc =
|
|
+ let tok = match s with
|
|
+ | NoStorage -> "NoStorage"
|
|
+ | Static -> "Static"
|
|
+ | Register -> "Register"
|
|
+ | Extern -> "Extern"
|
|
+ in text ("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 text ("Ikind_" ^ tok)
|
|
+
|
|
+ method private pp_fkind (fkin:fkind) : doc =
|
|
+ let tok = match fkin with
|
|
+ | FFloat -> "FFloat"
|
|
+ | FDouble -> "FDouble"
|
|
+ | FLongDouble -> "FLongDouble"
|
|
+ in text ("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 text ("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 text ("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-old/src/maincil.ml cil-new/src/maincil.ml
|
|
--- cil-old/src/maincil.ml 2005-11-22 06:34:41.000000000 +0100
|
|
+++ cil-new/src/maincil.ml 2006-09-13 13:52:09.000000000 +0200
|
|
@@ -105,6 +105,7 @@
|
|
Simplemem.feature;
|
|
Simplify.feature;
|
|
Dataslicing.feature;
|
|
+ Atermprinter.feature;
|
|
]
|
|
@ Feature_config.features
|
|
|