cil 0.0.0 → 0.0.1
raw patch · 7 files changed
+2149/−85 lines, 7 files
Files
- GenCIL.hs +400/−0
- Language/CIL.hs +194/−12
- Makefile +24/−0
- cil.cabal +4/−3
- cil_types.mli +1527/−0
- dumpcil/Makefile +0/−11
- dumpcil/dump_cil.ml +0/−59
+ GenCIL.hs view
@@ -0,0 +1,400 @@+-- | 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,20 +1,202 @@-{- Generated by DrIFT (Automatic class derivations for Haskell) -}-{-# LINE 1 "Language/CIL.DrIFT.hs" #-}+-- | 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- ( File (..)+ ( 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 (..)+ ) where -import Text.Parse+import System.Exit+import System.Process -data File = File String- deriving Show {-!derive : 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 -{-* Generated by DrIFT : Look, but Don't Touch. *-}-instance Parse File where- parse = constructors- [ ( "File" , fmap File parse )- ]+ -- | 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 () --- Imported from other files :-+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 !-}++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 !-}+
+ Makefile view
@@ -0,0 +1,24 @@+.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,5 +1,5 @@ name: cil-version: 0.0.0+version: 0.0.1 category: Language @@ -20,8 +20,9 @@ cabal-version: >= 1.6 extra-source-files:- dumpcil/dump_cil.ml- dumpcil/Makefile+ Makefile+ cil_types.mli+ GenCIL.hs library build-depends:
+ cil_types.mli view
@@ -0,0 +1,1527 @@+(**************************************************************************)+(* *)+(* 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:+*)
− dumpcil/Makefile
@@ -1,11 +0,0 @@-FRAMAC_SHARE :=$(shell frama-c.byte -print-path)-FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)-PLUGIN_NAME = DumpCIL-PLUGIN_CMO = dump_cil--include $(FRAMAC_SHARE)/Makefile.dynamic--.PHONY:clean-all-clean-all: clean- -rm -f .depend- -rm -f $(FRAMAC_LIBDIR)/DumpCIL.*
− dumpcil/dump_cil.ml
@@ -1,59 +0,0 @@-open Ast-open Cil_types-open File-open Lexing-open List--let error loc msg = prerr_endline ("ERROR: " ^ msg); exit 1--let unknown =- { pos_fname = "unknown"- ; pos_lnum = 0- ; pos_bol = 0- ; pos_cnum = 0- }--let format_fundec _ _ = "function declaration"--let format_global a = match a with- GType (a, loc) -> "typedef"- | GCompTag (a, loc) -> "struct-union definition"- | GCompTagDecl (a, loc) -> "struct-union declaration"- | GEnumTag (a, loc) -> "enum definition"- | GEnumTagDecl (a, loc) -> "enum declaration"- | GVarDecl (f, v, loc) -> "variable declaration"- | GVar (v, i, loc) -> "variable definition"- | GFun (a, loc) -> format_fundec a loc- | GAsm (_, loc) -> error loc "asm not supported"- | GPragma (a, loc) -> ""- | GText _ -> "text"- | GAnnot _ -> "annot"--let dump file =- (match file.globinit with- None -> ()- | Some f -> error unknown "initializer not supported");- iter (fun a -> if String.length a == 0 then () else print_endline a) (map format_global file.globals)--let run () =- File.init_from_cmdline ();- dump (Ast.get ())--module Self =- Plugin.Register- (struct- let name = "DumpCIL"- let shortname = "DumpCIL"- let descr = "Dumps CIL and ACSL to stdout."- end);;--module Enabled =- Self.False- (struct- let option_name = "-dumpcil"- let descr = "Dumps CIL and ACSL to stdout."- end);;--let () = Db.Main.extend (fun () -> if Enabled.get () then run ())--