# Path: modules/run_ast/ast.py
# CPPPATH = 'utils/cpp.exe' if sys.platform == 'win32' else 'cpp'
# ABS_PATH = os.path.dirname(__file__)
# class IdentifyVarDecl(NodeVisitor):
# class RunAstDecl(object):
#     def __init__(self):
#     def getnumberofline(nodecoord):
#     def visit_Decl(self, node):
#     def __init__(self, _cfilepath):
#     def identify_decl(self):
# 
# Path: modules/invariant_tools/pips/translate_pips/translate_pips.py
# class PipsTranslateAnnot(object):
#     def __init__(self):
#     def instprecondinprog(self, _cprogrampath):
#     def hasprecondmorelines(_listcfile, _actualindex):
#     def translatepreconditionpips(self, _precondtext):
# 
# Path: modules/invariant_tools/pagai/translate_inv_pagai/translate_pagai.py
# class TranslatePagai(object):
#     def __init__(self):
#     def removenotprintable(self, __listprogram):
#     def identifyInv(self, __pathprogram):
#     def applyesbmcassume(self, __inv):
#     def writeInvPAGAI(self, __pathprogram, addassume):
# 
# Path: modules/invariant_tools/pagai/generate_inv_pagai/generate_inv_pagai.py
# class GeneratePagaiInv(object):
#     def __init__(self):
#     def generate_inv(self, __pathprogram):
# 
# Path: modules/bmc_check/esbmccheck.py
# class DepthEsbmcCheck(object):
#     def __init__(self):
#     def getlastlinenumfromce(_esbmccepath, _indexliststartsearch):
#     def translatecedata(self, _listlinesfromce):
#     def handletextfrom_ce(self, _stringtxtce, _enablescopecheck):
#     def getfunctnamebylinenum(self, _linenum):
#     def checkscopeextraassume(self, _linenumber):
#     def lastsearchbylinetoassume(_esbmccepath, _indexliststartsearch):
#     def getlastdatafromce(self, _esbmccepath):
#     def addassumeinprogram(self, _cprogrampath):
#     def savelist2file(_pathfile, _list2file):
#     def isdefiniedmemlimit(self):
#     def hasincorrectopesbmc(_esbmcoutput):
#     def hastimeoutfromesbmc(_esbmcoutput):
#     def hassuccessfulfromesbmc(_esbmcoutput):
#     def checkwithkparallel(self, _cprogrampath, _actual_ce, _listtmpfiles):
#     def cleantmpfiles(_listfiles2delete):
#     def kinductioncheck(self, _cprogrampath):
#     def getnumbeginfuncts(_cfilepath):
#     def configureUAPath(self):
#     def execUA(self, _cprogrampath, ua_ops):
#     def execBaseCase(self, _cprogrampath, actual_ce, lastResult):
#     def execForwardCondition(self, _cprogrampath, actual_ce, lastResult, listtmpfiles):
#     def execInductiveStep(self, _cprogrampath, actual_ce, lastResult, listtmpfiles, actual_detphver):
#     def check_witnessresult(self, _listresultwitness):
#     def check_witnessresultUA(self, _listresultwitness):
# 
# Path: modules/gnu_extension/hack_extensions.py
# def countwhiledelimiter(_list, _index):
# def make_pycparser_compatible(data):


import argparse
import shutil
import sys
import os
import commands
import re
import time
import random
import string
import platform
import time
from pipes import quote
from modules.run_ast import ast
from modules.invariant_tools.pips.translate_pips import translate_pips
from modules.invariant_tools.pagai.translate_inv_pagai import translate_pagai
from modules.invariant_tools.pagai.generate_inv_pagai import generate_inv_pagai
from modules.bmc_check import esbmccheck
from modules.gnu_extension import hack_extensions
from __future__ import print_function


# From project

class DepthK(object):
    def __init__(self, _cfilepath):
        self.cfilepath = _cfilepath
        self.inputisexti = False
        self.listnumbeginfunc = []
        self.nameoforicprogram = os.path.basename(_cfilepath)
        self.actual_cprogramname = ""
        self.depthkname_ext = "_new_depthk_" + str(time.strftime('%H:%M:%S').replace(":", "_")) + ".c"
        self.debug_op = False
        self.uncrustify_cfg = os.path.dirname(os.path.abspath(__file__)) + \
                              "/modules/preprocessing/uncrustify_files/ben.cfg"
        self.onlygeninvs_p = False
        self.en_kparalell = False
        self.esbmcpath = ''
        self.esbmcsolver = ""
        self.esbmc_memlimit = ""
        self.esbmc_timeout = ""
        self.esbmc_extraop = ""
        self.esbmc_arch = ""
        self.maxk = 10
        self.maxdepthcheck = 25
        #self.disableuse_ce = False
        self.use_counter_example = False
        self.pipsscriptpath = os.path.abspath(".") + \
                              '/modules/invariant_tools/pips/script_template/' + \

