diff --git a/GenCIL.hs b/GenCIL.hs
deleted file mode 100644
--- a/GenCIL.hs
+++ /dev/null
@@ -1,400 +0,0 @@
--- | Parses OCaml cil_types.mli file and generates an equivalent CIL.hs file and a supporting Frama-C plugin (-dumpcil).
-module Main (main) where
-
-import Data.Char
-import Data.List hiding (group)
-import System.Process
-import Text.ParserCombinators.Poly.Plain
-import Text.Printf
-
-main :: IO ()
-main = do
- f <- readFile "cil_types.mli"
- writeFile "cil_types_nocomments.mli" $ decomment f
- let types = parseOCaml f
- system "mkdir -p install-dumpcil-plugin"
- writeFile "install-dumpcil-plugin/Makefile" $ dumpcilMakefile
- writeFile "install-dumpcil-plugin/dump_cil.ml" $ dumpcilPlugin types
- writeFile "CIL.hs" $ haskellCIL types
-
-
--- OCaml type types.
-
--- Type definitions.
-data TypeDef
- = Sum [(String, [TypeApply])]
- | Record [(String, TypeApply)]
- | Alias TypeApply
- deriving (Show, Eq)
-
---- Type definition name with parameters.
-data TypeName = TypeName String [String] deriving (Show, Eq)
-
--- Type references. Either type applications or tuples.
-data TypeApply
- = TypeApply VarPar [TypeApply]
- | TypeApplyGroup TypeApply
- deriving (Show, Eq)
-
--- Type variables or parameters.
-data VarPar = Var String | Par String deriving (Show, Eq)
-
-
-
-cap :: String -> String
-cap [] = []
-cap (a:b) = toUpper a : b
-
-isAlias :: TypeDef -> Bool
-isAlias (Alias _) = True
-isAlias _ = False
-
--- Haskell CIL module generation.
-haskellCIL :: [(TypeName, TypeDef)] -> String
-haskellCIL types = unlines
- [ "-- | A Haskell interface to OCaml's CIL library, via Frama-C, providing both a simplied C AST and the ACSL specification language."
- , "module Language.CIL"
- , " ( parseC"
- , " , debugParseC"
- , " , installPlugin"
- , " , Exn (..)"
- , " , Position (..)"
- , " , Int64 (..)"
- , unlines [ printf " , %-26s %s" (cap name) (if isAlias t then "" else "(..)") | (TypeName name _, t) <- types ]
- , " )"
- , " where"
- , ""
- , "import System.Exit"
- , "import System.Process"
- -- , "import Text.Parse"
- , ""
- , "-- | Parse a C compilation unit (file)."
- , "parseC :: FilePath -> IO File"
- , "parseC file = do"
- , " (exitCode, out, err) <- readProcessWithExitCode \"frama-c\" [\"-dumpcil\", file] \"\""
- , " let code = unlines $ tail $ lines out"
- , " case exitCode of"
- , " ExitSuccess -> return $ read code"
- , " ExitFailure _ -> putStrLn err >> exitWith exitCode"
- , ""
- , "-- | Prints output from frama-c -dumpcil."
- , "debugParseC :: FilePath -> IO ()"
- , "debugParseC file = do"
- , " (exitCode, out, err) <- readProcessWithExitCode \"frama-c\" [\"-dumpcil\", file] \"\""
- , " putStrLn out"
- , ""
- -- {-
- -- case exitCode of
- -- ExitSuccess -> case runParser parse code of
- -- (Left s, a) -> putStrLn ("parse error: " ++ s ++ "\n" ++ code ++ "\n" ++ a) >> exitFailure
- -- (Right f, _) -> return f
- -- ExitFailure _ -> putStrLn err >> exitWith exitCode
- -- -}
- , " -- | Installs Frama-C '-dumpcil' plugin. Creates 'install-dumpcil-pluging' directory, deposits a Makefile and dump_cil.ml, then runs 'make' and 'make install'."
- , "installPlugin :: IO ()"
- , "installPlugin = do"
- , " putStrLn \"creating install-dumpcil-plugin directory for plugin compiling and installation ...\""
- , " system \"mkdir -p install-dumpcil-plugin\""
- , " writeFile \"install-dumpcil-plugin/Makefile\" " ++ show dumpcilMakefile
- , " writeFile \"install-dumpcil-plugin/dump_cil.ml\" " ++ show (dumpcilPlugin types)
- , " putStrLn \"running 'make' to compile dumpcil plugin ...\""
- , " system \"cd install-dumpcil-plugin && make\""
- , " putStrLn \"running 'make install' to install dumpcil plugin ...\""
- , " system \"cd install-dumpcil-plugin && make install\""
- , " return ()"
- , ""
- , "data Exn = Exn " ++ derives
- , "data Position = Position FilePath Int Int " ++ derives
- , "data Int64 = Int64 " ++ derives
- , ""
- , unlines [ printf "%s %s %s = %s %s" (if isAlias t then "type" else "data") (cap name) (intercalate " " params) (fType name t) (if isAlias t then "" else derives) | (TypeName name params, t) <- types ]
- ]
- where
- derives = "deriving (Show, Read, Eq) {-! derive : Parse !-}"
- fType :: String -> TypeDef -> String
- fType name t = case t of
- Sum constructors -> intercalate " | " [ constructorName name ++ concat [ " " ++ group (fTypeApply t) | t <- args ] | (name, args) <- constructors ]
- Record fields -> printf "%s { %s }" (cap name) $ intercalate ", " [ printf "%s :: %s" field (fTypeApply tr) | (field, tr) <- fields ]
- Alias tr -> fTypeApply tr
-
- fTypeApply :: TypeApply -> String
- fTypeApply a = case a of
- TypeApply a [] -> name a
- TypeApply (Var "list") [a] -> "[" ++ fTypeApply a ++ "]"
- TypeApply (Var "option") [a] -> "Maybe " ++ group (fTypeApply a)
- TypeApply (Var "ref") [a] -> fTypeApply a
- TypeApply (Var "tuple") args -> group $ intercalate ", " (map fTypeApply args)
- TypeApply a args -> name a ++ concat [ " (" ++ fTypeApply t ++ ")" | t <- args ]
- TypeApplyGroup a -> fTypeApply a
- where
- name (Var n) = cap n
- name (Par n) = n
-
-constructorName :: String -> String
-constructorName a = case a of
- "Block" -> "Block'"
- "True" -> "True'"
- "False" -> "False'"
- "Nothing" -> "Nothing'"
- a -> cap a
-
-
--- Frama-C 'dumpcil' plugin generation.
-dumpcilPlugin :: [(TypeName, TypeDef)] -> String
-dumpcilPlugin types = unlines
- [ "open Ast"
- , "open Cil_types"
- , "open File"
- , "open Lexing"
- , "open List"
- , "open String"
- , "open Int64"
- , "open Char"
- , ""
- , "let string a = \"\\\"\" ^ a ^ \"\\\"\" (* XXX Doesn't handle '\\' or '\"' chars in string. *)"
- , "let position t = \"Position \\\"\" ^ t.pos_fname ^ \"\\\" \" ^ string_of_int t.pos_lnum ^ \" \" ^ string_of_int (t.pos_cnum - t.pos_bol + 1)"
- , "let bool a = if a then \"True\" else \"False\""
- , "let char = Char.escaped"
- , "let int = string_of_int"
- , "let int64 = Int64.to_string"
- , "let float = string_of_float"
- , ""
- , "let rec " ++ intercalate "\nand " (map fType types)
- , ""
- , "let run () ="
- , " File.init_from_cmdline ();"
- , " print_endline (file (Ast.get ()))"
- , ""
- , "module Self ="
- , " Plugin.Register"
- , " (struct"
- , " let name = \"dumpcil\""
- , " let shortname = \"dumpcil\""
- , " let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\""
- , " end);;"
- , ""
- , "module Enabled ="
- , " Self.False"
- , " (struct"
- , " let option_name = \"-dumpcil\""
- , " let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\""
- , " end);;"
- , ""
- , "let () = Db.Main.extend (fun () -> if Enabled.get () then run ())"
- ]
- where
- fType :: (TypeName, TypeDef) -> String
- fType (TypeName name args, m) = name ++ concatMap (" " ++) args ++ " m = " ++ case m of -- Parametric types are passed formating functions for each of the parameters.
- Sum constructors -> function (map constructor constructors) ++ " m"
- Record fields -> "\"" ++ cap name ++ " { " ++ intercalate ", " (map field fields) ++ " }\""
- Alias m -> fTypeApply m ++ " m"
-
- constructor :: (String, [TypeApply]) -> (String, String)
- constructor (name, []) = (name, show $ cap name)
- constructor (name, [m]) = (name ++ " m1", show (constructorName name) ++ " ^ \" \" ^ " ++ fTypeApply m ++ " m1")
- constructor (name, args) = (name ++ " " ++ group (intercalate ", " [ "m" ++ show i | i <- [1 .. length args] ]), show (constructorName name) ++ concat [ " ^ \" \" ^ " ++ metaGroup (fTypeApply m ++ " m" ++ show i) | (m, i) <- zip args [1..] ])
-
- field :: (String, TypeApply) -> String
- field (name, t) = name ++ " = " ++ "\" ^ " ++ fTypeApply t ++ " m." ++ name ++ " ^ \""
-
- -- Returns an OCaml function :: Data -> String
- fTypeApply :: TypeApply -> String
- fTypeApply m = case m of
- TypeApply (Var "exn") [] -> "(fun _ -> \"Exn\")"
- TypeApply m [] -> name m -- Vars are top level functions, Params should be functions passed in and thus in scope.
- TypeApply (Var "list") [m] -> function [("m", "\"[ \" ^ concat \", \" (map " ++ group (fTypeApply m) ++ " m) ^ \" ]\"")]
- TypeApply (Var "option") [m] -> function [("None", show "Nothing"), ("Some m", show "Just " ++ " ^ " ++ metaGroup (fTypeApply m ++ " m"))]
- TypeApply (Var "ref") [m] -> function [("m", metaGroup (fTypeApply m ++ " (!m)"))]
- TypeApply (Var "tuple") args -> function [(group $ intercalate ", " [ "m" ++ show i | i <- [1 .. length args] ], metaGroup $ intercalate " ^ \", \" ^ " [ metaGroup (fTypeApply m ++ " m" ++ show i) | (m, i) <- zip args [1..] ])]
- TypeApply m args -> function [("m", metaGroup (name m ++ concat [ " " ++ function [("m", metaGroup (fTypeApply arg ++ " m"))] | arg <- args ] ++ " m"))]
- TypeApplyGroup a -> fTypeApply a
- where
- name (Var n) = n
- name (Par n) = n
-
- function :: [(String, String)] -> String
- function matches = group $ "function " ++ intercalate " | " [ a ++ " -> " ++ b | (a, b) <- matches ]
-
-group :: String -> String
-group a = "(" ++ a ++ ")"
-
-metaGroup :: String -> String
-metaGroup a = group $ "\"(\" ^ " ++ a ++ " ^ \")\""
-
-
--- | Makefile used to install the dumpcil plugin.
-dumpcilMakefile :: String
-dumpcilMakefile = unlines
- [ "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"
- ]
-
-
-
--- Lexing.
-
-data Token
- = Type
- | Of
- | Eq
- | Pipe
- | Colon
- | SemiColon
- | Star
- | Comma
- | ParenLeft
- | ParenRight
- | BraceLeft
- | BraceRight
- | Constructor String
- | Variable String
- | Parameter String
- deriving (Show, Eq)
-
-lexer :: String -> [Token]
-lexer = map t . filter (/= "mutable") . filter (not . null) . concatMap split . words . decomment
- where
- split :: String -> [String]
- split a = case break isSym a of
- (word, []) -> [word]
- (word, (a:b)) -> [word, [a]] ++ split b
- isSym = flip elem "=|;:*,(){}"
- t :: String -> Token
- t a = case a of
- "type" -> Type
- "and" -> Type
- "of" -> Of
- "=" -> Eq
- "|" -> Pipe
- ":" -> Colon
- ";" -> SemiColon
- "*" -> Star
- "," -> Comma
- "(" -> ParenLeft
- ")" -> ParenRight
- "{" -> BraceLeft
- "}" -> BraceRight
- '\'':a -> Parameter a
- a | elem '.' a -> t $ tail $ dropWhile (/= '.') a
- a:b | isUpper a -> Constructor (a : b)
- | otherwise -> Variable (a : b)
- a -> error $ "unexpected string: " ++ a
-
-decomment :: String -> String
-decomment = decomment' 0
- where
- decomment' :: Int -> String -> String
- decomment' n "" | n == 0 = ""
- | otherwise = error "reached end of file without closing comment"
- decomment' n ('(':'*':a) = " " ++ decomment' (n + 1) a
- decomment' n ('*':')':a) | n > 0 = " " ++ decomment' (n - 1) a
- | otherwise = error "unexpected closing comment"
- decomment' n (a:b) = (if n > 0 && a /= '\n' then ' ' else a) : decomment' n b
-
-
-
-
-
-
-
--- Parsing.
-
-type OCaml a = Parser Token a
-
-parseOCaml :: String -> [(TypeName, TypeDef)]
-parseOCaml a = case runParser (many typeDef `discard` eof) $ lexer a of
- (Left msg, remaining) -> error $ msg ++ "\nremaining tokens: " ++ show (take 30 $ remaining) ++ " ..."
- (Right a, []) -> a
- (Right _, remaining) -> error $ "parsed, but with remaining tokens: " ++ show remaining
-
-tok :: Token -> OCaml ()
-tok a = satisfy (== a) >> return ()
-
-parameter :: OCaml String
-parameter = do
- a <- satisfy (\ a -> case a of { Parameter _ -> True; _ -> False })
- case a of
- Parameter s -> return s
- _ -> undefined
-
-constructor :: OCaml String
-constructor = do
- a <- satisfy (\ a -> case a of { Constructor _ -> True; _ -> False })
- case a of
- Constructor s -> return s
- _ -> undefined
-
-variable :: OCaml String
-variable = do
- a <- satisfy (\ a -> case a of { Variable _ -> True; _ -> False })
- case a of
- Variable s -> return s
- _ -> undefined
-
-typeDef :: OCaml (TypeName, TypeDef)
-typeDef = do { tok Type; n <- typeName; tok Eq; e <- typeExpr; return (n, e) }
-
-typeName :: OCaml TypeName
-typeName = oneOf
- [ do { tok ParenLeft; a <- parameter; b <- many1 (tok Comma >> parameter); tok ParenRight; n <- variable; return $ TypeName n $ a : b }
- , do { p <- parameter; n <- variable; return $ TypeName n [p] }
- , do { n <- variable; return $ TypeName n [] }
- ]
-
-varPars :: OCaml [VarPar]
-varPars = do { a <- varPar; b <- many varPar; return $ a : b }
- where
- varPar :: OCaml VarPar
- varPar = oneOf [variable >>= return . Var, parameter >>= return . Par]
-
-typeApply :: OCaml TypeApply
-typeApply = oneOf
- [ do { tok ParenLeft; a <- varPars; b <- many1 (tok Comma >> varPars); tok ParenRight; c <- varPars; return $ TypeApplyGroup $ apply (map (apply []) (a : b)) c }
- , do { tok ParenLeft; a <- typeApply; tok ParenRight; b <- varPars; return $ TypeApplyGroup $ apply [a] b }
- , do { tok ParenLeft; a <- typeApply; tok ParenRight; return $ TypeApplyGroup a }
- -- XXX Need to prevent nested tuples.
- , do { a <- varPars; b <- many1 (tok Star >> typeApply); return $ TypeApply (Var "tuple") $ flattenTuples $ apply [] a : b }
- , do { a <- varPars; return $ apply [] a }
- ]
- where
- apply :: [TypeApply] -> [VarPar] -> TypeApply
- apply _ [] = error "typeApply: no type to apply to"
- apply args [a] = TypeApply a args
- apply args (a:b) = apply [(apply args [a])] b
-
- flattenTuples :: [TypeApply] -> [TypeApply]
- flattenTuples = concatMap flattenTuple
-
- flattenTuple :: TypeApply -> [TypeApply]
- flattenTuple (TypeApply (Var "tuple") args) = args
- flattenTuple a = [a]
-
-typeExpr :: OCaml TypeDef
-typeExpr = oneOf
- [ recordType >>= return . Record
- , sumType >>= return . Sum
- , typeApply >>= return . Alias
- ]
-
-recordType :: OCaml [(String, TypeApply)]
-recordType = do { tok BraceLeft; f <- recordField; fs <- many (tok SemiColon >> recordField); optional $ tok SemiColon; tok BraceRight; return $ f : fs }
-
-recordField :: OCaml (String, TypeApply)
-recordField = do { n <- variable; tok Colon; t <- typeApply; return (n, t) }
-
-sumType :: OCaml [(String, [TypeApply])]
-sumType = do { optional (tok Pipe); a <- sumConstructor; b <- many (tok Pipe >> sumConstructor); return $ a : b }
-
-sumConstructor :: OCaml (String, [TypeApply])
-sumConstructor = oneOf
- [ do { n <- constructor; tok Of; a <- typeApply; return (n, detuple a) }
- , do { n <- constructor; return (n, []) }
- ]
- where
- detuple :: TypeApply -> [TypeApply]
- detuple (TypeApply (Var "tuple") args) = args
- detuple a = [a]
-
diff --git a/Language/CIL.hs b/Language/CIL.hs
--- a/Language/CIL.hs
+++ b/Language/CIL.hs
@@ -1,202 +1,410 @@
--- | A Haskell interface to OCaml's CIL library, via Frama-C, providing both a simplied C AST and the ACSL specification language.
+-- | Parsing the C Intermediate Language (CIL).
+-- CIL provides a manageable means to analyze and compile C code.
+--
+-- The common method to reduce C to CIL is to use the cilly driver:
+--
+-- > cilly --merge --keepmerged { c-files-and-options }
+--
+--
module Language.CIL
- ( parseC
- , debugParseC
- , installPlugin
- , Exn (..)
- , Position (..)
- , Int64 (..)
- , BitsSizeofTyp (..)
- , BitsSizeofTypCache (..)
- , Termination_kind (..)
- , File (..)
- , Global (..)
- , Typ (..)
- , Ikind (..)
- , Fkind (..)
- , Attribute (..)
- , Attributes
- , Attrparam (..)
- , Compinfo (..)
- , Fieldinfo (..)
- , Enuminfo (..)
- , Enumitem (..)
- , Typeinfo (..)
- , Varinfo (..)
- , Storage (..)
- , Exp (..)
- , Exp_node (..)
- , Exp_info (..)
- , Constant (..)
- , Unop (..)
- , Binop (..)
- , Lval
- , Lhost (..)
- , Offset (..)
- , Init (..)
- , Initinfo (..)
- , Fundec (..)
- , Block (..)
- , Stmt (..)
- , Label (..)
- , Stmtkind (..)
- , Instr (..)
- , Location
- , Typsig (..)
- , Logic_type (..)
- , Identified_term (..)
- , Logic_label (..)
- , Term (..)
- , Term_node (..)
- , Term_lval
- , Term_lhost (..)
- , Term_offset (..)
- , Logic_info (..)
- , Builtin_logic_info (..)
- , Logic_body (..)
- , Logic_type_info (..)
- , Logic_type_def (..)
- , Logic_var (..)
- , Logic_ctor_info (..)
- , Quantifiers
- , Relation (..)
- , Predicate (..)
- , Identified_predicate (..)
- , Variant
- , Zone (..)
- , Assigns
- , Named (..)
- , Spec (..)
- , Behavior (..)
- , Loop_pragma (..)
- , Slice_pragma (..)
- , Impact_pragma (..)
- , Pragma (..)
- , Validity (..)
- , Annot_checked_status (..)
- , Annotation_status (..)
- , Annot_status (..)
- , Code_annot (..)
- , Funspec
- , Code_annotation (..)
- , Funbehavior
- , Global_annotation (..)
- , Kinstr (..)
- , Mach (..)
+ ( Name
+ , Type (..)
+ , Stmt (..)
+ , Expr (..)
+ , Init (..)
+ , Apply (..)
+ , parseCIL
+ , position
+ ) where
- )
+import Data.ByteString (ByteString)
+import Data.List
+import Language.C hiding (Name)
+import Language.C.Data.Ident
+
+-- | Identifiers.
+type Name = String
+
+-- | Types.
+data Type
+ = Void
+ | Array Int Type
+ | Ptr Type
+ | Volatile Type -- ^ A volatile qualified type.
+ | Typedef Type
+ | Struct [(Name, Type)]
+ | Union [(Name, Type)]
+ | Enum [(Name, Int)]
+ | BitField Type [(Name, Int)]
+ | StructRef Name -- ^ Reference to a struct type.
+ | UnionRef Name -- ^ Reference to a union type.
+ | EnumRef Name -- ^ Reference to an enum type.
+ | TypedefRef Name -- ^ Reference to a previously defined typedef.
+ | Function Type [Type]
+ | Int8
+ | Int16
+ | Int32
+ | Word8
+ | Word16
+ | Word32
+ | Float
+ | Double
+ deriving (Show, Eq)
+
+-- | Statements.
+data Stmt
+ = Null
+ | Compound [Name] [Stmt] Position
+ | TypeDecl Name Type Position
+ | VariableDef Name Type (Maybe Init) Position
+ | FunctionDef Name Type [(Name, Type)] Stmt Position
+ | Assign Expr Expr Position
+ | StmtApply Apply Position
+ | While Expr Stmt Position
+ | If Expr Stmt Stmt Position
+ | Return (Maybe Expr) Position
+ | Goto Name Position
+ | Break Position
+ | Switch Expr Stmt Position
+ | Case Expr Stmt Position
+ | Default Stmt Position
+ deriving (Show, Eq)
+
+-- | Expressions.
+data Expr
+ = ConstInt Int Position
+ | ConstFloat Double Position
+ | ConstChar Char Position
+ | ConstString String Position
+ | Var Name Position -- ^ Variable reference.
+ | Mul Expr Expr Position -- ^ a * b
+ | Div Expr Expr Position -- ^ a / b
+ | Rmd Expr Expr Position -- ^ a % b
+ | Add Expr Expr Position -- ^ a + b
+ | Sub Expr Expr Position -- ^ a - b
+ | Shl Expr Expr Position -- ^ a << b
+ | Shr Expr Expr Position -- ^ a >> b
+ | Lt Expr Expr Position -- ^ a < b
+ | Gt Expr Expr Position -- ^ a > b
+ | Le Expr Expr Position -- ^ a <= b
+ | Ge Expr Expr Position -- ^ a >= b
+ | Eq Expr Expr Position -- ^ a == b
+ | Neq Expr Expr Position -- ^ a != b
+ | And Expr Expr Position -- ^ a & b
+ | Xor Expr Expr Position -- ^ a ^ b
+ | Or Expr Expr Position -- ^ a | b
+ | Adr Expr Position -- ^ &a
+ | Ind Expr Position -- ^ \*a
+ | Minus Expr Position -- ^ \-a
+ | Comp Expr Position -- ^ ~a
+ | Neg Expr Position -- ^ !a
+ | Cast Type Expr Position -- ^ (...) a
+ | Index Expr Expr Position -- ^ a[b]
+ | ExprApply Apply Position -- ^ a(x, y, z)
+ | Mem Expr Name Position -- ^ a.name
+ | MemInd Expr Name Position -- ^ a->name
+ | SizeT Type Position -- ^ sizeof(type)
+ | SizeE Expr Position -- ^ sizeof(expr)
+ deriving (Show, Eq)
+
+-- | Initialization expressions.
+data Init
+ = Init Expr
+ | InitList [Init]
+ deriving (Show, Eq)
+
+-- | Function application.
+data Apply = Apply Expr [Expr] deriving (Show, Eq)
+
+instance Pos Stmt where
+ posOf a = case a of
+ Null -> undefined
+ Compound _ _ p -> p
+ TypeDecl _ _ p -> p
+ VariableDef _ _ _ p -> p
+ FunctionDef _ _ _ _ p -> p
+ Assign _ _ p -> p
+ StmtApply _ p -> p
+ While _ _ p -> p
+ If _ _ _ p -> p
+ Return _ p -> p
+ Goto _ p -> p
+ Break p -> p
+ Switch _ _ p -> p
+ Case _ _ p -> p
+ Default _ p -> p
+
+instance Pos Expr where
+ posOf a = case a of
+ ConstInt _ p -> p
+ ConstFloat _ p -> p
+ ConstChar _ p -> p
+ ConstString _ p -> p
+ Var _ p -> p
+ Mul _ _ p -> p
+ Div _ _ p -> p
+ Rmd _ _ p -> p
+ Add _ _ p -> p
+ Sub _ _ p -> p
+ Shl _ _ p -> p
+ Shr _ _ p -> p
+ Lt _ _ p -> p
+ Gt _ _ p -> p
+ Le _ _ p -> p
+ Ge _ _ p -> p
+ Eq _ _ p -> p
+ Neq _ _ p -> p
+ And _ _ p -> p
+ Xor _ _ p -> p
+ Or _ _ p -> p
+ Adr _ p -> p
+ Ind _ p -> p
+ Minus _ p -> p
+ Comp _ p -> p
+ Neg _ p -> p
+ Cast _ _ p -> p
+ Index _ _ p -> p
+ Mem _ _ p -> p
+ MemInd _ _ p -> p
+ SizeT _ p -> p
+ SizeE _ p -> p
+ ExprApply _ p -> p
+
+-- | Parses a merged CIL program, given a file name and contents.
+parseCIL :: String -> ByteString -> Stmt
+parseCIL name code = case parseC code (initPos name) of
+ Left e -> error $ "parsing error: " ++ show e
+ Right a -> cStat $ cTranslUnit a
+
+-- | Rewrites a program to a single statement.
+cTranslUnit :: CTranslUnit -> CStat
+cTranslUnit (CTranslUnit items _) = CCompound [] (map f items ++ [CBlockStmt callMain]) none
where
+ f (CDeclExt a) = CBlockDecl a
+ f (CFDefExt a) = CNestedFunDef a
+ f a@(CAsmExt _) = notSupported a "inline assembly"
+ callMain :: CStat
+ callMain = CExpr (Just $ CCall (CVar (Ident "main" 0 none) none) [] none) none
+ none :: NodeInfo
+ none = internalNode
-import System.Exit
-import System.Process
+-- | Name of identifier.
+name :: Ident -> Name
+name (Ident name _ _) = name
--- | Parse a C compilation unit (file).
-parseC :: FilePath -> IO File
-parseC file = do
- (exitCode, out, err) <- readProcessWithExitCode "frama-c" ["-dumpcil", file] ""
- let code = unlines $ tail $ lines out
- case exitCode of
- ExitSuccess -> return $ read code
- ExitFailure _ -> putStrLn err >> exitWith exitCode
+-- | Converts 'CStat' to 'Stmt'.
+cStat :: CStat -> Stmt
+cStat a = case a of
+ CLabel i a [] _ -> Compound [name i] [cStat a] p
+ CCompound ids items _ -> Compound (map name ids) (map cBlockItem items) p
+ CReturn Nothing _ -> Return Nothing p
+ CReturn (Just a) _ -> Return (Just $ cExpr a) p
+ CGoto (Ident name _ _) _ -> Goto name p
+ CBreak _ -> Break p
+ CWhile condition stmt False _ -> While (cExpr condition) (cStat stmt) p
+ CIf condition onTrue (Just onFalse) _ -> If (cExpr condition) (cStat onTrue) (cStat onFalse) p
+ CIf condition onTrue Nothing _ -> If (cExpr condition) (cStat onTrue) Null p
+ CSwitch expr stmt _ -> Switch (cExpr expr) (cStat stmt) p
+ CCase a b _ -> Case (cExpr a) (cStat b) p
+ CDefault a _ -> Default (cStat a) p
--- | Prints output from frama-c -dumpcil.
-debugParseC :: FilePath -> IO ()
-debugParseC file = do
- (exitCode, out, err) <- readProcessWithExitCode "frama-c" ["-dumpcil", file] ""
- putStrLn out
+ CExpr Nothing _ -> Null
+ CExpr (Just (CAssign op a b n)) _ -> case op of
+ CAssignOp -> Assign (cExpr a) (cExpr b) $ posOf n
+ CMulAssOp -> f CMulOp
+ CDivAssOp -> f CDivOp
+ CRmdAssOp -> f CRmdOp
+ CAddAssOp -> f CAddOp
+ CSubAssOp -> f CSubOp
+ CShlAssOp -> f CShlOp
+ CShrAssOp -> f CShrOp
+ CAndAssOp -> f CAndOp
+ CXorAssOp -> f CXorOp
+ COrAssOp -> f COrOp
+ where
+ f :: CBinaryOp -> Stmt
+ f op = cStat (CExpr (Just (CAssign CAssignOp a (CBinary op a b n) n)) n)
- -- | Installs Frama-C '-dumpcil' plugin. Creates 'install-dumpcil-pluging' directory, deposits a Makefile and dump_cil.ml, then runs 'make' and 'make install'.
-installPlugin :: IO ()
-installPlugin = do
- putStrLn "creating install-dumpcil-plugin directory for plugin compiling and installation ..."
- system "mkdir -p install-dumpcil-plugin"
- writeFile "install-dumpcil-plugin/Makefile" "FRAMAC_SHARE :=$(shell frama-c.byte -print-path)\nFRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)\nPLUGIN_NAME = Dumpcil\nPLUGIN_CMO = dump_cil\ninclude $(FRAMAC_SHARE)/Makefile.dynamic\n"
- writeFile "install-dumpcil-plugin/dump_cil.ml" "open Ast\nopen Cil_types\nopen File\nopen Lexing\nopen List\nopen String\nopen Int64\nopen Char\n\nlet string a = \"\\\"\" ^ a ^ \"\\\"\" (* XXX Doesn't handle '\\' or '\"' chars in string. *)\nlet position t = \"Position \\\"\" ^ t.pos_fname ^ \"\\\" \" ^ string_of_int t.pos_lnum ^ \" \" ^ string_of_int (t.pos_cnum - t.pos_bol + 1)\nlet bool a = if a then \"True\" else \"False\"\nlet char = Char.escaped\nlet int = string_of_int\nlet int64 = Int64.to_string\nlet float = string_of_float\n\nlet rec bitsSizeofTyp m = (function Not_Computed -> \"Not_Computed\" | Not_Computable m1 -> \"Not_Computable\" ^ \" \" ^ (fun _ -> \"Exn\") m1 | Computed m1 -> \"Computed\" ^ \" \" ^ int m1) m\nand bitsSizeofTypCache m = \"BitsSizeofTypCache { scache = \" ^ bitsSizeofTyp m.scache ^ \" }\"\nand termination_kind m = (function Normal -> \"Normal\" | Exits -> \"Exits\" | Breaks -> \"Breaks\" | Continues -> \"Continues\" | Returns -> \"Returns\") m\nand file m = \"File { fileName = \" ^ string m.fileName ^ \", globals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (global) m) ^ \" ]\") m.globals ^ \", globinit = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ fundec m ^ \")\")) m.globinit ^ \", globinitcalled = \" ^ bool m.globinitcalled ^ \" }\"\nand global m = (function GType (m1, m2) -> \"GType\" ^ \" \" ^ (\"(\" ^ typeinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GCompTag (m1, m2) -> \"GCompTag\" ^ \" \" ^ (\"(\" ^ compinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GCompTagDecl (m1, m2) -> \"GCompTagDecl\" ^ \" \" ^ (\"(\" ^ compinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GEnumTag (m1, m2) -> \"GEnumTag\" ^ \" \" ^ (\"(\" ^ enuminfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GEnumTagDecl (m1, m2) -> \"GEnumTagDecl\" ^ \" \" ^ (\"(\" ^ enuminfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GVarDecl (m1, m2, m3) -> \"GVarDecl\" ^ \" \" ^ (\"(\" ^ funspec m1 ^ \")\") ^ \" \" ^ (\"(\" ^ varinfo m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | GVar (m1, m2, m3) -> \"GVar\" ^ \" \" ^ (\"(\" ^ varinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ initinfo m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | GFun (m1, m2) -> \"GFun\" ^ \" \" ^ (\"(\" ^ fundec m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GAsm (m1, m2) -> \"GAsm\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GPragma (m1, m2) -> \"GPragma\" ^ \" \" ^ (\"(\" ^ attribute m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GText m1 -> \"GText\" ^ \" \" ^ string m1 | GAnnot (m1, m2) -> \"GAnnot\" ^ \" \" ^ (\"(\" ^ global_annotation m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\")) m\nand typ m = (function TVoid m1 -> \"TVoid\" ^ \" \" ^ attributes m1 | TInt (m1, m2) -> \"TInt\" ^ \" \" ^ (\"(\" ^ ikind m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TFloat (m1, m2) -> \"TFloat\" ^ \" \" ^ (\"(\" ^ fkind m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TPtr (m1, m2) -> \"TPtr\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TArray (m1, m2, m3, m4) -> \"TArray\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ exp m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bitsSizeofTypCache m3 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m4 ^ \")\") | TFun (m1, m2, m3, m4) -> \"TFun\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3) -> (\"(\" ^ (\"(\" ^ string m1 ^ \")\") ^ \", \" ^ (\"(\" ^ typ m2 ^ \")\") ^ \", \" ^ (\"(\" ^ attributes m3 ^ \")\") ^ \")\"))) m) ^ \" ]\") m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m3 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m4 ^ \")\") | TNamed (m1, m2) -> \"TNamed\" ^ \" \" ^ (\"(\" ^ typeinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TComp (m1, m2, m3) -> \"TComp\" ^ \" \" ^ (\"(\" ^ compinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ bitsSizeofTypCache m2 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m3 ^ \")\") | TEnum (m1, m2) -> \"TEnum\" ^ \" \" ^ (\"(\" ^ enuminfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TBuiltin_va_list m1 -> \"TBuiltin_va_list\" ^ \" \" ^ attributes m1) m\nand ikind m = (function IBool -> \"IBool\" | IChar -> \"IChar\" | ISChar -> \"ISChar\" | IUChar -> \"IUChar\" | IInt -> \"IInt\" | IUInt -> \"IUInt\" | IShort -> \"IShort\" | IUShort -> \"IUShort\" | ILong -> \"ILong\" | IULong -> \"IULong\" | ILongLong -> \"ILongLong\" | IULongLong -> \"IULongLong\") m\nand fkind m = (function FFloat -> \"FFloat\" | FDouble -> \"FDouble\" | FLongDouble -> \"FLongDouble\") m\nand attribute m = (function Attr (m1, m2) -> \"Attr\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attrparam) m) ^ \" ]\") m2 ^ \")\") | AttrAnnot m1 -> \"AttrAnnot\" ^ \" \" ^ string m1) m\nand attributes m = (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m\nand attrparam m = (function AInt m1 -> \"AInt\" ^ \" \" ^ int m1 | AStr m1 -> \"AStr\" ^ \" \" ^ string m1 | ACons (m1, m2) -> \"ACons\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attrparam) m) ^ \" ]\") m2 ^ \")\") | ASizeOf m1 -> \"ASizeOf\" ^ \" \" ^ typ m1 | ASizeOfE m1 -> \"ASizeOfE\" ^ \" \" ^ attrparam m1 | ASizeOfS m1 -> \"ASizeOfS\" ^ \" \" ^ typsig m1 | AAlignOf m1 -> \"AAlignOf\" ^ \" \" ^ typ m1 | AAlignOfE m1 -> \"AAlignOfE\" ^ \" \" ^ attrparam m1 | AAlignOfS m1 -> \"AAlignOfS\" ^ \" \" ^ typsig m1 | AUnOp (m1, m2) -> \"AUnOp\" ^ \" \" ^ (\"(\" ^ unop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") | ABinOp (m1, m2, m3) -> \"ABinOp\" ^ \" \" ^ (\"(\" ^ binop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m3 ^ \")\") | ADot (m1, m2) -> \"ADot\" ^ \" \" ^ (\"(\" ^ attrparam m1 ^ \")\") ^ \" \" ^ (\"(\" ^ string m2 ^ \")\") | AStar m1 -> \"AStar\" ^ \" \" ^ attrparam m1 | AAddrOf m1 -> \"AAddrOf\" ^ \" \" ^ attrparam m1 | AIndex (m1, m2) -> \"AIndex\" ^ \" \" ^ (\"(\" ^ attrparam m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") | AQuestion (m1, m2, m3) -> \"AQuestion\" ^ \" \" ^ (\"(\" ^ attrparam m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m3 ^ \")\")) m\nand compinfo m = \"Compinfo { cstruct = \" ^ bool m.cstruct ^ \", cname = \" ^ string m.cname ^ \", ckey = \" ^ int m.ckey ^ \", cfields = \" ^ (function m -> \"[ \" ^ concat \", \" (map (fieldinfo) m) ^ \" ]\") m.cfields ^ \", cattr = \" ^ attributes m.cattr ^ \", cdefined = \" ^ bool m.cdefined ^ \", creferenced = \" ^ bool m.creferenced ^ \" }\"\nand fieldinfo m = \"Fieldinfo { fcomp = \" ^ compinfo m.fcomp ^ \", fname = \" ^ string m.fname ^ \", ftype = \" ^ typ m.ftype ^ \", fbitfield = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.fbitfield ^ \", fattr = \" ^ attributes m.fattr ^ \", floc = \" ^ location m.floc ^ \", faddrof = \" ^ bool m.faddrof ^ \", fsize_in_bits = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.fsize_in_bits ^ \", foffset_in_bits = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.foffset_in_bits ^ \", fpadding_in_bits = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.fpadding_in_bits ^ \" }\"\nand enuminfo m = \"Enuminfo { ename = \" ^ string m.ename ^ \", eitems = \" ^ (function m -> \"[ \" ^ concat \", \" (map (enumitem) m) ^ \" ]\") m.eitems ^ \", eattr = \" ^ attributes m.eattr ^ \", ereferenced = \" ^ bool m.ereferenced ^ \" }\"\nand enumitem m = \"Enumitem { einame = \" ^ string m.einame ^ \", eival = \" ^ exp m.eival ^ \", eihost = \" ^ enuminfo m.eihost ^ \", eiloc = \" ^ location m.eiloc ^ \" }\"\nand typeinfo m = \"Typeinfo { tname = \" ^ string m.tname ^ \", ttype = \" ^ typ m.ttype ^ \", treferenced = \" ^ bool m.treferenced ^ \" }\"\nand varinfo m = \"Varinfo { vname = \" ^ string m.vname ^ \", vorig_name = \" ^ string m.vorig_name ^ \", vtype = \" ^ typ m.vtype ^ \", vattr = \" ^ attributes m.vattr ^ \", vstorage = \" ^ storage m.vstorage ^ \", vglob = \" ^ bool m.vglob ^ \", vdefined = \" ^ bool m.vdefined ^ \", vformal = \" ^ bool m.vformal ^ \", vinline = \" ^ bool m.vinline ^ \", vdecl = \" ^ location m.vdecl ^ \", vid = \" ^ int m.vid ^ \", vaddrof = \" ^ bool m.vaddrof ^ \", vreferenced = \" ^ bool m.vreferenced ^ \", vgenerated = \" ^ bool m.vgenerated ^ \", vdescr = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m.vdescr ^ \", vdescrpure = \" ^ bool m.vdescrpure ^ \", vghost = \" ^ bool m.vghost ^ \", vlogic = \" ^ bool m.vlogic ^ \", vlogic_var_assoc = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_var m ^ \")\")) m.vlogic_var_assoc ^ \" }\"\nand storage m = (function NoStorage -> \"NoStorage\" | Static -> \"Static\" | Register -> \"Register\" | Extern -> \"Extern\") m\nand exp m = \"Exp { eid = \" ^ int m.eid ^ \", enode = \" ^ exp_node m.enode ^ \" }\"\nand exp_node m = (function Const m1 -> \"Const\" ^ \" \" ^ constant m1 | Lval m1 -> \"Lval\" ^ \" \" ^ lval m1 | SizeOf m1 -> \"SizeOf\" ^ \" \" ^ typ m1 | SizeOfE m1 -> \"SizeOfE\" ^ \" \" ^ exp m1 | SizeOfStr m1 -> \"SizeOfStr\" ^ \" \" ^ string m1 | AlignOf m1 -> \"AlignOf\" ^ \" \" ^ typ m1 | AlignOfE m1 -> \"AlignOfE\" ^ \" \" ^ exp m1 | UnOp (m1, m2, m3) -> \"UnOp\" ^ \" \" ^ (\"(\" ^ unop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ typ m3 ^ \")\") | BinOp (m1, m2, m3, m4) -> \"BinOp\" ^ \" \" ^ (\"(\" ^ binop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m3 ^ \")\") ^ \" \" ^ (\"(\" ^ typ m4 ^ \")\") | CastE (m1, m2) -> \"CastE\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") | AddrOf m1 -> \"AddrOf\" ^ \" \" ^ lval m1 | StartOf m1 -> \"StartOf\" ^ \" \" ^ lval m1 | Info (m1, m2) -> \"Info\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp_info m2 ^ \")\")) m\nand exp_info m = \"Exp_info { exp_loc = \" ^ location m.exp_loc ^ \", exp_type = \" ^ logic_type m.exp_type ^ \", exp_name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.exp_name ^ \" }\"\nand constant m = (function CInt64 (m1, m2, m3) -> \"CInt64\" ^ \" \" ^ (\"(\" ^ int64 m1 ^ \")\") ^ \" \" ^ (\"(\" ^ ikind m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m3 ^ \")\") | CStr m1 -> \"CStr\" ^ \" \" ^ string m1 | CWStr m1 -> \"CWStr\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (int64) m) ^ \" ]\") m1 | CChr m1 -> \"CChr\" ^ \" \" ^ char m1 | CReal (m1, m2, m3) -> \"CReal\" ^ \" \" ^ (\"(\" ^ float m1 ^ \")\") ^ \" \" ^ (\"(\" ^ fkind m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m3 ^ \")\") | CEnum m1 -> \"CEnum\" ^ \" \" ^ enumitem m1) m\nand unop m = (function Neg -> \"Neg\" | BNot -> \"BNot\" | LNot -> \"LNot\") m\nand binop m = (function 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\") m\nand lval m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ lhost m1 ^ \")\") ^ \", \" ^ (\"(\" ^ offset m2 ^ \")\") ^ \")\")) m\nand lhost m = (function Var m1 -> \"Var\" ^ \" \" ^ varinfo m1 | Mem m1 -> \"Mem\" ^ \" \" ^ exp m1) m\nand offset m = (function NoOffset -> \"NoOffset\" | Field (m1, m2) -> \"Field\" ^ \" \" ^ (\"(\" ^ fieldinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ offset m2 ^ \")\") | Index (m1, m2) -> \"Index\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ offset m2 ^ \")\")) m\nand init m = (function SingleInit m1 -> \"SingleInit\" ^ \" \" ^ exp m1 | CompoundInit (m1, m2) -> \"CompoundInit\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ offset m1 ^ \")\") ^ \", \" ^ (\"(\" ^ init m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m2 ^ \")\")) m\nand initinfo m = \"Initinfo { init = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ init m ^ \")\")) m.init ^ \" }\"\nand fundec m = \"Fundec { svar = \" ^ varinfo m.svar ^ \", sformals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (varinfo) m) ^ \" ]\") m.sformals ^ \", slocals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (varinfo) m) ^ \" ]\") m.slocals ^ \", smaxid = \" ^ int m.smaxid ^ \", sbody = \" ^ block m.sbody ^ \", smaxstmtid = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.smaxstmtid ^ \", sallstmts = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.sallstmts ^ \", sspec = \" ^ funspec m.sspec ^ \" }\"\nand block m = \"Block { battrs = \" ^ attributes m.battrs ^ \", blocals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (varinfo) m) ^ \" ]\") m.blocals ^ \", bstmts = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.bstmts ^ \" }\"\nand stmt m = \"Stmt { labels = \" ^ (function m -> \"[ \" ^ concat \", \" (map (label) m) ^ \" ]\") m.labels ^ \", skind = \" ^ stmtkind m.skind ^ \", sid = \" ^ int m.sid ^ \", succs = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.succs ^ \", preds = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.preds ^ \", ghost = \" ^ bool m.ghost ^ \" }\"\nand label m = (function Label (m1, m2, m3) -> \"Label\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m3 ^ \")\") | Case (m1, m2) -> \"Case\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | Default m1 -> \"Default\" ^ \" \" ^ location m1) m\nand stmtkind m = (function Instr m1 -> \"Instr\" ^ \" \" ^ instr m1 | Return (m1, m2) -> \"Return\" ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ exp m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | Goto (m1, m2) -> \"Goto\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ stmt (!m) ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | Break m1 -> \"Break\" ^ \" \" ^ location m1 | Continue m1 -> \"Continue\" ^ \" \" ^ location m1 | If (m1, m2, m3, m4) -> \"If\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ block m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\") | Switch (m1, m2, m3, m4) -> \"Switch\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\") | Loop (m1, m2, m3, m4, m5) -> \"Loop\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (code_annotation) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ stmt m ^ \")\")) m4 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ stmt m ^ \")\")) m5 ^ \")\") | Block m1 -> \"Block'\" ^ \" \" ^ block m1 | UnspecifiedSequence m1 -> \"UnspecifiedSequence\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3, m4) -> (\"(\" ^ (\"(\" ^ stmt m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (lval) m) ^ \" ]\") m2 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (lval) m) ^ \" ]\") m3 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (lval) m) ^ \" ]\") m4 ^ \")\") ^ \")\"))) m) ^ \" ]\") m1 | TryFinally (m1, m2, m3) -> \"TryFinally\" ^ \" \" ^ (\"(\" ^ block m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | TryExcept (m1, m2, m3, m4) -> \"TryExcept\" ^ \" \" ^ (\"(\" ^ block m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function (m1, m2) -> (\"(\" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (instr) m) ^ \" ]\") m1 ^ \")\") ^ \", \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ block m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\")) m\nand instr m = (function Set (m1, m2, m3) -> \"Set\" ^ \" \" ^ (\"(\" ^ lval m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | Call (m1, m2, m3, m4) -> \"Call\" ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ lval m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (exp) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\") | Asm (m1, m2, m3, m4, m5, m6) -> \"Asm\" ^ \" \" ^ (\"(\" ^ attributes m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3) -> (\"(\" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m1 ^ \")\") ^ \", \" ^ (\"(\" ^ string m2 ^ \")\") ^ \", \" ^ (\"(\" ^ lval m3 ^ \")\") ^ \")\"))) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3) -> (\"(\" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m1 ^ \")\") ^ \", \" ^ (\"(\" ^ string m2 ^ \")\") ^ \", \" ^ (\"(\" ^ exp m3 ^ \")\") ^ \")\"))) m) ^ \" ]\") m4 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m5 ^ \")\") ^ \" \" ^ (\"(\" ^ location m6 ^ \")\") | Skip m1 -> \"Skip\" ^ \" \" ^ location m1 | Code_annot (m1, m2) -> \"Code_annot\" ^ \" \" ^ (\"(\" ^ code_annotation m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\")) m\nand location m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ position m1 ^ \")\") ^ \", \" ^ (\"(\" ^ position m2 ^ \")\") ^ \")\")) m\nand typsig m = (function TSArray (m1, m2, m3) -> \"TSArray\" ^ \" \" ^ (\"(\" ^ typsig m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int64 m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m3 ^ \")\") | TSPtr (m1, m2) -> \"TSPtr\" ^ \" \" ^ (\"(\" ^ typsig m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m2 ^ \")\") | TSComp (m1, m2, m3) -> \"TSComp\" ^ \" \" ^ (\"(\" ^ bool m1 ^ \")\") ^ \" \" ^ (\"(\" ^ string m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m3 ^ \")\") | TSFun (m1, m2, m3, m4) -> \"TSFun\" ^ \" \" ^ (\"(\" ^ typsig m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (typsig) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m4 ^ \")\") | TSEnum (m1, m2) -> \"TSEnum\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m2 ^ \")\") | TSBase m1 -> \"TSBase\" ^ \" \" ^ typ m1) m\nand logic_type m = (function Ctype m1 -> \"Ctype\" ^ \" \" ^ typ m1 | Ltype (m1, m2) -> \"Ltype\" ^ \" \" ^ (\"(\" ^ logic_type_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_type) m) ^ \" ]\") m2 ^ \")\") | Lvar m1 -> \"Lvar\" ^ \" \" ^ string m1 | Linteger -> \"Linteger\" | Lreal -> \"Lreal\" | Larrow (m1, m2) -> \"Larrow\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_type) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ logic_type m2 ^ \")\")) m\nand identified_term m = \"Identified_term { it_id = \" ^ int m.it_id ^ \", it_content = \" ^ term m.it_content ^ \" }\"\nand logic_label m = (function StmtLabel m1 -> \"StmtLabel\" ^ \" \" ^ (function m -> (\"(\" ^ stmt (!m) ^ \")\")) m1 | LogicLabel m1 -> \"LogicLabel\" ^ \" \" ^ string m1) m\nand term m = \"Term { term_node = \" ^ term_node m.term_node ^ \", term_loc = \" ^ (function (m1, m2) -> (\"(\" ^ (\"(\" ^ position m1 ^ \")\") ^ \", \" ^ (\"(\" ^ position m2 ^ \")\") ^ \")\")) m.term_loc ^ \", term_type = \" ^ logic_type m.term_type ^ \", term_name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.term_name ^ \" }\"\nand term_node m = (function TConst m1 -> \"TConst\" ^ \" \" ^ constant m1 | TLval m1 -> \"TLval\" ^ \" \" ^ term_lval m1 | TSizeOf m1 -> \"TSizeOf\" ^ \" \" ^ typ m1 | TSizeOfE m1 -> \"TSizeOfE\" ^ \" \" ^ term m1 | TSizeOfStr m1 -> \"TSizeOfStr\" ^ \" \" ^ string m1 | TAlignOf m1 -> \"TAlignOf\" ^ \" \" ^ typ m1 | TAlignOfE m1 -> \"TAlignOfE\" ^ \" \" ^ term m1 | TUnOp (m1, m2) -> \"TUnOp\" ^ \" \" ^ (\"(\" ^ unop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TBinOp (m1, m2, m3) -> \"TBinOp\" ^ \" \" ^ (\"(\" ^ binop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | TCastE (m1, m2) -> \"TCastE\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TAddrOf m1 -> \"TAddrOf\" ^ \" \" ^ term_lval m1 | TStartOf m1 -> \"TStartOf\" ^ \" \" ^ term_lval m1 | Tapp (m1, m2, m3) -> \"Tapp\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ logic_label m1 ^ \")\") ^ \", \" ^ (\"(\" ^ logic_label m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m3 ^ \")\") | Tlambda (m1, m2) -> \"Tlambda\" ^ \" \" ^ (\"(\" ^ quantifiers m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TDataCons (m1, m2) -> \"TDataCons\" ^ \" \" ^ (\"(\" ^ logic_ctor_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m2 ^ \")\") | Tif (m1, m2, m3) -> \"Tif\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Told m1 -> \"Told\" ^ \" \" ^ term m1 | Tat (m1, m2) -> \"Tat\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ logic_label m2 ^ \")\") | Tbase_addr m1 -> \"Tbase_addr\" ^ \" \" ^ term m1 | Tblock_length m1 -> \"Tblock_length\" ^ \" \" ^ term m1 | Tnull -> \"Tnull\" | TCoerce (m1, m2) -> \"TCoerce\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ typ m2 ^ \")\") | TCoerceE (m1, m2) -> \"TCoerceE\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TUpdate (m1, m2, m3) -> \"TUpdate\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ fieldinfo m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Ttypeof m1 -> \"Ttypeof\" ^ \" \" ^ term m1 | Ttype m1 -> \"Ttype\" ^ \" \" ^ typ m1 | Tempty_set -> \"Tempty_set\" | Tunion m1 -> \"Tunion\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Tinter m1 -> \"Tinter\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Tcomprehension (m1, m2, m3) -> \"Tcomprehension\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ quantifiers m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m ^ \")\")) m3 ^ \")\") | Trange (m1, m2) -> \"Trange\" ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ term m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ term m ^ \")\")) m2 ^ \")\") | Tlet (m1, m2) -> \"Tlet\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\")) m\nand term_lval m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ term_lhost m1 ^ \")\") ^ \", \" ^ (\"(\" ^ term_offset m2 ^ \")\") ^ \")\")) m\nand term_lhost m = (function TVar m1 -> \"TVar\" ^ \" \" ^ logic_var m1 | TResult m1 -> \"TResult\" ^ \" \" ^ typ m1 | TMem m1 -> \"TMem\" ^ \" \" ^ term m1) m\nand term_offset m = (function TNoOffset -> \"TNoOffset\" | TField (m1, m2) -> \"TField\" ^ \" \" ^ (\"(\" ^ fieldinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term_offset m2 ^ \")\") | TIndex (m1, m2) -> \"TIndex\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term_offset m2 ^ \")\")) m\nand logic_info m = \"Logic_info { l_var_info = \" ^ logic_var m.l_var_info ^ \", l_labels = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m.l_labels ^ \", l_tparams = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.l_tparams ^ \", l_type = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_type m ^ \")\")) m.l_type ^ \", l_profile = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_var) m) ^ \" ]\") m.l_profile ^ \", l_body = \" ^ logic_body m.l_body ^ \" }\"\nand builtin_logic_info m = \"Builtin_logic_info { bl_name = \" ^ string m.bl_name ^ \", bl_labels = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m.bl_labels ^ \", bl_params = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.bl_params ^ \", bl_type = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_type m ^ \")\")) m.bl_type ^ \", bl_profile = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ string m1 ^ \")\") ^ \", \" ^ (\"(\" ^ logic_type m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m.bl_profile ^ \" }\"\nand logic_body m = (function LBnone -> \"LBnone\" | LBreads m1 -> \"LBreads\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (identified_term) m) ^ \" ]\") m1 | LBterm m1 -> \"LBterm\" ^ \" \" ^ term m1 | LBpred m1 -> \"LBpred\" ^ \" \" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 | LBinductive m1 -> \"LBinductive\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3, m4) -> (\"(\" ^ (\"(\" ^ string m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m2 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m3 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m4 ^ \")\") ^ \")\"))) m) ^ \" ]\") m1) m\nand logic_type_info m = \"Logic_type_info { lt_name = \" ^ string m.lt_name ^ \", lt_params = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.lt_params ^ \", lt_def = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_type_def m ^ \")\")) m.lt_def ^ \" }\"\nand logic_type_def m = (function LTsum m1 -> \"LTsum\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_ctor_info) m) ^ \" ]\") m1 | LTsyn m1 -> \"LTsyn\" ^ \" \" ^ logic_type m1) m\nand logic_var m = \"Logic_var { lv_name = \" ^ string m.lv_name ^ \", lv_id = \" ^ int m.lv_id ^ \", lv_type = \" ^ logic_type m.lv_type ^ \", lv_origin = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ varinfo m ^ \")\")) m.lv_origin ^ \" }\"\nand logic_ctor_info m = \"Logic_ctor_info { ctor_name = \" ^ string m.ctor_name ^ \", ctor_type = \" ^ logic_type_info m.ctor_type ^ \", ctor_params = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_type) m) ^ \" ]\") m.ctor_params ^ \" }\"\nand quantifiers m = (function m -> \"[ \" ^ concat \", \" (map (logic_var) m) ^ \" ]\") m\nand relation m = (function Rlt -> \"Rlt\" | Rgt -> \"Rgt\" | Rle -> \"Rle\" | Rge -> \"Rge\" | Req -> \"Req\" | Rneq -> \"Rneq\") m\nand predicate m = (function Pfalse -> \"Pfalse\" | Ptrue -> \"Ptrue\" | Papp (m1, m2, m3) -> \"Papp\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ logic_label m1 ^ \")\") ^ \", \" ^ (\"(\" ^ logic_label m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m3 ^ \")\") | Pseparated m1 -> \"Pseparated\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Prel (m1, m2, m3) -> \"Prel\" ^ \" \" ^ (\"(\" ^ relation m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Pand (m1, m2) -> \"Pand\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Por (m1, m2) -> \"Por\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pxor (m1, m2) -> \"Pxor\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pimplies (m1, m2) -> \"Pimplies\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Piff (m1, m2) -> \"Piff\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pnot m1 -> \"Pnot\" ^ \" \" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 | Pif (m1, m2, m3) -> \"Pif\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m3 ^ \")\") | Plet (m1, m2) -> \"Plet\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pforall (m1, m2) -> \"Pforall\" ^ \" \" ^ (\"(\" ^ quantifiers m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pexists (m1, m2) -> \"Pexists\" ^ \" \" ^ (\"(\" ^ quantifiers m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pold m1 -> \"Pold\" ^ \" \" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 | Pat (m1, m2) -> \"Pat\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ logic_label m2 ^ \")\") | Pvalid m1 -> \"Pvalid\" ^ \" \" ^ term m1 | Pvalid_index (m1, m2) -> \"Pvalid_index\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | Pvalid_range (m1, m2, m3) -> \"Pvalid_range\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Pfresh m1 -> \"Pfresh\" ^ \" \" ^ term m1 | Psubtype (m1, m2) -> \"Psubtype\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\")) m\nand identified_predicate m = \"Identified_predicate { ip_name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.ip_name ^ \", ip_loc = \" ^ location m.ip_loc ^ \", ip_id = \" ^ int m.ip_id ^ \", ip_content = \" ^ predicate m.ip_content ^ \" }\"\nand variant term m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ term m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m2 ^ \")\") ^ \")\")) m\nand zone locs m = (function Location m1 -> \"Location\" ^ \" \" ^ locs m1 | Nothing -> \"Nothing\") m\nand assigns locs m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ (function m -> (\"(\" ^ zone (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> (\"(\" ^ zone (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\"))) m) ^ \" ]\") m2 ^ \")\") ^ \")\")) m\nand named a m = \"Named { name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.name ^ \", loc = \" ^ location m.loc ^ \", content = \" ^ a m.content ^ \" }\"\nand spec term pred locs m = \"Spec { spec_requires = \" ^ (function m -> \"[ \" ^ concat \", \" (map (pred) m) ^ \" ]\") m.spec_requires ^ \", spec_behavior = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> (\"(\" ^ behavior (function m -> (\"(\" ^ pred m ^ \")\")) (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\"))) m) ^ \" ]\") m.spec_behavior ^ \", spec_variant = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ (function m -> (\"(\" ^ variant (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m ^ \")\")) m.spec_variant ^ \", spec_terminates = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ pred m ^ \")\")) m.spec_terminates ^ \", spec_complete_behaviors = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\")) m) ^ \" ]\") m.spec_complete_behaviors ^ \", spec_disjoint_behaviors = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\")) m) ^ \" ]\") m.spec_disjoint_behaviors ^ \" }\"\nand behavior pred locs m = \"Behavior { b_name = \" ^ string m.b_name ^ \", b_assumes = \" ^ (function m -> \"[ \" ^ concat \", \" (map (pred) m) ^ \" ]\") m.b_assumes ^ \", b_post_cond = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ termination_kind m1 ^ \")\") ^ \", \" ^ (\"(\" ^ pred m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m.b_post_cond ^ \", b_assigns = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> (\"(\" ^ assigns (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\"))) m) ^ \" ]\") m.b_assigns ^ \" }\"\nand loop_pragma term m = (function Unroll_level m1 -> \"Unroll_level\" ^ \" \" ^ term m1 | Widen_hints m1 -> \"Widen_hints\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Widen_variables m1 -> \"Widen_variables\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1) m\nand slice_pragma term m = (function SPexpr m1 -> \"SPexpr\" ^ \" \" ^ term m1 | SPctrl -> \"SPctrl\" | SPstmt -> \"SPstmt\") m\nand impact_pragma term m = (function IPexpr m1 -> \"IPexpr\" ^ \" \" ^ term m1 | IPstmt -> \"IPstmt\") m\nand pragma term m = (function Loop_pragma m1 -> \"Loop_pragma\" ^ \" \" ^ (function m -> (\"(\" ^ loop_pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1 | Slice_pragma m1 -> \"Slice_pragma\" ^ \" \" ^ (function m -> (\"(\" ^ slice_pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1 | Impact_pragma m1 -> \"Impact_pragma\" ^ \" \" ^ (function m -> (\"(\" ^ impact_pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1) m\nand validity m = (function True -> \"True\" | False -> \"False\" | Maybe -> \"Maybe\") m\nand annot_checked_status m = \"Annot_checked_status { emitter = \" ^ string m.emitter ^ \", valid = \" ^ validity m.valid ^ \" }\"\nand annotation_status m = (function Unknown -> \"Unknown\" | Checked m1 -> \"Checked\" ^ \" \" ^ annot_checked_status m1) m\nand annot_status m = \"Annot_status { status = \" ^ annotation_status m.status ^ \" }\"\nand code_annot term pred spec_pred locs m = (function AAssert (m1, m2, m3) -> \"AAssert\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ pred m2 ^ \")\") ^ \" \" ^ (\"(\" ^ annot_status m3 ^ \")\") | AStmtSpec m1 -> \"AStmtSpec\" ^ \" \" ^ (function m -> (\"(\" ^ spec (function m -> (\"(\" ^ term m ^ \")\")) (function m -> (\"(\" ^ spec_pred m ^ \")\")) (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\")) m1 | AInvariant (m1, m2, m3) -> \"AInvariant\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m2 ^ \")\") ^ \" \" ^ (\"(\" ^ pred m3 ^ \")\") | AVariant m1 -> \"AVariant\" ^ \" \" ^ (function m -> (\"(\" ^ variant (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1 | AAssigns (m1, m2) -> \"AAssigns\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ assigns (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\")) m2 ^ \")\") | APragma m1 -> \"APragma\" ^ \" \" ^ (function m -> (\"(\" ^ pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1) m\nand funspec m = (function m -> (\"(\" ^ spec (function m -> (\"(\" ^ term m ^ \")\")) (function m -> (\"(\" ^ identified_predicate m ^ \")\")) (function m -> (\"(\" ^ identified_term m ^ \")\")) m ^ \")\")) m\nand code_annotation m = \"Code_annotation { annot_content = \" ^ (function m -> (\"(\" ^ code_annot (function m -> (\"(\" ^ term m ^ \")\")) (function m -> (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m ^ \")\")) (function m -> (\"(\" ^ identified_predicate m ^ \")\")) (function m -> (\"(\" ^ identified_term m ^ \")\")) m ^ \")\")) m.annot_content ^ \", annot_id = \" ^ int m.annot_id ^ \" }\"\nand funbehavior m = (function m -> (\"(\" ^ behavior (function m -> (\"(\" ^ identified_predicate m ^ \")\")) (function m -> (\"(\" ^ identified_term m ^ \")\")) m ^ \")\")) m\nand global_annotation m = (function Dfun_or_pred m1 -> \"Dfun_or_pred\" ^ \" \" ^ logic_info m1 | Daxiomatic (m1, m2) -> \"Daxiomatic\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (global_annotation) m) ^ \" ]\") m2 ^ \")\") | Dtype m1 -> \"Dtype\" ^ \" \" ^ logic_type_info m1 | Dlemma (m1, m2, m3, m4, m5) -> \"Dlemma\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m4 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m5 ^ \")\") | Dinvariant m1 -> \"Dinvariant\" ^ \" \" ^ logic_info m1 | Dtype_annot m1 -> \"Dtype_annot\" ^ \" \" ^ logic_info m1) m\nand kinstr m = (function Kstmt m1 -> \"Kstmt\" ^ \" \" ^ stmt m1 | Kglobal -> \"Kglobal\") m\nand mach m = \"Mach { version_major = \" ^ int m.version_major ^ \", version_minor = \" ^ int m.version_minor ^ \", version = \" ^ string m.version ^ \", underscore_name = \" ^ bool m.underscore_name ^ \", sizeof_short = \" ^ int m.sizeof_short ^ \", sizeof_int = \" ^ int m.sizeof_int ^ \", sizeof_long = \" ^ int m.sizeof_long ^ \", sizeof_longlong = \" ^ int m.sizeof_longlong ^ \", sizeof_ptr = \" ^ int m.sizeof_ptr ^ \", sizeof_enum = \" ^ int m.sizeof_enum ^ \", sizeof_float = \" ^ int m.sizeof_float ^ \", sizeof_double = \" ^ int m.sizeof_double ^ \", sizeof_longdouble = \" ^ int m.sizeof_longdouble ^ \", sizeof_void = \" ^ int m.sizeof_void ^ \", sizeof_fun = \" ^ int m.sizeof_fun ^ \", size_t = \" ^ string m.size_t ^ \", wchar_t = \" ^ string m.wchar_t ^ \", ptrdiff_t = \" ^ string m.ptrdiff_t ^ \", enum_are_signed = \" ^ bool m.enum_are_signed ^ \", alignof_short = \" ^ int m.alignof_short ^ \", alignof_int = \" ^ int m.alignof_int ^ \", alignof_long = \" ^ int m.alignof_long ^ \", alignof_longlong = \" ^ int m.alignof_longlong ^ \", alignof_ptr = \" ^ int m.alignof_ptr ^ \", alignof_enum = \" ^ int m.alignof_enum ^ \", alignof_float = \" ^ int m.alignof_float ^ \", alignof_double = \" ^ int m.alignof_double ^ \", alignof_longdouble = \" ^ int m.alignof_longdouble ^ \", alignof_str = \" ^ int m.alignof_str ^ \", alignof_fun = \" ^ int m.alignof_fun ^ \", alignof_char_array = \" ^ int m.alignof_char_array ^ \", char_is_unsigned = \" ^ bool m.char_is_unsigned ^ \", const_string_literals = \" ^ bool m.const_string_literals ^ \", little_endian = \" ^ bool m.little_endian ^ \" }\"\n\nlet run () =\n File.init_from_cmdline ();\n print_endline (file (Ast.get ()))\n\nmodule Self =\n Plugin.Register\n (struct\n let name = \"dumpcil\"\n let shortname = \"dumpcil\"\n let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\"\n end);;\n\nmodule Enabled =\n Self.False\n (struct\n let option_name = \"-dumpcil\"\n let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\"\n end);;\n\nlet () = Db.Main.extend (fun () -> if Enabled.get () then run ())\n"
- putStrLn "running 'make' to compile dumpcil plugin ..."
- system "cd install-dumpcil-plugin && make"
- putStrLn "running 'make install' to install dumpcil plugin ..."
- system "cd install-dumpcil-plugin && make install"
- return ()
+ CExpr (Just (CCall func args _)) n -> StmtApply (Apply (cExpr func) (map cExpr args)) $ posOf n
-data Exn = Exn deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Position = Position FilePath Int Int deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Int64 = Int64 deriving (Show, Read, Eq) {-! derive : Parse !-}
+ CExpr (Just (CUnary op a n1)) n2
+ | elem op [CPreIncOp, CPostIncOp] -> cStat $ CExpr (Just (CAssign CAddAssOp a one n1)) n2
+ | elem op [CPreDecOp, CPostDecOp] -> cStat $ CExpr (Just (CAssign CSubAssOp a one n1)) n2
+ where
+ one = CConst $ CIntConst (cInteger 1) n1
-data BitsSizeofTyp = Not_Computed | Not_Computable (Exn) | Computed (Int) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data BitsSizeofTypCache = BitsSizeofTypCache { scache :: BitsSizeofTyp } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Termination_kind = Normal | Exits | Breaks | Continues | Returns deriving (Show, Read, Eq) {-! derive : Parse !-}
-data File = File { fileName :: String, globals :: [Global], globinit :: Maybe (Fundec), globinitcalled :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Global = GType (Typeinfo) (Location) | GCompTag (Compinfo) (Location) | GCompTagDecl (Compinfo) (Location) | GEnumTag (Enuminfo) (Location) | GEnumTagDecl (Enuminfo) (Location) | GVarDecl (Funspec) (Varinfo) (Location) | GVar (Varinfo) (Initinfo) (Location) | GFun (Fundec) (Location) | GAsm (String) (Location) | GPragma (Attribute) (Location) | GText (String) | GAnnot (Global_annotation) (Location) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Typ = TVoid (Attributes) | TInt (Ikind) (Attributes) | TFloat (Fkind) (Attributes) | TPtr (Typ) (Attributes) | TArray (Typ) (Maybe (Exp)) (BitsSizeofTypCache) (Attributes) | TFun (Typ) (Maybe ([(String, Typ, Attributes)])) (Bool) (Attributes) | TNamed (Typeinfo) (Attributes) | TComp (Compinfo) (BitsSizeofTypCache) (Attributes) | TEnum (Enuminfo) (Attributes) | TBuiltin_va_list (Attributes) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Ikind = IBool | IChar | ISChar | IUChar | IInt | IUInt | IShort | IUShort | ILong | IULong | ILongLong | IULongLong deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Fkind = FFloat | FDouble | FLongDouble deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Attribute = Attr (String) ([Attrparam]) | AttrAnnot (String) deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Attributes = [Attribute]
-data Attrparam = AInt (Int) | AStr (String) | ACons (String) ([Attrparam]) | ASizeOf (Typ) | ASizeOfE (Attrparam) | ASizeOfS (Typsig) | AAlignOf (Typ) | AAlignOfE (Attrparam) | AAlignOfS (Typsig) | AUnOp (Unop) (Attrparam) | ABinOp (Binop) (Attrparam) (Attrparam) | ADot (Attrparam) (String) | AStar (Attrparam) | AAddrOf (Attrparam) | AIndex (Attrparam) (Attrparam) | AQuestion (Attrparam) (Attrparam) (Attrparam) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Compinfo = Compinfo { cstruct :: Bool, cname :: String, ckey :: Int, cfields :: [Fieldinfo], cattr :: Attributes, cdefined :: Bool, creferenced :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Fieldinfo = Fieldinfo { fcomp :: Compinfo, fname :: String, ftype :: Typ, fbitfield :: Maybe (Int), fattr :: Attributes, floc :: Location, faddrof :: Bool, fsize_in_bits :: Maybe (Int), foffset_in_bits :: Maybe (Int), fpadding_in_bits :: Maybe (Int) } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Enuminfo = Enuminfo { ename :: String, eitems :: [Enumitem], eattr :: Attributes, ereferenced :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Enumitem = Enumitem { einame :: String, eival :: Exp, eihost :: Enuminfo, eiloc :: Location } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Typeinfo = Typeinfo { tname :: String, ttype :: Typ, treferenced :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Varinfo = Varinfo { vname :: String, vorig_name :: String, vtype :: Typ, vattr :: Attributes, vstorage :: Storage, vglob :: Bool, vdefined :: Bool, vformal :: Bool, vinline :: Bool, vdecl :: Location, vid :: Int, vaddrof :: Bool, vreferenced :: Bool, vgenerated :: Bool, vdescr :: Maybe (String), vdescrpure :: Bool, vghost :: Bool, vlogic :: Bool, vlogic_var_assoc :: Maybe (Logic_var) } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Storage = NoStorage | Static | Register | Extern deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Exp = Exp { eid :: Int, enode :: Exp_node } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Exp_node = Const (Constant) | Lval (Lval) | SizeOf (Typ) | SizeOfE (Exp) | SizeOfStr (String) | AlignOf (Typ) | AlignOfE (Exp) | UnOp (Unop) (Exp) (Typ) | BinOp (Binop) (Exp) (Exp) (Typ) | CastE (Typ) (Exp) | AddrOf (Lval) | StartOf (Lval) | Info (Exp) (Exp_info) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Exp_info = Exp_info { exp_loc :: Location, exp_type :: Logic_type, exp_name :: [String] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Constant = CInt64 (Int64) (Ikind) (Maybe (String)) | CStr (String) | CWStr ([Int64]) | CChr (Char) | CReal (Float) (Fkind) (Maybe (String)) | CEnum (Enumitem) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Unop = Neg | BNot | LNot deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Binop = PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP | Mult | Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Lval = (Lhost, Offset)
-data Lhost = Var (Varinfo) | Mem (Exp) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Offset = NoOffset | Field (Fieldinfo) (Offset) | Index (Exp) (Offset) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Init = SingleInit (Exp) | CompoundInit (Typ) ([(Offset, Init)]) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Initinfo = Initinfo { init :: Maybe (Init) } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Fundec = Fundec { svar :: Varinfo, sformals :: [Varinfo], slocals :: [Varinfo], smaxid :: Int, sbody :: Block, smaxstmtid :: Maybe (Int), sallstmts :: [Stmt], sspec :: Funspec } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Block = Block { battrs :: Attributes, blocals :: [Varinfo], bstmts :: [Stmt] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Stmt = Stmt { labels :: [Label], skind :: Stmtkind, sid :: Int, succs :: [Stmt], preds :: [Stmt], ghost :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Label = Label (String) (Location) (Bool) | Case (Exp) (Location) | Default (Location) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Stmtkind = Instr (Instr) | Return (Maybe (Exp)) (Location) | Goto (Stmt) (Location) | Break (Location) | Continue (Location) | If (Exp) (Block) (Block) (Location) | Switch (Exp) (Block) ([Stmt]) (Location) | Loop ([Code_annotation]) (Block) (Location) (Maybe (Stmt)) (Maybe (Stmt)) | Block' (Block) | UnspecifiedSequence ([(Stmt, [Lval], [Lval], [Lval])]) | TryFinally (Block) (Block) (Location) | TryExcept (Block) (([Instr], Exp)) (Block) (Location) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Instr = Set (Lval) (Exp) (Location) | Call (Maybe (Lval)) (Exp) ([Exp]) (Location) | Asm (Attributes) ([String]) ([(Maybe (String), String, Lval)]) ([(Maybe (String), String, Exp)]) ([String]) (Location) | Skip (Location) | Code_annot (Code_annotation) (Location) deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Location = (Position, Position)
-data Typsig = TSArray (Typsig) (Maybe (Int64)) ([Attribute]) | TSPtr (Typsig) ([Attribute]) | TSComp (Bool) (String) ([Attribute]) | TSFun (Typsig) ([Typsig]) (Bool) ([Attribute]) | TSEnum (String) ([Attribute]) | TSBase (Typ) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_type = Ctype (Typ) | Ltype (Logic_type_info) ([Logic_type]) | Lvar (String) | Linteger | Lreal | Larrow ([Logic_type]) (Logic_type) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Identified_term = Identified_term { it_id :: Int, it_content :: Term } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_label = StmtLabel (Stmt) | LogicLabel (String) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Term = Term { term_node :: Term_node, term_loc :: (Position, Position), term_type :: Logic_type, term_name :: [String] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Term_node = TConst (Constant) | TLval (Term_lval) | TSizeOf (Typ) | TSizeOfE (Term) | TSizeOfStr (String) | TAlignOf (Typ) | TAlignOfE (Term) | TUnOp (Unop) (Term) | TBinOp (Binop) (Term) (Term) | TCastE (Typ) (Term) | TAddrOf (Term_lval) | TStartOf (Term_lval) | Tapp (Logic_info) ([(Logic_label, Logic_label)]) ([Term]) | Tlambda (Quantifiers) (Term) | TDataCons (Logic_ctor_info) ([Term]) | Tif (Term) (Term) (Term) | Told (Term) | Tat (Term) (Logic_label) | Tbase_addr (Term) | Tblock_length (Term) | Tnull | TCoerce (Term) (Typ) | TCoerceE (Term) (Term) | TUpdate (Term) (Fieldinfo) (Term) | Ttypeof (Term) | Ttype (Typ) | Tempty_set | Tunion ([Term]) | Tinter ([Term]) | Tcomprehension (Term) (Quantifiers) (Maybe (Named (Predicate))) | Trange (Maybe (Term)) (Maybe (Term)) | Tlet (Logic_info) (Term) deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Term_lval = (Term_lhost, Term_offset)
-data Term_lhost = TVar (Logic_var) | TResult (Typ) | TMem (Term) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Term_offset = TNoOffset | TField (Fieldinfo) (Term_offset) | TIndex (Term) (Term_offset) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_info = Logic_info { l_var_info :: Logic_var, l_labels :: [Logic_label], l_tparams :: [String], l_type :: Maybe (Logic_type), l_profile :: [Logic_var], l_body :: Logic_body } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Builtin_logic_info = Builtin_logic_info { bl_name :: String, bl_labels :: [Logic_label], bl_params :: [String], bl_type :: Maybe (Logic_type), bl_profile :: [(String, Logic_type)] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_body = LBnone | LBreads ([Identified_term]) | LBterm (Term) | LBpred (Named (Predicate)) | LBinductive ([(String, [Logic_label], [String], Named (Predicate))]) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_type_info = Logic_type_info { lt_name :: String, lt_params :: [String], lt_def :: Maybe (Logic_type_def) } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_type_def = LTsum ([Logic_ctor_info]) | LTsyn (Logic_type) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_var = Logic_var { lv_name :: String, lv_id :: Int, lv_type :: Logic_type, lv_origin :: Maybe (Varinfo) } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Logic_ctor_info = Logic_ctor_info { ctor_name :: String, ctor_type :: Logic_type_info, ctor_params :: [Logic_type] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Quantifiers = [Logic_var]
-data Relation = Rlt | Rgt | Rle | Rge | Req | Rneq deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Predicate = Pfalse | Ptrue | Papp (Logic_info) ([(Logic_label, Logic_label)]) ([Term]) | Pseparated ([Term]) | Prel (Relation) (Term) (Term) | Pand (Named (Predicate)) (Named (Predicate)) | Por (Named (Predicate)) (Named (Predicate)) | Pxor (Named (Predicate)) (Named (Predicate)) | Pimplies (Named (Predicate)) (Named (Predicate)) | Piff (Named (Predicate)) (Named (Predicate)) | Pnot (Named (Predicate)) | Pif (Term) (Named (Predicate)) (Named (Predicate)) | Plet (Logic_info) (Named (Predicate)) | Pforall (Quantifiers) (Named (Predicate)) | Pexists (Quantifiers) (Named (Predicate)) | Pold (Named (Predicate)) | Pat (Named (Predicate)) (Logic_label) | Pvalid (Term) | Pvalid_index (Term) (Term) | Pvalid_range (Term) (Term) (Term) | Pfresh (Term) | Psubtype (Term) (Term) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Identified_predicate = Identified_predicate { ip_name :: [String], ip_loc :: Location, ip_id :: Int, ip_content :: Predicate } deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Variant term = (term, Maybe (String))
-data Zone locs = Location (locs) | Nothing' deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Assigns locs = (Zone (locs), [Zone (locs)])
-data Named a = Named { name :: [String], loc :: Location, content :: a } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Spec term pred locs = Spec { spec_requires :: [pred], spec_behavior :: [Behavior (pred) (locs)], spec_variant :: Maybe (Variant (term)), spec_terminates :: Maybe (pred), spec_complete_behaviors :: [[String]], spec_disjoint_behaviors :: [[String]] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Behavior pred locs = Behavior { b_name :: String, b_assumes :: [pred], b_post_cond :: [(Termination_kind, pred)], b_assigns :: [Assigns (locs)] } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Loop_pragma term = Unroll_level (term) | Widen_hints ([term]) | Widen_variables ([term]) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Slice_pragma term = SPexpr (term) | SPctrl | SPstmt deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Impact_pragma term = IPexpr (term) | IPstmt deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Pragma term = Loop_pragma (Loop_pragma (term)) | Slice_pragma (Slice_pragma (term)) | Impact_pragma (Impact_pragma (term)) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Validity = True' | False' | Maybe deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Annot_checked_status = Annot_checked_status { emitter :: String, valid :: Validity } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Annotation_status = Unknown | Checked (Annot_checked_status) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Annot_status = Annot_status { status :: Annotation_status } deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Code_annot term pred spec_pred locs = AAssert ([String]) (pred) (Annot_status) | AStmtSpec (Spec (term) (spec_pred) (locs)) | AInvariant ([String]) (Bool) (pred) | AVariant (Variant (term)) | AAssigns ([String]) (Assigns (locs)) | APragma (Pragma (term)) deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Funspec = Spec (Term) (Identified_predicate) (Identified_term)
-data Code_annotation = Code_annotation { annot_content :: Code_annot (Term) (Named (Predicate)) (Identified_predicate) (Identified_term), annot_id :: Int } deriving (Show, Read, Eq) {-! derive : Parse !-}
-type Funbehavior = Behavior (Identified_predicate) (Identified_term)
-data Global_annotation = Dfun_or_pred (Logic_info) | Daxiomatic (String) ([Global_annotation]) | Dtype (Logic_type_info) | Dlemma (String) (Bool) ([Logic_label]) ([String]) (Named (Predicate)) | Dinvariant (Logic_info) | Dtype_annot (Logic_info) deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Kinstr = Kstmt (Stmt) | Kglobal deriving (Show, Read, Eq) {-! derive : Parse !-}
-data Mach = Mach { version_major :: Int, version_minor :: Int, version :: String, underscore_name :: Bool, sizeof_short :: Int, sizeof_int :: Int, sizeof_long :: Int, sizeof_longlong :: Int, sizeof_ptr :: Int, sizeof_enum :: Int, sizeof_float :: Int, sizeof_double :: Int, sizeof_longdouble :: Int, sizeof_void :: Int, sizeof_fun :: Int, size_t :: String, wchar_t :: String, ptrdiff_t :: String, enum_are_signed :: Bool, alignof_short :: Int, alignof_int :: Int, alignof_long :: Int, alignof_longlong :: Int, alignof_ptr :: Int, alignof_enum :: Int, alignof_float :: Int, alignof_double :: Int, alignof_longdouble :: Int, alignof_str :: Int, alignof_fun :: Int, alignof_char_array :: Int, char_is_unsigned :: Bool, const_string_literals :: Bool, little_endian :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-}
+ _ -> notSupported a "statement"
+ where
+ p = posOf a
+
+cExpr :: CExpr -> Expr
+cExpr a = case a of
+ CConst (CIntConst i _) -> ConstInt (fromIntegral $ getCInteger i) p
+ CConst (CFloatConst (CFloat s) _) -> ConstFloat (read s) p
+ CConst (CCharConst (CChar a _) _) -> ConstChar a p
+ CConst (CStrConst (CString a _) _) -> ConstString a p
+ CVar (Ident name _ _) _ -> Var name p
+ CBinary CMulOp a b _ -> Mul (cExpr a) (cExpr b) p
+ CBinary CDivOp a b _ -> Div (cExpr a) (cExpr b) p
+ CBinary CRmdOp a b _ -> Rmd (cExpr a) (cExpr b) p
+ CBinary CAddOp a b _ -> Add (cExpr a) (cExpr b) p
+ CBinary CSubOp a b _ -> Sub (cExpr a) (cExpr b) p
+ CBinary CShlOp a b _ -> Shl (cExpr a) (cExpr b) p
+ CBinary CShrOp a b _ -> Shr (cExpr a) (cExpr b) p
+ CBinary CLeOp a b _ -> Lt (cExpr a) (cExpr b) p
+ CBinary CGrOp a b _ -> Gt (cExpr a) (cExpr b) p
+ CBinary CLeqOp a b _ -> Le (cExpr a) (cExpr b) p
+ CBinary CGeqOp a b _ -> Ge (cExpr a) (cExpr b) p
+ CBinary CEqOp a b _ -> Eq (cExpr a) (cExpr b) p
+ CBinary CNeqOp a b _ -> Neq (cExpr a) (cExpr b) p
+ CBinary CAndOp a b _ -> And (cExpr a) (cExpr b) p
+ CBinary CXorOp a b _ -> Xor (cExpr a) (cExpr b) p
+ CBinary COrOp a b _ -> Or (cExpr a) (cExpr b) p
+ CUnary CAdrOp a _ -> Adr (cExpr a) p
+ CUnary CIndOp a _ -> Ind (cExpr a) p
+ CUnary CMinOp a _ -> Minus (cExpr a) p
+ CUnary CCompOp a _ -> Comp (cExpr a) p
+ CUnary CNegOp a _ -> Neg (cExpr a) p
+ CCast decl a _ -> Cast (cDeclType decl) (cExpr a) p
+ CIndex a b _ -> Index (cExpr a) (cExpr b) p
+ CCall func args _ -> ExprApply (Apply (cExpr func) (map cExpr args)) p
+ CMember a (Ident name _ _) False _ -> Mem (cExpr a) name p
+ CMember a (Ident name _ _) True _ -> MemInd (cExpr a) name p
+ CSizeofType a _ -> SizeT (cDeclType a) p
+ CSizeofExpr a _ -> SizeE (cExpr a) p
+ _ -> notSupported a "expressions"
+ where
+ p = posOf a
+
+cBlockItem :: CBlockItem -> Stmt
+cBlockItem a = case a of
+ CBlockStmt a -> cStat a
+ CBlockDecl a -> cDecl a
+ CNestedFunDef a -> cFunDef a
+
+cDecl :: CDecl -> Stmt
+cDecl a = case a of
+ CDecl [CTypeSpec (CSUType (CStruct CStructTag (Just (Ident name _ _)) (Just decls) [] _) _)] [] _ -> TypeDecl name (structOrBitField decls) p
+ CDecl [CTypeSpec (CSUType (CStruct CUnionTag (Just (Ident name _ _)) (Just decls) [] _) _)] [] _ -> TypeDecl name (Union $ map field decls) p
+ CDecl [CTypeSpec (CEnumType (CEnum (Just (Ident name _ _)) (Just enums) [] _) _)] [] _ -> TypeDecl name (Enum [ (field, fromIntegral $ getCInteger i) | (Ident field _ _, Just (CConst (CIntConst i _))) <- enums ]) p
+ CDecl (CStorageSpec (CTypedef _) : specs) a n -> TypeDecl name (Typedef $ cDeclType $ CDecl specs (init a) n) p
+ where
+ (Just (CDeclr (Just (Ident name _ _)) [] Nothing [] _), Nothing, Nothing) = last a
+ CDecl _ [(Just (CDeclr _ (CFunDeclr _ _ _ : _) _ _ _), _, _)] _ -> Null -- Ignore function prototypes.
+ CDecl specs [(Just (CDeclr (Just (Ident name _ _)) _ Nothing [] _), init , Nothing)] _
+ | any isExtern specs -> Null -- Ignore external variable decls.
+ | otherwise -> case init of
+ Nothing -> VariableDef name (cDeclType a) Nothing p
+ Just init -> VariableDef name (cDeclType a) (Just $ cInit init) p
+ where
+ isExtern (CStorageSpec (CExtern _)) = True
+ isExtern _ = False
+ _ -> notSupported a "declaration"
+ where
+ p = posOf a
+
+cInit :: CInit -> Init
+cInit a = case a of
+ CInitExpr init _ -> Init $ cExpr init
+ CInitList a _ | all null $ fst $ unzip a -> InitList [ cInit a | ([], a) <- a ]
+ _ -> notSupported a "initializer"
+
+
+-- | A struct or a bit field.
+structOrBitField :: [CDecl] -> Type
+structOrBitField decls
+ | all isField decls = Struct $ map field decls
+ | all isBitField decls = BitField typ $ map f decls
+ | otherwise = notSupported (head decls) "inconsistent fields"
+ where
+ isField (CDecl _ [(Just (CDeclr (Just _) _ Nothing [] _), Nothing, Nothing)] _) = True
+ isField _ = False
+ typ = cDeclType $ head decls
+ isBitField d@(CDecl _ [(Just (CDeclr (Just _) _ Nothing [] _), Nothing, Just (CConst (CIntConst _ _)))] _) = cDeclType d == typ
+ isBitField _ = False
+ f :: CDecl -> (Name, Int)
+ f (CDecl _ [(Just (CDeclr (Just (Ident name _ _)) _ Nothing [] _), Nothing, Just (CConst (CIntConst cint _)))] _) = (name, fromIntegral $ getCInteger cint)
+ f a = notSupported a "bit field format"
+
+-- | Struct and union fields.
+field :: CDecl -> (Name, Type)
+field a = case a of
+ d@(CDecl _ [(Just (CDeclr (Just (Ident name _ _)) _ Nothing [] _), Nothing, Nothing)] _) -> (name, cDeclType d)
+ _ -> notSupported a "struct/union field"
+
+-- | A 'Type' from a 'CDecl'.
+cDeclType :: CDecl -> Type
+cDeclType a = case a of
+ CDecl specs [] _ -> cDeclSpec specs
+ CDecl specs [(Just (CDeclr _ derived Nothing [] _), _, _)] _ -> foldr cDerivedDeclr (cDeclSpec specs) derived
+ _ -> notSupported a "declaration type"
+
+cDeclSpec :: [CDeclSpec] -> Type
+cDeclSpec = cDeclSpec . sortBy f
+ where
+ f (CTypeQual _) _ = LT
+ f _ (CTypeQual _) = GT
+ f _ _ = EQ
+
+ cDeclSpec a = case a of
+ [] -> notSupported' a "empty type specification"
+ [CTypeSpec (CVoidType _)] -> Void
+ [CTypeSpec (CSUType (CStruct CStructTag (Just (Ident name _ _)) Nothing [] _) _)] -> StructRef name
+ [CTypeSpec (CSUType (CStruct CUnionTag (Just (Ident name _ _)) Nothing [] _) _)] -> UnionRef name
+ [CTypeSpec (CEnumType (CEnum (Just (Ident name _ _)) Nothing [] _) _)] -> EnumRef name
+ [CTypeSpec (CTypeDef (Ident name _ _) _)] -> TypedefRef name
+ CStorageSpec (CTypedef _) : a -> Typedef $ cDeclSpec a
+ CTypeQual (CVolatQual _) : a -> Volatile $ cDeclSpec a
+ CTypeQual _ : a -> cDeclSpec a -- Ignore other type qualifiers.
+ CStorageSpec _ : a -> cDeclSpec a -- Ignore storage specs.
+ CTypeSpec (CSignedType _) : a -> cDeclSpec a
+ CTypeSpec (CUnsigType _) : a -> case cDeclSpec a of
+ Int8 -> Word8
+ Int16 -> Word16
+ Int32 -> Word32
+ _ -> notSupported' a "type specification"
+ CTypeSpec (CCharType _) : _ -> Int8
+ CTypeSpec (CShortType _) : _ -> Int16
+ CTypeSpec (CLongType _) : _ -> Int32
+ CTypeSpec (CIntType _) : _ -> Int32
+ CTypeSpec (CFloatType _) : _ -> Float
+ CTypeSpec (CDoubleType _) : _ -> Double
+ _ -> notSupported' a "type specification"
+
+cDerivedDeclr :: CDerivedDeclr -> Type -> Type
+cDerivedDeclr a t = case a of
+ CPtrDeclr quals _ -> volatile quals $ Ptr t
+ CArrDeclr quals (CArrSize _ (CConst (CIntConst i _))) _ -> volatile quals $ Array (fromIntegral $ getCInteger i) t
+ CFunDeclr (Right (decls, False)) [] _ -> Function t $ map cDeclType decls
+ _ -> notSupported' a "derived declaration"
+ where
+ volatile quals typ = if any isVolatile quals then Volatile typ else typ
+ isVolatile (CVolatQual _) = True
+ isVolatile _ = False
+
+cFunDef :: CFunDef -> Stmt
+cFunDef (CFunDef specs (CDeclr (Just (Ident name _ _)) (CFunDeclr (Right (args', False)) [] _ : rest) Nothing [] _) [] stat n) = FunctionDef name (foldr cDerivedDeclr (cDeclSpec specs) rest) args (cStat stat) (posOf n)
+ where
+ args :: [(Name, Type)]
+ args = [ (name, cDeclType decl) | decl@(CDecl _ [(Just (CDeclr (Just (Ident name _ _)) _ Nothing [] _), Nothing, Nothing)] _) <- args' ]
+cFunDef a = notSupported a "function"
+-- FunctionDecl Type Name [Type] Stmt Position
+
+err :: (Pretty a, Pos a) => a -> String -> b
+err a m = error $ position a ++ ": " ++ m ++ ": " ++ show (pretty a)
+
+err' :: Pos a => a -> String -> b
+err' a m = error $ position a ++ ": " ++ m
+
+notSupported :: (Pretty a, Pos a) => a -> String -> b
+notSupported a m = err a $ "not supported: " ++ m
+
+notSupported' :: Pos a => a -> String -> b
+notSupported' a m = err' a $ "not supported: " ++ m
+
+-- | Format the file position of something with ties to the orignial source, like a 'Stmt' or 'Expr'.
+position :: Pos a => a -> String
+position a = f ++ ":" ++ show l ++ ":" ++ show c
+ where
+ Position f l c = posOf a
diff --git a/Makefile b/Makefile
deleted file mode 100644
--- a/Makefile
+++ /dev/null
@@ -1,24 +0,0 @@
-.PHONY: all
-all: Language/CIL.hs
-
-CIL.hs: GenCIL.hs
- runhaskell -W GenCIL.hs
-
-Language/CIL.hs: CIL.hs
- mkdir -p Language && cp CIL.hs Language/CIL.hs
-
-#DrIFT-cabalized -o Language/CIL.hs CIL.hs
-
-.PHONY: test
-test: Test.hs Language/CIL.hs
- runhaskell -W Test.hs
-
-.PHONY: clean
-clean:
- -rm *.o *.hi
- -rm Language/*.o Language/*.hi
- -rm cil_types_nocomments.mli
- -rm CIL.hs
- -rm -r Language
- -rm -rf install-dumpcil-plugin
-
diff --git a/cil.cabal b/cil.cabal
--- a/cil.cabal
+++ b/cil.cabal
@@ -1,12 +1,13 @@
name: cil
-version: 0.0.2
+version: 0.1.0
category: Language
-synopsis: An interface to CIL and ACSL through Frama-C.
+synopsis: An interface to CIL.
description:
- TODO
+ CIL (http://cil.sourceforge.net/) is a C frontend that reduces C to a manageable subset,
+ useful for source code analyzers, instrumenters, and compilers.
author: Tom Hawkins
maintainer: Tom Hawkins
@@ -19,24 +20,17 @@
build-type: Simple
cabal-version: >= 1.6
-extra-source-files:
- Makefile
- cil_types.mli
- GenCIL.hs
-
library
build-depends:
- base >= 4.0 && < 5.0,
- process >= 1.0.1 && < 1.1,
- polyparse >= 1.4
+ base >= 4.0 && < 5.0,
+ bytestring >= 0.9 && < 1.0,
+ language-c >= 0.3.2 && < 0.4
exposed-modules:
Language.CIL
- extensions: GADTs, EmptyDataDecls
+ extensions:
- if impl(ghc > 6.8)
- ghc-options: -fwarn-tabs
ghc-options: -W
source-repository head
diff --git a/cil_types.mli b/cil_types.mli
deleted file mode 100644
--- a/cil_types.mli
+++ /dev/null
@@ -1,1527 +0,0 @@
-(**************************************************************************)
-(* *)
-(* Copyright (C) 2001-2003 *)
-(* George C. Necula *)
-(* Scott McPeak *)
-(* Wes Weimer *)
-(* Ben Liblit *)
-(* 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. The names of the contributors may not be used to endorse or *)
-(* promote products derived from this software without specific prior *)
-(* written permission. *)
-(* *)
-(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
-(* "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 *)
-(* COPYRIGHT OWNER 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. *)
-(* *)
-(* File modified by CEA (Commissariat a l'energie atomique et aux *)
-(* energies alternatives). *)
-(**************************************************************************)
-
-(** The Abstract Syntax of CIL.
- @plugin development guide *)
-
-(**************************** WARNING ***************************************)
-(* Remember to reflect any change here into the visitor and pretty-printer *)
-(* in cil.ml. In particular, if a type becomes mutable, it is necessary to *)
-(* adapt the Cil.behavior type and the copy_behavior accordingly. *)
-(* A first test to see if something has been broken by a change is to launch*)
-(* ptests.byte -add-options '-files-debug "-check -copy"' *)
-(* In addition, it is a good idea to add some invariant checks in the *)
-(* check_file class in frama-c/src/file.ml (before lauching the tests) *)
-(****************************************************************************)
-
-(** This is used to cache the computation of the size of types in bits. *)
-type bitsSizeofTyp = Not_Computed | Not_Computable of exn | Computed of int
-type bitsSizeofTypCache = { mutable scache : bitsSizeofTyp}
-
-(** kind of termination a post-condition applies to. See ACSL manual. *)
-type termination_kind = Normal | Exits | Breaks | Continues | Returns
-
-(** The top-level representation of a CIL source file (and the result of the
- * parsing and elaboration). Its main contents is the list of global
- * declarations and definitions. You can iterate over the globals in a
- * {!Cil_types.file} using the following iterators: {!Cil.mapGlobals},
- * {!Cil.iterGlobals} and {!Cil.foldGlobals}. You can also use the
- * {!Cil.dummyFile} when you need a {!Cil_types.file} as a placeholder. For each
- * global item CIL stores the source location where it appears (using the
- * type {!Cil_types.location}) *)
-type file =
- { mutable fileName: string; (** The complete file name *)
- mutable globals: global list; (** List of globals as they will appear
- in the printed file *)
- mutable globinit: fundec option;
- (** An optional global initializer function. This is a function where
- * you can put stuff that must be executed before the program is
- * started. This function, is conceptually at the end of the file,
- * although it is not part of the globals list. Use {!Cil.getGlobInit}
- * to create/get one. *)
- mutable globinitcalled: bool;
- (** Whether the global initialization function is called in main. This
- should always be false if there is no global initializer. When
- you create a global initialization CIL will try to insert code in
- main to call it. *)
- }
-(** Top-level representation of a C source file.
- @plugin development guide *)
-
-(** The main type for representing global declarations and definitions. A list
- of these form a CIL file. The order of globals in the file is generally
- important.
- @plugin development guide *)
-and global =
- | GType of typeinfo * location
- (** A typedef. All uses of type names (through the [TNamed] constructor)
- must be preceeded in the file by a definition of the name. The string
- is the defined name and always not-empty. *)
-
- | GCompTag of compinfo * location
- (** Defines a struct/union tag with some fields. There must be one of
- these for each struct/union tag that you use (through the [TComp]
- constructor) since this is the only context in which the fields are
- printed. Consequently nested structure tag definitions must be
- broken into individual definitions with the innermost structure
- defined first. *)
-
- | GCompTagDecl of compinfo * location
- (** Declares a struct/union tag. Use as a forward declaration. This is
- * printed without the fields. *)
-
- | GEnumTag of enuminfo * location
- (** Declares an enumeration tag with some fields. There must be one of
- these for each enumeration tag that you use (through the [TEnum]
- constructor) since this is the only context in which the items are
- printed. *)
-
- | GEnumTagDecl of enuminfo * location
- (** Declares an enumeration tag. Use as a forward declaration. This is
- * printed without the items. *)
-
- | GVarDecl of funspec * varinfo * location
- (** A variable declaration (not a definition). If the variable has a
- function type then this is a prototype. There can be several
- declarations and at most one definition for a given variable. If both
- forms appear then they must share the same varinfo structure. A
- prototype shares the varinfo with the fundec of the definition. Either
- has storage Extern or there must be a definition in this file *)
-
- | GVar of varinfo * initinfo * location
- (** A variable definition. Can have an initializer. The initializer is
- * updateable so that you can change it without requiring to recreate
- * the list of globals. There can be at most one definition for a
- * variable in an entire program. Cannot have storage Extern or function
- * type. *)
-
-
- | GFun of fundec * location
- (** A function definition. *)
-
- | GAsm of string * location (** Global asm statement. These ones
- can contain only a template *)
- | GPragma of attribute * location (** Pragmas at top level. Use the same
- syntax as attributes *)
- | GText of string (** Some text (printed verbatim) at
- top level. E.g., this way you can
- put comments in the output. *)
- | GAnnot of global_annotation * location
- (** a global annotation. Can be
- - an axiom or a lemma
- - a predicate declaration or definition
- - a global type invariant
- - a global invariant
- - a logic function declaration or definition.
- *)
-
-(** {b Types}. A C type is represented in CIL using the type {!Cil_types.typ}.
- * Among types we differentiate the integral types (with different kinds
- * denoting the sign and precision), floating point types, enumeration types,
- * array and pointer types, and function types. Every type is associated with
- * a list of attributes, which are always kept in sorted order. Use
- * {!Cil.addAttribute} and {!Cil.addAttributes} to construct list of
- * attributes. If you want to inspect a type, you should use
- * {!Cil.unrollType} or {!Cil.unrollTypeDeep} to see through the uses of
- * named types. *)
-(** CIL is configured at build-time with the sizes and alignments of the
- * underlying compiler (GCC or MSVC). CIL contains functions that can compute
- * the size of a type (in bits) {!Cil.bitsSizeOf}, the alignment of a type
- * (in bytes) {!Cil.alignOf_int}, and can convert an offset into a start and
- * width (both in bits) using the function {!Cil.bitsOffset}. At the moment
- * these functions do not take into account the [packed] attributes and
- * pragmas. *)
-
-and typ =
- TVoid of attributes (** Void type. Also predefined as {!Cil.voidType} *)
- | TInt of ikind * attributes
- (** An integer type. The kind specifies the sign and width. Several
- * useful variants are predefined as {!Cil.intType}, {!Cil.uintType},
- * {!Cil.longType}, {!Cil.charType}. *)
-
- | TFloat of fkind * attributes
- (** A floating-point type. The kind specifies the precision. You can
- * also use the predefined constant {!Cil.doubleType}. *)
-
- | TPtr of typ * attributes
- (** Pointer type. Several useful variants are predefined as
- * {!Cil.charPtrType}, {!Cil.charConstPtrType} (pointer to a
- * constant character), {!Cil.voidPtrType},
- * {!Cil.intPtrType} *)
-
- | TArray of typ * exp option * bitsSizeofTypCache * attributes
- (** Array type. It indicates the base type and the array length. *)
-
- | TFun of typ * (string * typ * attributes) list option * bool * attributes
- (** Function type. Indicates the type of the result, the name, type
- * and name attributes of the formal arguments ([None] if no
- * arguments were specified, as in a function whose definition or
- * prototype we have not seen; [Some \[\]] means void). Use
- * {!Cil.argsToList} to obtain a list of arguments. The boolean
- * indicates if it is a variable-argument function. If this is the
- * type of a varinfo for which we have a function declaration then
- * the information for the formals must match that in the
- * function's sformals. Use {!Cil.setFormals}, or
- * {!Cil.setFunctionType}, or {!Cil.makeFormalVar} for this
- * purpose. *)
-
- | TNamed of typeinfo * attributes
- (** The use of a named type. All uses of the same type name must
- * share the typeinfo. Each such type name must be preceeded
- * in the file by a [GType] global. This is printed as just the
- * type name. The actual referred type is not printed here and is
- * carried only to simplify processing. To see through a sequence
- * of named type references, use {!Cil.unrollType}. The attributes
- * are in addition to those given when the type name was defined. *)
-
- | TComp of compinfo * bitsSizeofTypCache * attributes
- (** A reference to a struct or a union type. All references to the
- same struct or union must share the same compinfo among them and
- with a [GCompTag] global that preceeds all uses (except maybe
- those that are pointers to the composite type). The attributes
- given are those pertaining to this use of the type and are in
- addition to the attributes that were given at the definition of
- the type and which are stored in the compinfo. *)
-
- | TEnum of enuminfo * attributes
- (** A reference to an enumeration type. All such references must
- share the enuminfo among them and with a [GEnumTag] global that
- preceeds all uses. The attributes refer to this use of the
- enumeration and are in addition to the attributes of the
- enumeration itself, which are stored inside the enuminfo *)
-
- | TBuiltin_va_list of attributes
- (** This is the same as the gcc's type with the same name *)
-
-(** Various kinds of integers *)
-and ikind =
- IBool (** [_Bool] *)
- | IChar (** [char] *)
- | ISChar (** [signed char] *)
- | IUChar (** [unsigned char] *)
- | IInt (** [int] *)
- | IUInt (** [unsigned int] *)
- | IShort (** [short] *)
- | IUShort (** [unsigned short] *)
- | ILong (** [long] *)
- | IULong (** [unsigned long] *)
- | ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *)
- | IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft
- Visual C) *)
-
-(** Various kinds of floating-point numbers*)
-and fkind =
- FFloat (** [float] *)
- | FDouble (** [double] *)
- | FLongDouble (** [long double] *)
-
-(** {b Attributes.} *)
-
-and attribute =
- | Attr of string * attrparam list
-(** An attribute has a name and some optional parameters. The name should not
- * start or end with underscore. When CIL parses attribute names it will
- * strip leading and ending underscores (to ensure that the multitude of GCC
- * attributes such as const, __const and __const__ all mean the same thing.) *)
- | AttrAnnot of string
-
-(** Attributes are lists sorted by the attribute name. Use the functions
- * {!Cil.addAttribute} and {!Cil.addAttributes} to insert attributes in an
- * attribute list and maintain the sortedness. *)
-and attributes = attribute list
-
-(** The type of parameters of attributes *)
-and attrparam =
- | AInt of int (** An integer constant *)
- | AStr of string (** A string constant *)
- | ACons of string * attrparam list (** Constructed attributes. These
- are printed [foo(a1,a2,...,an)].
- The list of parameters can be
- empty and in that case the
- parentheses are not printed. *)
- | ASizeOf of typ (** A way to talk about types *)
- | ASizeOfE of attrparam
- | ASizeOfS of typsig (** Replacement for ASizeOf in type
- signatures. Only used for
- attributes inside typsigs.*)
- | AAlignOf of typ
- | AAlignOfE of attrparam
- | AAlignOfS of typsig
- | AUnOp of unop * attrparam
- | ABinOp of binop * attrparam * attrparam
- | ADot of attrparam * string (** a.foo **)
- | AStar of attrparam (** * a *)
- | AAddrOf of attrparam (** & a **)
- | AIndex of attrparam * attrparam (** a1[a2] *)
- | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **)
-
-
-(** {b Structures.} The {!Cil_types.compinfo} describes the definition of a
- * structure or union type. Each such {!Cil_types.compinfo} must be defined at the
- * top-level using the [GCompTag] constructor and must be shared by all
- * references to this type (using either the [TComp] type constructor or from
- * the definition of the fields.
-
- If all you need is to scan the definition of each
- * composite type once, you can do that by scanning all top-level [GCompTag].
-
- * Constructing a {!Cil_types.compinfo} can be tricky since it must contain fields
- * that might refer to the host {!Cil_types.compinfo} and furthermore the type of
- * the field might need to refer to the {!Cil_types.compinfo} for recursive types.
- * Use the {!Cil.mkCompInfo} function to create a {!Cil_types.compinfo}. You can
- * easily fetch the {!Cil_types.fieldinfo} for a given field in a structure with
- * {!Cil.getCompField}. *)
-
-(** The definition of a structure or union type. Use {!Cil.mkCompInfo} to
- * make one and use {!Cil.copyCompInfo} to copy one (this ensures that a new
- * key is assigned and that the fields have the right pointers to parents.).
- @plugin development guide *)
-and compinfo = {
- mutable cstruct: bool;
- (** True if struct, False if union *)
- mutable cname: string;
- (** The name. Always non-empty. Use {!Cil.compFullName} to get the full
- * name of a comp (along with the struct or union) *)
- mutable ckey: int;
- (** A unique integer. This is assigned by {!Cil.mkCompInfo} using a
- * global variable in the Cil module. Thus two identical structs in two
- * different files might have different keys. Use {!Cil.copyCompInfo} to
- * copy structures so that a new key is assigned. *)
- mutable cfields: fieldinfo list;
- (** Information about the fields. Notice that each fieldinfo has a
- * pointer back to the host compinfo. This means that you should not
- * share fieldinfo's between two compinfo's *)
- mutable cattr: attributes;
- (** The attributes that are defined at the same time as the composite
- * type. These attributes can be supplemented individually at each
- * reference to this [compinfo] using the [TComp] type constructor. *)
- mutable cdefined: bool;
- (** This boolean flag can be used to distinguish between structures
- that have not been defined and those that have been defined but have
- no fields (such things are allowed in gcc). *)
- mutable creferenced: bool;
- (** True if used. Initially set to false. *)
- }
-
-(** {b Structure fields.} The {!Cil_types.fieldinfo} structure is used to describe
- * a structure or union field. Fields, just like variables, can have
- * attributes associated with the field itself or associated with the type of
- * the field (stored along with the type of the field). *)
-
-(** Information about a struct/union field.
- @plugin development guide *)
-and fieldinfo = {
- mutable fcomp: compinfo;
- (** The host structure that contains this field. There can be only one
- * [compinfo] that contains the field. *)
- mutable fname: string;
- (** The name of the field. Might be the value of {!Cil.missingFieldName}
- * in which case it must be a bitfield and is not printed and it does not
- * participate in initialization *)
- mutable ftype: typ;
- (** The type *)
- mutable fbitfield: int option;
- (** If a bitfield then ftype should be an integer type and the width of
- * the bitfield must be 0 or a positive integer smaller or equal to the
- * width of the integer type. A field of width 0 is used in C to control
- * the alignment of fields. *)
- mutable fattr: attributes;
- (** The attributes for this field (not for its type) *)
- mutable floc: location;
- (** The location where this field is defined *)
- mutable faddrof: bool;
- (** Adapted from CIL [vaddrof] field for variables. Only set for
- * non-array fields. Variable whose field address is taken is not marked
- * anymore as having its own address taken.
- * True if the address of this field is taken. CIL will set these
- * flags when it parses C, but you should make sure to set the flag
- * whenever your transformation create [AddrOf] expression. *)
- mutable fsize_in_bits: int option;
- (** Similar to [fbitfield] for all types of fields. Useful when
- * the type of the field is changed in the analyzer, to recall the size
- * of the original field.
- @deprecated only Jessie uses this
- *)
- mutable foffset_in_bits: int option;
- (** Store the offset at which the field starts in the structure.
- @deprecated only Jessie uses this *)
- mutable fpadding_in_bits: int option;
- (** Store the size of the padding that follows the field, if any.
- @deprecated only Jessie uses this *)
-}
-
-
-
-(** {b Enumerations.} Information about an enumeration. This is shared by all
- * references to an enumeration. Make sure you have a [GEnumTag] for each
- * of these. *)
-
-(** Information about an enumeration.
- @plugin development guide *)
-and enuminfo = {
- mutable ename: string;
- (** The name. Always non-empty. *)
- mutable eitems: enumitem list;
- (** Items. The list must be non-empty *)
- mutable eattr: attributes;
- (** The attributes that are defined at the same time as the enumeration
- * type. These attributes can be supplemented individually at each
- * reference to this [enuminfo] using the [TEnum] type constructor. *)
- mutable ereferenced: bool;
- (** True if used. Initially set to false*)
-}
-
-and enumitem =
- { mutable einame: string; (** the name, always non-empty. *)
- mutable eival: exp; (** value of the item.
- Must be a compile-time constant *)
- mutable eihost: enuminfo; (** the host enumeration in which the
- item is declared. *)
- eiloc: location;
- }
-
-(** Information about a defined type.
- @plugin development guide *)
-and typeinfo = {
- mutable tname: string;
- (** The name. Can be empty only in a [GType] when introducing a composite
- * or enumeration tag. If empty cannot be refered to from the file *)
- mutable ttype: typ;
- (** The actual type. This includes the attributes that were present in
- * the typedef *)
- mutable treferenced: bool;
- (** True if used. Initially set to false*)
-}
-
-(** {b Variables.}
- Each local or global variable is represented by a unique {!Cil_types.varinfo}
-structure. A global {!Cil_types.varinfo} can be introduced with the [GVarDecl] or
-[GVar] or [GFun] globals. A local varinfo can be introduced as part of a
-function definition {!Cil_types.fundec}.
-
- All references to a given global or local variable must refer to the same
-copy of the [varinfo]. Each [varinfo] has a globally unique identifier that
-can be used to index maps and hashtables (the name can also be used for this
-purpose, except for locals from different functions). This identifier is
-constructor using a global counter.
-
- It is very important that you construct [varinfo] structures using only one
- of the following functions:
-- {!Cil.makeGlobalVar} : to make a global variable
-- {!Cil.makeTempVar} : to make a temporary local variable whose name
-will be generated so that to avoid conflict with other locals.
-- {!Cil.makeLocalVar} : like {!Cil.makeTempVar} but you can specify the
-exact name to be used.
-- {!Cil.copyVarinfo}: make a shallow copy of a varinfo assigning a new name
-and a new unique identifier
-
- A [varinfo] is also used in a function type to denote the list of formals.
-
-*)
-
-(** Information about a variable.
- @plugin development guide *)
-and varinfo = {
- mutable vname: string;
- (** The name of the variable. Cannot be empty. It is primarily your
- * responsibility to ensure the uniqueness of a variable name. For local
- * variables {!Cil.makeTempVar} helps you ensure that the name is unique.
- *)
-
- vorig_name: string;
- (** the original name of the variable. Need not be unique. *)
-
- mutable vtype: typ;
- (** The declared type of the variable. *)
-
- mutable vattr: attributes;
- (** A list of attributes associated with the variable.*)
- mutable vstorage: storage;
- (** The storage-class *)
-
- mutable vglob: bool;
- (** True if this is a global variable*)
-
- mutable vdefined: bool;
- (** True if the variable or function is defined in the file.
- * Only relevant for functions and global variables.
- * Not used in particular for local variables and logic variables. *)
-
- mutable vformal: bool;
- (** True if the variable is a formal parameter of a function. *)
-
- mutable vinline: bool;
- (** Whether this varinfo is for an inline function. *)
-
- mutable vdecl: location;
- (** Location of variable declaration. *)
-
- mutable vid: int;
- (** A unique integer identifier. This field will be
- * set for you if you use one of the {!Cil.makeFormalVar},
- * {!Cil.makeLocalVar}, {!Cil.makeTempVar}, {!Cil.makeGlobalVar}, or
- * {!Cil.copyVarinfo}. *)
-
- mutable vaddrof: bool;
- (** True if the address of this variable is taken. CIL will set these
- * flags when it parses C, but you should make sure to set the flag
- * whenever your transformation create [AddrOf] expression. *)
-
- mutable vreferenced: bool;
- (** True if this variable is ever referenced. This is computed by
- * [removeUnusedVars]. It is safe to just initialize this to False *)
-
- vgenerated: bool;
- (** true for temporary variables generated by CIL normalization.
- false for variables coming directly from user input.
- *)
-
- mutable vdescr: string option; (** For most temporary variables, a
- description of what the var holds.
- (e.g. for temporaries used for
- function call results, this string
- is a representation of the function
- call.) *)
-
- mutable vdescrpure: bool; (** Indicates whether the vdescr above
- is a pure expression or call.
- True for all CIL expressions and
- Lvals, but false for e.g. function
- calls.
- Printing a non-pure vdescr more
- than once may yield incorrect
- results. *)
-
- mutable vghost: bool; (** Indicates if the variable is declared in ghost code *)
-
- vlogic: bool;
- (** False if this variable is a C variable. *)
-
- mutable vlogic_var_assoc: logic_var option
- (** logic variable representing this variable in the logic world*)
-}
-
-(** Storage-class information *)
-and storage =
- NoStorage (** The default storage. Nothing is printed *)
- | Static
- | Register
- | Extern
-
-
-(** {b Expressions.} The CIL expression language contains only the side-effect free expressions of
-C. They are represented as the type {!Cil_types.exp}. There are several
-interesting aspects of CIL expressions:
-
- Integer and floating point constants can carry their textual representation.
-This way the integer 15 can be printed as 0xF if that is how it occurred in the
-source.
-
- CIL uses 64 bits to represent the integer constants and also stores the width
-of the integer type. Care must be taken to ensure that the constant is
-representable with the given width. Use the functions {!Cil.kinteger},
-{!Cil.kinteger64} and {!Cil.integer} to construct constant
-expressions. CIL predefines the constants {!Cil.zero},
-{!Cil.one} and {!Cil.mone} (for -1).
-
- Use the functions {!Cil.isConstant} and {!Cil.isInteger} to test if
-an expression is a constant and a constant integer respectively.
-
- CIL keeps the type of all unary and binary expressions. You can think of that
-type qualifying the operator. Furthermore there are different operators for
-arithmetic and comparisons on arithmetic types and on pointers.
-
- Another unusual aspect of CIL is that the implicit conversion between an
-expression of array type and one of pointer type is made explicit, using the
-[StartOf] expression constructor (which is not printed). If you apply the
-[AddrOf}]constructor to an lvalue of type [T] then you will be getting an
-expression of type [TPtr(T)].
-
- You can find the type of an expression with {!Cil.typeOf}.
-
- You can perform constant folding on expressions using the function
-{!Cil.constFold}.
-*)
-
-(** Expressions (Side-effect free)*)
-and exp = { eid: int; (** unique identifier *)
- enode: exp_node; (** the expression itself *)
- }
-
-and exp_node =
- Const of constant (** Constant *)
- | Lval of lval (** Lvalue *)
- | SizeOf of typ
- (** sizeof(). Has [unsigned int] type (ISO 6.5.3.4). This is not
- * turned into a constant because some transformations might want to
- * change types *)
-
- | SizeOfE of exp
- (** sizeof() *)
-
- | SizeOfStr of string
- (** sizeof(string_literal). We separate this case out because this is the
- * only instance in which a string literal should not be treated as
- * having type pointer to character. *)
-
- | AlignOf of typ
- (** This corresponds to the GCC __alignof_. Has [unsigned int] type *)
- | AlignOfE of exp
-
-
- | UnOp of unop * exp * typ
- (** Unary operation. Includes the type of the result. *)
-
- | BinOp of binop * exp * exp * typ
- (** Binary operation. Includes the type of the result. The arithmetic
- * conversions are made explicit for the arguments. *)
-
- | CastE of typ * exp
- (** Use {!Cil.mkCast} to make casts. *)
-
- | AddrOf of lval
- (** Always use {!Cil.mkAddrOf} to construct one of these. Apply to an
- * lvalue of type [T] yields an expression of type [TPtr(T)] *)
-
- | StartOf of lval
- (** Conversion from an array to a pointer to the beginning of the array.
- * Given an lval of type [TArray(T)] produces an expression of type
- * [TPtr(T)]. In C this operation is implicit, the [StartOf] operator is
- * not printed. We have it in CIL because it makes the typing rules
- * simpler. *)
-
- | Info of exp * exp_info
- (** Additional information on the underlying expression *)
-
-(** Additional information on an expression *)
-and exp_info = {
- exp_loc : location;
- exp_type : logic_type; (** when used as placeholder for a term *)
- exp_name: string list;
-}
-
-(** {b Constants.} *)
-
-(** Literal constants *)
-and constant =
- | CInt64 of int64 * ikind * string option
- (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the
- * textual representation, if available. (This allows us to print a
- * constant as, for example, 0xF instead of 15.) Use {!Cil.integer} or
- * {!Cil.kinteger} to create these. Watch out for integers that cannot be
- * represented on 64 bits. OCAML does not give Overflow exceptions. *)
- | CStr of string
- (** String constant. The escape characters inside the string have been
- * already interpreted. This constant has pointer to character type! The
- * only case when you would like a string literal to have an array type
- * is when it is an argument to sizeof. In that case you should use
- * SizeOfStr. *)
- | CWStr of int64 list
- (** Wide character string constant. Note that the local interpretation
- * of such a literal depends on {!Cil.theMachine.wcharType} and {!Cil.theMachine.wcharKind}.
- * Such a constant has type pointer to {!Cil.theMachine.wcharType}. The
- * escape characters in the string have not been "interpreted" in
- * the sense that L"A\xabcd" remains "A\xabcd" rather than being
- * represented as the wide character list with two elements: 65 and
- * 43981. That "interpretation" depends on the underlying wide
- * character type. *)
- | CChr of char
- (** Character constant. This has type int, so use charConstToInt
- * to read the value in case sign-extension is needed. *)
- | CReal of float * fkind * string option
- (** Floating point constant. Give the fkind (see ISO 6.4.4.2) and also
- * the textual representation, if available. *)
- | CEnum of enumitem
- (** An enumeration constant
- * Use [Cillower.lowerEnumVisitor] to replace these with integer
- * constants. *)
-
-(** Unary operators *)
-and unop =
- Neg (** Unary minus *)
- | BNot (** Bitwise complement (~) *)
- | LNot (** Logical Not (!) *)
-
-(** Binary operations *)
-and binop =
- PlusA (** arithmetic + *)
- | PlusPI (** pointer + integer *)
- | IndexPI (** pointer + integer but only when
- * it arises from an expression
- * [e\[i\]] when [e] is a pointer and
- * not an array. This is semantically
- * the same as PlusPI but CCured uses
- * this as a hint that the integer is
- * probably positive. *)
- | MinusA (** arithmetic - *)
- | MinusPI (** pointer - integer *)
- | MinusPP (** pointer - pointer *)
- | Mult (** * *)
- | Div (** / *)
- | Mod (** % *)
- | Shiftlt (** shift left *)
- | Shiftrt (** shift right *)
-
- | Lt (** < (arithmetic comparison) *)
- | Gt (** > (arithmetic comparison) *)
- | Le (** <= (arithmetic comparison) *)
- | Ge (** >= (arithmetic comparison) *)
- | Eq (** == (arithmetic comparison) *)
- | Ne (** != (arithmetic comparison) *)
- | BAnd (** bitwise and *)
- | BXor (** exclusive-or *)
- | BOr (** inclusive-or *)
-
- | LAnd (** logical and. Unlike other
- * expressions this one does not
- * always evaluate both operands. If
- * you want to use these, you must
- * set {!Cil.useLogicalOperators}. *)
- | LOr (** logical or. Unlike other
- * expressions this one does not
- * always evaluate both operands. If
- * you want to use these, you must
- * set {!Cil.useLogicalOperators}. *)
-
-(** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator.
-In C the syntax for lvalues is not always a good indication of the meaning
-of the lvalue. For example the C value
-{v
-a[0][1][2]
- v}
- might involve 1, 2 or 3 memory reads when used in an expression context,
-depending on the declared type of the variable [a]. If [a] has type [int
-\[4\]\[4\]\[4\]] then we have one memory read from somewhere inside the area
-that stores the array [a]. On the other hand if [a] has type [int ***] then
-the expression really means [* ( * ( * (a + 0) + 1) + 2)], in which case it is
-clear that it involves three separate memory operations.
-
-An lvalue denotes the contents of a range of memory addresses. This range
-is denoted as a host object along with an offset within the object. The
-host object can be of two kinds: a local or global variable, or an object
-whose address is in a pointer expression. We distinguish the two cases so
-that we can tell quickly whether we are accessing some component of a
-variable directly or we are accessing a memory location through a pointer.
-To make it easy to
-tell what an lvalue means CIL represents lvalues as a host object and an
-offset (see {!Cil_types.lval}). The host object (represented as
-{!Cil_types.lhost}) can be a local or global variable or can be the object
-pointed-to by a pointer expression. The offset (represented as
-{!Cil_types.offset}) is a sequence of field or array index designators.
-
- Both the typing rules and the meaning of an lvalue is very precisely
-specified in CIL.
-
- The following are a few useful function for operating on lvalues:
-- {!Cil.mkMem} - makes an lvalue of [Mem] kind. Use this to ensure
-that certain equivalent forms of lvalues are canonized.
-For example, [*&x = x].
-- {!Cil.typeOfLval} - the type of an lvalue
-- {!Cil.typeOffset} - the type of an offset, given the type of the
-host.
-- {!Cil.addOffset} and {!Cil.addOffsetLval} - extend sequences
-of offsets.
-- {!Cil.removeOffset} and {!Cil.removeOffsetLval} - shrink sequences
-of offsets.
-
-The following equivalences hold {v
-Mem(AddrOf(Mem a, aoff)), off = Mem a, aoff + off
-Mem(AddrOf(Var v, aoff)), off = Var v, aoff + off
-AddrOf (Mem a, NoOffset) = a
- v} *)
-
-and lval =
- lhost * offset
-
-(** The host part of an {!Cil_types.lval}. *)
-and lhost =
- | Var of varinfo
- (** The host is a variable. *)
-
- | Mem of exp
- (** The host is an object of type [T] when the expression has pointer
- * [TPtr(T)]. *)
-
-
-(** The offset part of an {!Cil_types.lval}. Each offset can be applied to certain
- * kinds of lvalues and its effect is that it advances the starting address
- * of the lvalue and changes the denoted type, essentially focussing to some
- * smaller lvalue that is contained in the original one.
- @plugin development guide *)
-and offset =
- | NoOffset (** No offset. Can be applied to any lvalue and does
- * not change either the starting address or the type.
- * This is used when the lval consists of just a host
- * or as a terminator in a list of other kinds of
- * offsets. *)
-
- | Field of fieldinfo * offset
- (** A field offset. Can be applied only to an lvalue
- * that denotes a structure or a union that contains
- * the mentioned field. This advances the offset to the
- * beginning of the mentioned field and changes the
- * type to the type of the mentioned field. *)
-
- | Index of exp * offset
- (** An array index offset. Can be applied only to an
- * lvalue that denotes an array. This advances the
- * starting address of the lval to the beginning of the
- * mentioned array element and changes the denoted type
- * to be the type of the array element *)
-
-
-(** {b Initializers.}
-A special kind of expressions are those that can appear as initializers for
-global variables (initialization of local variables is turned into
-assignments). The initializers are represented as type {!Cil_types.init}. You
-can create initializers with {!Cil.makeZeroInit} and you can conveniently
-scan compound initializers them with {!Cil.foldLeftCompound}.
-*)
-(** Initializers for global variables. *)
-and init =
- | SingleInit of exp (** A single initializer *)
- | CompoundInit of typ * (offset * init) list
- (** Used only for initializers of structures, unions and arrays.
- * The offsets are all of the form [Field(f, NoOffset)] or
- * [Index(i, NoOffset)] and specify the field or the index being
- * initialized. For structures all fields
- * must have an initializer (except the unnamed bitfields), in
- * the proper order. This is necessary since the offsets are not
- * printed. For arrays the list must contain a prefix of the
- * initializers; the rest are 0-initialized.
- * For unions there must be exactly one initializer. If
- * the initializer is not for the first field then a field
- * designator is printed, so you better be on GCC since MSVC does
- * not understand this. You can scan an initializer list with
- * {!Cil.foldLeftCompound}. *)
-
-(** We want to be able to update an initializer in a global variable, so we
- * define it as a mutable field *)
-and initinfo = {
- mutable init : init option;
- }
-
-(** {b Function definitions.}
-A function definition is always introduced with a [GFun] constructor at the
-top level. All the information about the function is stored into a
-{!Cil_types.fundec}. Some of the information (e.g. its name, type,
-storage, attributes) is stored as a {!Cil_types.varinfo} that is a field of the
-[fundec]. To refer to the function from the expression language you must use
-the [varinfo].
-
- The function definition contains, in addition to the body, a list of all the
-local variables and separately a list of the formals. Both kind of variables
-can be referred to in the body of the function. The formals must also be shared
-with the formals that appear in the function type. For that reason, to
-manipulate formals you should use the provided functions
-{!Cil.makeFormalVar} and {!Cil.setFormals}.
-*)
-(** Function definitions.
- @plugin development guide *)
-and fundec =
- { mutable svar: varinfo;
- (** Holds the name and type as a variable, so we can refer to it
- * easily from the program. All references to this function either
- * in a function call or in a prototype must point to the same
- * [varinfo]. *)
- mutable sformals: varinfo list;
- (** Formals. These must be in the same order and with the same
- * information as the formal information in the type of the function.
- * Use {!Cil.setFormals} or
- * {!Cil.setFunctionType} to set these formals and ensure that they
- * are reflected in the function type. Do not make copies of these
- * because the body refers to them. *)
- mutable slocals: varinfo list;
- (** Locals. Does NOT include the sformals. Do not make copies of
- * these because the body refers to them. *)
- mutable smaxid: int; (** Max local id. Starts at 0. Used for
- * creating the names of new temporary
- * variables. Updated by
- * {!Cil.makeLocalVar} and
- * {!Cil.makeTempVar}. You can also use
- * {!Cil.setMaxId} to set it after you
- * have added the formals and locals. *)
- mutable sbody: block; (** The function body. *)
- mutable smaxstmtid: int option; (** max id of a (reachable) statement
- * in this function, if we have
- * computed it. range = 0 ...
- * (smaxstmtid-1). This is computed by
- * {!Cil.computeCFGInfo}. *)
- mutable sallstmts: stmt list; (** After you call {!Cil.computeCFGInfo}
- * this field is set to contain all
- * statements in the function *)
- mutable sspec: funspec;
- }
-
-
-(** A block is a sequence of statements with the control falling through from
- one element to the next *)
-and block =
- { mutable battrs: attributes; (** Attributes for the block *)
- mutable blocals: varinfo list; (** variables that are local to
- the block. It is a subset of the
- slocals of the enclosing function.
- *)
- mutable bstmts: stmt list; (** The statements comprising the block*)
- }
-
-(** {b Statements}.
-CIL statements are the structural elements that make the CFG. They are
-represented using the type {!Cil_types.stmt}. Every
-statement has a (possibly empty) list of labels. The
-{!Cil_types.stmtkind} field of a statement indicates what kind of statement it
-is.
-
- Use {!Cil.mkStmt} to make a statement and the fill-in the fields.
-
-CIL also comes with support for control-flow graphs. The [sid] field in
-[stmt] can be used to give unique numbers to statements, and the [succs]
-and [preds] fields can be used to maintain a list of successors and
-predecessors for every statement. The CFG information is not computed by
-default. Instead you must explicitly use the functions
-{!Cil.prepareCFG} and {!Cil.computeCFGInfo} to do it.
-
-*)
-(** Statements.
- @plugin development guide *)
-and stmt = {
- mutable labels: label list;
- (** Whether the statement starts with some labels, case statements or
- * default statements. *)
-
- mutable skind: stmtkind;
- (** The kind of statement *)
-
- mutable sid: int;
- (** A number (>= 0) that is unique in a function. Filled in only after
- * the CFG is computed. *)
- mutable succs: stmt list;
- (** The successor statements. They can always be computed from the skind
- * and the context in which this statement appears. Filled in only after
- * the CFG is computed. *)
- mutable preds: stmt list;
- (** The inverse of the succs function. *)
-
- mutable ghost : bool
- }
-
-(** Labels *)
-and label =
- Label of string * location * bool
- (** A real label. If the bool is "true", the label is from the
- * input source program. If the bool is "false", the label was
- * created by CIL or some other transformation *)
- | Case of exp * location (** A case statement. This expression
- * is lowered into a constant if
- * {!Cil.lowerConstants} is set to
- * true. *)
- | Default of location (** A default statement *)
-
-
-
-(* The various kinds of statements *)
-and stmtkind =
- | Instr of instr
- (** A group of instructions that do not contain control flow. Control
- * implicitly falls through. *)
-
- | Return of exp option * location
- (** The return statement. This is a leaf in the CFG. *)
-
- | Goto of stmt ref * location
- (** A goto statement. Appears from actual goto's in the code or from
- * goto's that have been inserted during elaboration. The reference
- * points to the statement that is the target of the Goto. This means that
- * you have to update the reference whenever you replace the target
- * statement. The target statement MUST have at least a label. *)
-
- | Break of location
- (** A break to the end of the nearest enclosing Loop or Switch *)
-
- | Continue of location
- (** A continue to the start of the nearest enclosing [Loop] *)
- | If of exp * block * block * location
- (** A conditional. Two successors, the "then" and the "else" branches.
- * Both branches fall-through to the successor of the If statement. *)
-
- | Switch of exp * block * (stmt list) * location
- (** A switch statement. The statements that implement the cases can be
- * reached through the provided list. For each such target you can find
- * among its labels what cases it implements. The statements that
- * implement the cases are somewhere within the provided [block]. *)
-
- | Loop of code_annotation list *
- block * location * (stmt option) * (stmt option)
- (** A [while(1)] loop. The termination test is implemented in the body of
- * a loop using a [Break] statement. If prepareCFG has been called,
- * the first stmt option will point to the stmt containing the continue
- * label for this loop and the second will point to the stmt containing
- * the break label for this loop. *)
-
- | Block of block
- (** Just a block of statements. Use it as a way to keep some block
- * attributes local *)
-
- | UnspecifiedSequence of (stmt * lval list * lval list * lval list) list
- (** statements whose order of execution is not specified by
- ISO/C. This is important for the order of side effects
- during evaluation of expressions. Each statement comes
- together with three list of lval
- - lvals that are written during the sequence and whose future
- value depends upon the statement (it is legal to read from them)
- - lvals that are written during the evaluation of the statement itself
- - lval that are read.
- Note that this include only a subset of the affectations
- of the statement. Namely, the
- temporary variables generated by cil are excluded (i.e. it
- is assumed that the "compilation" is correct). In addition,
- side effects caused by function applications are not taken
- into account in the list. For a single statement, the written lvals
- are supposed to be ordered (or their order of evaluation doesn't
- matter), so that an alarm should be emitted only if the lvals read by
- a statement overlap with the lvals written (or read) by another
- statement of the sequence.
-
- At this time this feature is
- experimental and may miss some unspecified sequences.
-
- In case you do not care about this feature just handle it
- like a block (see {!Cil.block_from_unspecified_sequence}) *)
- | TryFinally of block * block * location
- (** On MSVC we support structured exception handling. This is what you
- * might expect. Control can get into the finally block either from the
- * end of the body block, or if an exception is thrown. *)
-
- | TryExcept of block * (instr list * exp) * block * location
- (** On MSVC we support structured exception handling. The try/except
- * statement is a bit tricky:
-{v __try \{ blk \}
- __except (e) \{
- handler
- \}
-v}
-
- The argument to __except must be an expression. However, we keep a
- list of instructions AND an expression in case you need to make
- function calls. We'll print those as a comma expression. The control
- can get to the __except expression only if an exception is thrown.
- After that, depending on the value of the expression the control
- goes to the handler, propagates the exception, or retries the
- exception !!! The location corresponds to the try keyword.
- *)
-
-
-(** Instructions. They may cause effects directly but may not have control
- flow.*)
-and instr =
- Set of lval * exp * location (** An assignment. A cast is present
- if the exp has different type
- from lval *)
- | Call of lval option * exp * exp list * location
- (** optional: result is an lval. A cast might be
- necessary if the declared result type of the
- function is not the same as that of the
- destination. If the function is declared then
- casts are inserted for those arguments that
- correspond to declared formals. (The actual
- number of arguments might be smaller or larger
- than the declared number of arguments. C allows
- this.) If the type of the result variable is not
- the same as the declared type of the function
- result then an implicit cast exists. *)
-
- (* See the GCC specification for the meaning of ASM.
- * If the source is MS VC then only the templates
- * are used *)
- (* sm: I've added a notes.txt file which contains more
- * information on interpreting Asm instructions *)
- | Asm of attributes * (* Really only const and volatile can appear
- * here *)
- string list * (* templates (CR-separated) *)
- (string option * string * lval) list *
- (* outputs must be lvals with
- * optional names and constraints.
- * I would like these
- * to be actually variables, but I
- * run into some trouble with ASMs
- * in the Linux sources *)
- (string option * string * exp) list *
- (* inputs with optional names and constraints *)
- string list * (* register clobbers *)
- location
- (** An inline assembly instruction. The arguments are (1) a list of
- attributes (only const and volatile can appear here and only for
- GCC), (2) templates (CR-separated), (3) a list of
- outputs, each of which is an lvalue with a constraint, (4) a list
- of input expressions along with constraints, (5) clobbered
- registers, and (5) location information *)
-
- | Skip of location
-
- | Code_annot of code_annotation * location
-
-(** Describes a location in a source file *)
-and location = Lexing.position * Lexing.position
-
-(** Type signatures. Two types are identical iff they have identical
- signatures *)
-and typsig =
- TSArray of typsig * int64 option * attribute list
- | TSPtr of typsig * attribute list
- | TSComp of bool * string * attribute list
- | TSFun of typsig * typsig list * bool * attribute list
- | TSEnum of string * attribute list
- | TSBase of typ
-
-(** Abstract syntax trees for annotations *)
-
-(** Types of logic terms. *)
-and logic_type =
- | Ctype of typ (** a C type *)
- | Ltype of logic_type_info * logic_type list
- (** an user-defined logic type with its parameters *)
- | Lvar of string (** a type variable. *)
- | Linteger (** mathematical integers, {i i.e.} Z *)
- | Lreal (** mathematical reals, {i i.e.} R *)
- | Larrow of logic_type list * logic_type (** (n-ary) function type *)
-
-(** tsets with an unique identifier.
- Use [Logic_const.new_location] to generate a new id. *)
-and identified_term =
- { it_id: int; (** the identifier. *)
- it_content: term (** the term *)
- }
-
-(** logic label referring to a particular program point. *)
-and logic_label =
- | StmtLabel of stmt ref (** label of a C statement. *)
- | LogicLabel of string (** builtin logic label ({t Here, Pre}, ...) *)
-
-(* Expressions follow CIL constructs (with prefix T) *)
-
-(** Logic terms. *)
-and term = {
- term_node : term_node; (** kind of term. *)
- term_loc : Lexing.position * Lexing.position;
- (** position in the source file. *)
- term_type : logic_type; (** type of the term. *)
- term_name: string list; (** names of the term if any. *)
-}
-
-(** the various kind of terms. *)
-and term_node =
- (* same constructs as exp *)
- | TConst of constant (** a constant. *)
- | TLval of term_lval (** an L-value *)
- | TSizeOf of typ (** size of a given C type. *)
- | TSizeOfE of term (** size of the type of an expression. *)
- | TSizeOfStr of string (** size of a string constant. *)
- | TAlignOf of typ (** alignment of a type. *)
- | TAlignOfE of term (** alignment of the type of an expression. *)
- | TUnOp of unop * term (** unary operator. *)
- | TBinOp of binop * term * term (** binary operators. *)
- | TCastE of typ * term (** cast to a C type. *)
- | TAddrOf of term_lval (** address of a term. *)
- | TStartOf of term_lval (** beginning of an array. *)
- (* additional constructs *)
- | Tapp of logic_info * (logic_label * logic_label) list * term list
- (** application of a logic function. *)
- | Tlambda of quantifiers * term (** lambda abstraction. *)
- | TDataCons of logic_ctor_info * term list
- (** constructor of logic sum-type. *)
- | Tif of term * term * term
- (** conditional operator*)
- | Told of term (** term refers to the pre-state of the function. *)
- | Tat of term * logic_label
- (** term refers to a particular program point. *)
- | Tbase_addr of term (** base address of a pointer. *)
- | Tblock_length of term (** length of the block pointed to by the term. *)
- | Tnull (** the null pointer. *)
- | TCoerce of term * typ (** coercion to a given C type. *)
- | TCoerceE of term * term (** coercion to the type of a given term. *)
- | TUpdate of term * fieldinfo * term
- (** functional update of a field. *)
- | Ttypeof of term (** type tag for a term. *)
- | Ttype of typ (** type tag for a C type. *)
- | Tempty_set (** the empty set. *)
- | Tunion of term list (** union of terms. *)
- | Tinter of term list (** intersection of terms. *)
- | Tcomprehension of
- term * quantifiers * predicate named option
- (** set defined in comprehension ({t \{ t[i] | integer i; 0 <= i < 5\}})
- *)
- | Trange of term option * term option (** range of integers. *)
- | Tlet of logic_info * term (** local binding *)
-
-(** lvalue: base address and offset. *)
-and term_lval =
- term_lhost * term_offset
-
-(** base address of an lvalue. *)
-and term_lhost =
- | TVar of logic_var (** a variable. *)
- | TResult of typ (** value returned by a C function.
- Only used in post-conditions or assigns
- *)
- | TMem of term (** memory access. *)
-
-(** offset of an lvalue. *)
-and term_offset =
- | TNoOffset (** no further offset. *)
- | TField of fieldinfo * term_offset
- (** access to the field of a compound type. *)
- | TIndex of term * term_offset
- (** index. Note that a range is denoted by [TIndex(t,Trange(i1,i2))] *)
-
-(** description of a logic function or predicate.
-@plugin development guide *)
-and logic_info = {
-(*
- mutable l_name : string; (** name of the function. *)
-*)
- mutable l_var_info : logic_var;
- (** we use only fields lv_name and lv_id of l_var_info
- we should factorize lv_type and l_type+l_profile below *)
- mutable l_labels : logic_label list; (** label arguments of the function. *)
- mutable l_tparams : string list; (** type parameters *)
- mutable l_type : logic_type option; (** return type. None for predicates *)
- mutable l_profile : logic_var list; (** type of the arguments. *)
- mutable l_body : logic_body; (** body of the function. *)
-}
-
-and builtin_logic_info =
- { mutable bl_name: string;
- mutable bl_labels: logic_label list;
- mutable bl_params: string list;
- mutable bl_type: logic_type option;
- mutable bl_profile: (string * logic_type) list;
- }
-
-and logic_body =
- | LBnone
- (** no definition and no reads clause *)
- | LBreads of identified_term list
- (** read accesses performed by a function. *)
- | LBterm of term (** direct definition of a function. *)
- | LBpred of predicate named (** direct definition of a predicate. *)
- | LBinductive of
- (string * logic_label list * string list * predicate named) list
- (** inductive definition *)
-
-(** description of a logic type*)
-and logic_type_info =
- { lt_name: string;
- lt_params : string list; (** type parameters*)
- mutable lt_def: logic_type_def option
- (** definition of the type. None for abstract types. *)
- }
- (* will be expanded when dealing with concrete types *)
-
-and logic_type_def =
- | LTsum of logic_ctor_info list (** sum type with its constructors. *)
- | LTsyn of logic_type (** Synonym of another type. *)
-
-(** description of a logic variable
-@plugin development guide *)
-and logic_var = {
- mutable lv_name : string; (** name of the variable. *)
- mutable lv_id : int; (** unique identifier *)
- mutable lv_type : logic_type; (** type of the variable. *)
- mutable lv_origin : varinfo option (** when the logic variable stems from a
- C variable, set to the original C variable.
- *)
-}
-
-(** description of a constructor of a logic sum-type*)
-and logic_ctor_info =
- { ctor_name: string; (** name of the constructor. *)
- ctor_type: logic_type_info; (** type to which the constructor belongs. *)
- ctor_params: logic_type list
- (** types of the parameters of the constructor. *)
- }
-
-(* Predicates *)
-
-(** variables bound by a quantifier. *)
-and quantifiers = logic_var list
-
-(** comparison relations*)
-and relation = Rlt | Rgt | Rle | Rge | Req | Rneq
-
-(** predicates *)
-and predicate =
- | Pfalse (** always-false predicate. *)
- | Ptrue (** always-true predicate. *)
- | Papp of logic_info * (logic_label * logic_label) list * term list
- (** application of a predicate. *)
- | Pseparated of term list
- | Prel of relation * term * term
- (** comparison of two terms. *)
- | Pand of predicate named * predicate named
- (** conjunction *)
- | Por of predicate named * predicate named
- (** disjunction. *)
- | Pxor of predicate named * predicate named
- (** logical xor. *)
- | Pimplies of predicate named * predicate named
- (** implication. *)
- | Piff of predicate named * predicate named
- (** equivalence. *)
- | Pnot of predicate named
- (** negation. *)
- | Pif of term * predicate named * predicate named
- (** conditional *)
- | Plet of logic_info * predicate named
- (** definition of a local variable *)
- | Pforall of quantifiers * predicate named
- (** universal quantification. *)
- | Pexists of quantifiers * predicate named
- (** existential quantification. *)
- | Pold of predicate named
- (** predicate refers to the pre-state of a function. *)
- | Pat of predicate named * logic_label
- (** predicate refers to a particular program point. *)
- | Pvalid of term
- (** the given locations are valid. *)
- | Pvalid_index of term * term
- (** {b deprecated:} Use [Pvalid(TLval(TBinOp(PlusPI,p,i)))] instead
-
- [Pvalid_index(p,i)] indicates that accessing the [i]th element
- of [p] is valid.
- *)
- | Pvalid_range of term * term * term
- (** {b deprecated:} Use [Pvalid(TLVal(TBinOp(PlusPI(p,Trange(i1,i2)))))]
- instead
-
- similar to [Pvalid_index] but for a range of indices.*)
- | Pfresh of term
- (** The given term is newly allocated in the post-state of a function.*)
- | Psubtype of term * term
- (** First term is a type tag that is a subtype of the second. *)
-
-(** predicate with an unique identifier.
-Use [Logic_const.new_predicate] to create fresh predicates *)
-and identified_predicate = {
- ip_name: string list; (** names given to the predicate if any.*)
- ip_loc: location; (** location in the source code. *)
- ip_id: int; (** identifier *)
- ip_content: predicate; (** the predicate itself*)
-}
-
-(* Polymorphic types shared with parsed trees (Logic_ptree) *)
-(** variant of a loop or a recursive function. Type shared with Logic_ptree. *)
-and 'term variant = 'term * string option
-
-(** zone assigned by a C function. Type shared with Logic_ptree. *)
-and 'locs zone =
- Location of 'locs (** tsets *)
- | Nothing (** nothing is assigned. *)
-
-(** zone assigned with its dependencies. Type shared with Logic_ptree.*)
-and 'locs assigns = 'locs zone * ('locs zone list)
-
-(** object that can be named (in particular predicates). *)
-and 'a named = { name : string list; (** list of given names *)
- loc : location; (** position in the source code. *)
- content : 'a; (** content *)
- }
-
-(** function contract. Type shared with Logic_ptree. *)
-and ('term,'pred,'locs) spec = {
- mutable spec_requires : 'pred list; (** global requirements. *)
- mutable spec_behavior : ('pred,'locs) behavior list;
- (** behaviors *)
- mutable spec_variant : 'term variant option;
- (** variant for recursive functions. *)
- mutable spec_terminates: 'pred option;
- (** termination condition. *)
- mutable spec_complete_behaviors: string list list;
- (** list of complete behaviors.
- It is possible to have more than one set of complete behaviors *)
- mutable spec_disjoint_behaviors: string list list;
- (** list of disjoint behaviors.
- It is possible to have more than one set of disjoint behaviors *)
-}
-
-(** behavior of a function. Type shared with Logic_ptree.
- @modify Boron-20100401 [b_ensures] is replaced by [b_post_cond].
- Old [b_ensures] represent the [Normal] case of [b_post_cond].
- *)
-and ('pred,'locs) behavior = {
- mutable b_name : string; (** name of the behavior. *)
- mutable b_assumes : 'pred list; (** assume clauses. *)
- mutable b_post_cond : (termination_kind * 'pred) list; (** post-condition. *)
- mutable b_assigns : 'locs assigns list; (** assignments. *)
-}
-
-(** pragmas for the value analysis plugin of Frama-C.
-Type shared with Logic_ptree.*)
-and 'term loop_pragma =
- | Unroll_level of 'term
- | Widen_hints of 'term list
- | Widen_variables of 'term list
-
-(** pragmas for the slicing plugin of Frama-C. Type shared with Logic_ptree.*)
-and 'term slice_pragma =
- | SPexpr of 'term
- | SPctrl
- | SPstmt
-
-(** pragmas for the impact plugin of Frama-C. Type shared with Logic_ptree.*)
-and 'term impact_pragma =
- | IPexpr of 'term
- | IPstmt
-
-(** the various kinds of pragmas. Type shared with Logic_ptree. *)
-and 'term pragma =
- | Loop_pragma of 'term loop_pragma
- | Slice_pragma of 'term slice_pragma
- | Impact_pragma of 'term impact_pragma
-
-(** Annotation status *)
-and validity = True | False | Maybe
-and annot_checked_status = { mutable emitter : string;
- mutable valid : validity }
-and annotation_status = | Unknown (* Nothing was ever tried to check it *)
- | Checked of annot_checked_status (* Something was tried *)
-and annot_status = { mutable status : annotation_status }
-(** all annotations that can be found in the code.
- Type shared with Logic_ptree. *)
-and ('term, 'pred, 'spec_pred, 'locs) code_annot =
- | AAssert of string list * 'pred * annot_status
- (** assertion to be checked. The list of strings is the list of
- behaviors to which this assertion applies.
- @deprecated since Beryllium-20090902, the annot_status
- field is no longer updated by anyone. Use {!Db.Annotations.Status}
- functions to access the true status. *)
-
- | AStmtSpec of ('term, 'spec_pred, 'locs) spec (** statement contract. *)
- | AInvariant of string list * bool * 'pred
- (** code invariant. The list of strings is the list of
- behaviors to which this invariant applies.
- The boolean flag is true for normal loop invariants
- and false for invariant-as-assertions.
- TODO: remove this constructor:
- - normal loop invariants are now under constructor ALoopBehavior
- - invariant-as-assertions should be just one variant of AAssert
- *)
- | AVariant of 'term variant (** loop variant. Note that
- there can be at most one variant
- associated to a given statement
- *)
- | AAssigns of string list * 'locs assigns
- | APragma of 'term pragma (** pragma. *)
-
-(** function contract. *)
-and funspec = (term, identified_predicate, identified_term) spec
-
-(** code annotation with an unique identifier.
- Use [Logic_const.new_code_annotation] to create new code annotations with
- a fresh id. *)
-and code_annotation =
- { annot_content :
- (term, predicate named, identified_predicate, identified_term)
- code_annot; (** content of the annotation. *)
- annot_id: int (** identifier. *) }
-
-(** behavior of a function. *)
-and funbehavior = (identified_predicate,identified_term) behavior
-
-(** global annotations, not attached to a statement or a function. *)
-and global_annotation =
- | Dfun_or_pred of logic_info
- | Daxiomatic of string * global_annotation list
- | Dtype of logic_type_info (** declaration of a logic type. *)
- | Dlemma of string * bool * logic_label list * string list * predicate named
- (** definition of a lemma. The boolean flag is true if the property.
- should be taken as an axiom and false if it must be proved.
- *)
- | Dinvariant of logic_info
- (** global invariant. The predicate does not have any argument. *)
- | Dtype_annot of logic_info
- (** type invariant. The predicate has exactly one argument. *)
-
-type kinstr =
- | Kstmt of stmt
- | Kglobal
-
-type mach = {
- version_major: int; (* Major version number *)
- version_minor: int; (* Minor version number *)
- version: string; (* version number *)
- underscore_name: bool; (* If assembly names have leading underscore *)
- sizeof_short: int; (* Size of "short" *)
- sizeof_int: int; (* Size of "int" *)
- sizeof_long: int ; (* Size of "long" *)
- sizeof_longlong: int; (* Size of "long long" *)
- sizeof_ptr: int; (* Size of pointers *)
- sizeof_enum: int; (* Size of enum types *)
- sizeof_float: int; (* Size of "float" *)
- sizeof_double: int; (* Size of "double" *)
- sizeof_longdouble: int; (* Size of "long double" *)
- sizeof_void: int; (* Size of "void" *)
- sizeof_fun: int; (* Size of function *)
- size_t: string; (* Type of "sizeof(T)" *)
- wchar_t: string; (* Type of "wchar_t" *)
- ptrdiff_t: string; (* Type of "ptrdiff_t" *)
- enum_are_signed: bool; (* Sign of enum types *)
- alignof_short: int; (* Alignment of "short" *)
- alignof_int: int; (* Alignment of "int" *)
- alignof_long: int; (* Alignment of "long" *)
- alignof_longlong: int; (* Alignment of "long long" *)
- alignof_ptr: int; (* Alignment of pointers *)
- alignof_enum: int; (* Alignment of enum types *)
- alignof_float: int; (* Alignment of "float" *)
- alignof_double: int; (* Alignment of "double" *)
- alignof_longdouble: int; (* Alignment of "long double" *)
- alignof_str: int; (* Alignment of strings *)
- alignof_fun: int; (* Alignment of function *)
- alignof_char_array: int; (* Alignment of arrays of char *)
- char_is_unsigned: bool; (* Whether "char" is unsigned *)
- const_string_literals: bool; (* Whether string literals have const chars *)
- little_endian: bool; (* whether the machine is little endian *)
-}
-
-(*
-Local Variables:
-compile-command: "LC_ALL=C make -C ../.."
-End:
-*)