cil (empty) → 0.0.0

raw patch · 6 files changed

+168/−0 lines, 6 filesdep +basedep +polyparsesetup-changed

Dependencies added: base, polyparse

Files

LICENSE +27/−0
Language/CIL.hs +20/−0
Setup.lhs +8/−0
cil.cabal +43/−0
dumpcil/Makefile +11/−0
dumpcil/dump_cil.ml +59/−0

+ LICENSE view

@@ -0,0 +1,27 @@+Copyright (c) Tom Hawkins 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.

+ Language/CIL.hs view

@@ -0,0 +1,20 @@+{- Generated by DrIFT (Automatic class derivations for Haskell) -}+{-# LINE 1 "Language/CIL.DrIFT.hs" #-}+module Language.CIL+  ( File (..)+  )+  where++import Text.Parse++data File = File String+  deriving Show {-!derive : Parse !-}+++{-* Generated by DrIFT : Look, but Don't Touch. *-}+instance Parse File where+    parse = constructors+	[ ( "File" , fmap File parse )+	]++--  Imported from other files :-

+ Setup.lhs view

@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain

+ cil.cabal view

@@ -0,0 +1,43 @@+name:    cil+version: 0.0.0++category: Language++synopsis: An interface to CIL and ACSL through Frama-C.++description:+  TODO++author:     Tom Hawkins <tomahawkins@gmail.com>+maintainer: Tom Hawkins <tomahawkins@gmail.com>++license:      BSD3+license-file: LICENSE++homepage: http://tomahawkins.org++build-type:    Simple+cabal-version: >= 1.6++extra-source-files:+  dumpcil/dump_cil.ml+  dumpcil/Makefile++library+    build-depends:+        base       >= 4.0 && < 5.0,+        polyparse  >= 1.4++    exposed-modules:+        Language.CIL++    extensions: GADTs, EmptyDataDecls++    if impl(ghc > 6.8)+          ghc-options: -fwarn-tabs+    ghc-options:       -W++source-repository head+    type:     git+    location: git://github.com/tomahawkins/cil.git+

+ dumpcil/Makefile view

@@ -0,0 +1,11 @@+FRAMAC_SHARE  :=$(shell frama-c.byte -print-path)+FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)+PLUGIN_NAME = DumpCIL+PLUGIN_CMO  = dump_cil++include $(FRAMAC_SHARE)/Makefile.dynamic++.PHONY:clean-all+clean-all: clean+	-rm -f .depend+	-rm -f $(FRAMAC_LIBDIR)/DumpCIL.*

+ dumpcil/dump_cil.ml view

@@ -0,0 +1,59 @@+open Ast+open Cil_types+open File+open Lexing+open List++let error loc msg = prerr_endline ("ERROR: " ^ msg); exit 1++let unknown =+  { pos_fname = "unknown"+  ; pos_lnum = 0+  ; pos_bol  = 0+  ; pos_cnum = 0+  }++let format_fundec _ _ = "function declaration"++let format_global a = match a with+    GType        (a, loc)    -> "typedef"+  | GCompTag     (a, loc)    -> "struct-union definition"+  | GCompTagDecl (a, loc)    -> "struct-union declaration"+  | GEnumTag     (a, loc)    -> "enum definition"+  | GEnumTagDecl (a, loc)    -> "enum declaration"+  | GVarDecl     (f, v, loc) -> "variable declaration"+  | GVar         (v, i, loc) -> "variable definition"+  | GFun         (a, loc)    -> format_fundec a loc+  | GAsm         (_, loc)    -> error loc "asm not supported"+  | GPragma      (a, loc)    -> ""+  | GText        _           -> "text"+  | GAnnot       _           -> "annot"++let dump file =+  (match file.globinit with+    None   -> ()+  | Some f -> error unknown "initializer not supported");+  iter (fun a -> if String.length a == 0 then () else print_endline a) (map format_global file.globals)++let run () =+  File.init_from_cmdline ();+  dump (Ast.get ())++module Self =+  Plugin.Register+    (struct+      let name = "DumpCIL"+      let shortname = "DumpCIL"+      let descr = "Dumps CIL and ACSL to stdout."+    end);;++module Enabled =+  Self.False+    (struct+      let option_name = "-dumpcil"+      let descr = "Dumps CIL and ACSL to stdout."+    end);;++let () = Db.Main.extend (fun () -> if Enabled.get () then run ())++