# Path: modules/run_ast/ast.py
# CPPPATH = 'utils/cpp.exe' if sys.platform == 'win32' else 'cpp'
# ABS_PATH = os.path.dirname(__file__)
# class IdentifyVarDecl(NodeVisitor):
# class RunAstDecl(object):
#     def __init__(self):
#     def getnumberofline(nodecoord):
#     def visit_Decl(self, node):
#     def __init__(self, _cfilepath):
#     def identify_decl(self):
# 
# Path: modules/invariant_tools/pips/translate_pips/translate_pips.py
# class PipsTranslateAnnot(object):
#     def __init__(self):
#     def instprecondinprog(self, _cprogrampath):
#     def hasprecondmorelines(_listcfile, _actualindex):
#     def translatepreconditionpips(self, _precondtext):
# 
# Path: modules/invariant_tools/pagai/translate_inv_pagai/translate_pagai.py
# class TranslatePagai(object):
#     def __init__(self):
#     def removenotprintable(self, __listprogram):
#     def identifyInv(self, __pathprogram):
#     def applyesbmcassume(self, __inv):
#     def writeInvPAGAI(self, __pathprogram, addassume):
# 
# Path: modules/invariant_tools/pagai/generate_inv_pagai/generate_inv_pagai.py
# class GeneratePagaiInv(object):
#     def __init__(self):
#     def generate_inv(self, __pathprogram):
# 
# Path: modules/bmc_check/esbmccheck.py
# class DepthEsbmcCheck(object):
#     def __init__(self):
#     def getlastlinenumfromce(_esbmccepath, _indexliststartsearch):
#     def translatecedata(self, _listlinesfromce):
#     def handletextfrom_ce(self, _stringtxtce, _enablescopecheck):
#     def getfunctnamebylinenum(self, _linenum):
#     def checkscopeextraassume(self, _linenumber):
#     def lastsearchbylinetoassume(_esbmccepath, _indexliststartsearch):
#     def getlastdatafromce(self, _esbmccepath):
#     def addassumeinprogram(self, _cprogrampath):
#     def savelist2file(_pathfile, _list2file):
#     def isdefiniedmemlimit(self):
#     def hasincorrectopesbmc(_esbmcoutput):
#     def hastimeoutfromesbmc(_esbmcoutput):
#     def hassuccessfulfromesbmc(_esbmcoutput):
#     def checkwithkparallel(self, _cprogrampath, _actual_ce, _listtmpfiles):
#     def cleantmpfiles(_listfiles2delete):
#     def kinductioncheck(self, _cprogrampath):
#     def getnumbeginfuncts(_cfilepath):
#     def configureUAPath(self):
#     def execUA(self, _cprogrampath, ua_ops):
#     def execBaseCase(self, _cprogrampath, actual_ce, lastResult):
#     def execForwardCondition(self, _cprogrampath, actual_ce, lastResult, listtmpfiles):
#     def execInductiveStep(self, _cprogrampath, actual_ce, lastResult, listtmpfiles, actual_detphver):
#     def check_witnessresult(self, _listresultwitness):
#     def check_witnessresultUA(self, _listresultwitness):
# 
# Path: modules/gnu_extension/hack_extensions.py
# def countwhiledelimiter(_list, _index):
# def make_pycparser_compatible(data):


# Path: depthk.py
import argparse
import shutil
import sys
import os
import commands
import re
import time
import random
import string
import platform
import time
from pipes import quote
from modules.run_ast import ast
from modules.invariant_tools.pips.translate_pips import translate_pips
from modules.invariant_tools.pagai.translate_inv_pagai import translate_pagai
from modules.invariant_tools.pagai.generate_inv_pagai import generate_inv_pagai
from modules.bmc_check import esbmccheck
from modules.gnu_extension import hack_extensions

from __future__ import print_function


# From project

class DepthK(object):
    def __init__(self, _cfilepath):
        self.cfilepath = _cfilepath
        self.inputisexti = False
        self.listnumbeginfunc = []
        self.nameoforicprogram = os.path.basename(_cfilepath)
        self.actual_cprogramname = ""
        self.depthkname_ext = "_new_depthk_" + str(time.strftime('%H:%M:%S').replace(":", "_")) + ".c"
        self.debug_op = False
        self.uncrustify_cfg = os.path.dirname(os.path.abspath(__file__)) + \
                              "/modules/preprocessing/uncrustify_files/ben.cfg"
        self.onlygeninvs_p = False
        self.en_kparalell = False
        self.esbmcpath = ''
        self.esbmcsolver = ""
        self.esbmc_memlimit = ""
        self.esbmc_timeout = ""
        self.esbmc_extraop = ""
        self.esbmc_arch = ""
        self.maxk = 10
        self.maxdepthcheck = 25
        #self.disableuse_ce = False
        self.use_counter_example = False
        self.pipsscriptpath = os.path.abspath(".") + \
                              '/modules/invariant_tools/pips/script_template/' + \

                              'script_generate_precod.pips'