-- | 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                      (..)
  , 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 System.Exit
import System.Process

-- | 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

 -- | 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 ()

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 !-}