cil 0.0.2 → 0.1.0
raw patch · 5 files changed
+408/−2157 lines, 5 filesdep +bytestringdep +language-cdep −polyparsedep −process
Dependencies added: bytestring, language-c
Dependencies removed: polyparse, process
Files
- GenCIL.hs +0/−400
- Language/CIL.hs +400/−192
- Makefile +0/−24
- cil.cabal +8/−14
- cil_types.mli +0/−1527
− GenCIL.hs
@@ -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]-
Language/CIL.hs view
@@ -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 }+--+-- <http://cil.sourceforge.net/> 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
− Makefile
@@ -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-
cil.cabal view
@@ -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 <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>@@ -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
− cil_types.mli
@@ -1,1527 +0,0 @@-(**************************************************************************)-(* *)-(* Copyright (C) 2001-2003 *)-(* George C. Necula <necula@cs.berkeley.edu> *)-(* Scott McPeak <smcpeak@cs.berkeley.edu> *)-(* Wes Weimer <weimer@cs.berkeley.edu> *)-(* Ben Liblit <liblit@cs.berkeley.edu> *)-(* 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(<type>). 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(<expression>) *)-- | 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:-*)