A | |
| aPostAsm [GenericAbstract] |
Generic forward non-relational abstract interpretation of ASM statements
stat The statement which is currently read, shouldGoBackOnJmp Is the statement read in a branch which has not been read before, f A reference to the set of the C functions, callStack The call stack, stack The memory stack, env The environment, context The context
|
| aPostAsmBlock [GenericAbstract] |
Generic forward non-relational abstract interpretation of ASM blocks
pre_loc The entry location of block, block The block of ASM statement to read, shouldGoBackOnJmp Is the statement read in a branch which has not been read before, f A reference to the set of C functions, callStack The call stack, stack The memory stack, env The environment, context The context
|
| aPostC [GenericAbstract] |
Generic forward non-relational abstract interpretation of C statements
stat The C statement, shouldGoBackOnJmp Is the statement read in a branch which has not been read before, f A reference to the C functions, callStack The call stack, lastAsmStack The stack state of the last ASM statement, env The environment, context The context
|
| aPostCBlock [GenericAbstract] |
Generic forward non-relational abstract interpretation of C blocks
program The block of C statements, shouldGoBackOnJmp Is the statement read in a branch which has not been read before, f A reference to the C functions, callStack The call stack, lastAsmStack The stack state of the last ASM statement, env The environment, context The context
|
| aPostGlobalC [GenericAbstract] |
Generic forward non-relational abstract interpretation of global statement
pre_loc The location before the global statement, stat The global statement, post_loc The location after the global statement, f A reference to the set of C functions, env The environement, context The context
|
| aPostProgram [GenericAbstract] |
Generic foward non-relational abstract interpretation of a block of global statements
pre_loc The location before the first global statement of the block, program The block of global statements, f A reference to the set of C functions, env The environment, context The context
|
| abexp [GenericAbstract] |
Generic abstract interpretation of boolean expression
b The boolean expression, context The context, env The environment, perhaps it will be modified
|
| abexpArithBin [SpecificAbstract] |
Specific abstract interpretation of binary boolean operators with arithmetics operands
a1 The abstract domain of the first operand, op The arithmetic to boolean binary operator, a2 The abstract domain of the second operand
|
| abexpBoolBin [GenericAbstract] |
Generic abstract interpretation of binary boolean operators
env1 The possible environment in which the first operand is satisfied, context1IsBot Is the context associated to env1 bottom, op The binary boolean operator, env2 The possible environment in which the second operand is satisfied, context2IsBot Is the context associated to env2 bottom
|
| abstrD2string [Debug] |
Deserialize an abstract domain
value The abstract domain
|
| abstrMax [Types] |
Maximum number
|
| abstrMin [Types] |
Minimum number
|
| abstrTop [Types] |
Top element of the abstract domains
|
| addLocationsProgram [Utils] |
Adds locations to an unlocated program
program The unlocated program
|
| addVarToContext [GenericAbstract] |
Adds an undefined variable to a context and returns the new context
vn The name of the variable, value The value of the variable that we want to set, env The environment, context The context
|
| alpha [SpecificAbstract] |
Abstraction of a real element
real_elem The real element
|
| analyseProgram [Analysis] |
Analyse a program and write results of this analysis or exceptions encountered
l The initial location of program, program The program already located to analyse
|
| areEnvironmentEqual [GenericAbstract] |
Test equality of two environments
e1 The first environment, e2 The second environment
|
| args2string [Debug] |
Deserialize arguments of a C function (which is a list of arithmetic expressions)
args The arguments
|
| args_def2string [Debug] |
Deserialize definition of arguments of a C function
args The definition of the arguments
|
| arith_expr2string [Debug] |
Deserialize arithmetic expressions
a The arithmetic expression
|
| arith_expr_needs_parenthesis [Debug] |
Remove sometimes some parenthesis
a An arithmetic expression
|
| asm_expr2string [Debug] |
Deserialize ASM expression
ae The ASM expression
|
B | |
| baexp [GenericAbstract] |
Backward abstract semantics of arithmetic expressions
a An arithmetic expression, context The context in which the arithmetic expression is performed, p The domain in which the evaluation of the arithmetic expression has to be, env The environment in which the arithmetic expression is performed, perhaps it will be modified
|
| baexpBin [SpecificAbstract] |
Backward abstract semantics of arithmetic binary operators
a1 The abstract domain of the first operand, op The arithmetic to boolean binary operator, a2 The abstract domain of the second operand, p The abstract domain in which we want the result of the operation
|
| baexpUna [SpecificAbstract] |
Backward abstract semantics of arithmetic unary operators
op The arithmetic unary operator, a The abstract domain of the operand, p The abstract domain in which we want the result of the operation
|
| block_c2string [Debug] |
Deserialize block of C statements
stat The block of C statements
|
| bool_expr2string [Debug] |
Deserialize boolean expressions
b The boolean expression
|
C | |
| contextMerge [GenericAbstract] |
Merge two contexts by returning the variables which are both represented by the same ids.
|
E | |
| eax_reg [SpecialVariables] |
Variable name of the register EAX
|
| ebx_reg [SpecialVariables] |
Variable name of the register EBX
|
| ecx_reg [SpecialVariables] |
Variable name of the register ECX
|
| edx_reg [SpecialVariables] |
Variable name of the register EDX
|
| environmentJoin [GenericAbstract] |
Joins two environment by joining all the ids.
|
| environmentMeet [GenericAbstract] |
Meet two environment by meeting all the ids.
|
| exception_type2string [Exceptions] |
Give the description of each exception type
t The type of the exception
|
| exceptions [Exceptions] |
The list of the current exceptions
|
F | |
| faexp [GenericAbstract] |
Forward abstract semantics of arithmetic expressions
a An arithmetic expression, context The context in which the arithmetic expression is performed, env The environment in which the arithmetic expression is performed, perhaps it will be modified
|
| faexpBin [SpecificAbstract] |
Forward abstract semantics of arithmetic binary operators
a1 The abstract domain of the first operand, op The arithmetic binary operator, a2 The abstract domain of the second operand
|
| faexpUna [SpecificAbstract] |
Forward abstract semantics of arithmetic unary operators
op The arithmetic unary operator, a The abstract domain of the operand
|
| forgetNewVariables [GenericAbstract] |
Remove from the environment the variables which have been added in the
newContext.
|
G | |
| getAsmValue [GenericAbstract] |
Get the abstract interpretation of an ASM expression
ae The ASM expression, context The context, env The environment
|
| getLastFunction [GenericAbstract] |
Get the C function in which a location is
l The location, f The reference to the set of the C functions which are known
|
| getLocationNumber [Utils] |
Return the number associated to a location
l The location
|
| getRegNameVar [Utils] |
Return the variable name of a register
reg The register
|
| getVar [GenericAbstract] |
Return a variable at a location in an environment
context The context in which vn is, vn The name of the variable, env The environment in which the variable will be searched
|
| global_statement2string [Debug] |
Deserialize global statements
stat The global statement
|
H | |
| handleException [Exceptions] |
Handle an exception and print the associated error
exception The exception
|
| handleExceptions [Exceptions] |
Handle every exception in chronological order
|
I | |
| initFunction [GenericAbstract] |
Initialize the call stack in order to prepare it before the call of a function
cCall Is it a call to a C function (respectively ASM function), callStack A reference to the call stack
|
| invMax [Utils] |
Returns the inverse of the maximum where a et b are already inversed
a 1/c, b 1/d
|
| invMin [Utils] |
Returns the inverse of the minimum where a et b are already inversed
a 1/c, b 1/d
|
| isInAbstractDomain [SpecificAbstract] |
Return true iff
n is the abstract domain p.
|
| is_register [SpecialVariables] |
Is a variable name a register's one
vn The name of the variable
|
J | |
| join [SpecificAbstract] |
Joins two abstract domains
a1 The first abstract domain, a2 The second abstract domain
|
| joinMemoryStack [GenericAbstract] |
Join the abstract values of two memory stacks
s1 The first memory stack, s2 The second memory stack
|
L | |
| labels [Types] |
Map which associates all the labels which have been encountered with their locations
|
| lastStat [SpecificAbstract] |
Last statement read.
|
| lastStat [Analysis] |
Analyse a program and write results of this analysis or exceptions encountered
l The initial location of program, program The program already located to analyse
|
| lfp [GenericAbstract] |
Calculates the least fixpoint of
env by the function e1 env The initial environment, e1 The function to apply on the environment until we have a fixpoint (or an over-approximation of it if we use a widening function), context The initial context, lastStack The initial memory stack
|
| loc2string [Debug] |
Deserialize location
l The location
|
M | |
| main [Analyser] |
Entry point of the program.
|
| matchAsmArgs [GenericAbstract] |
Adds the arguments from a memory stack to a context by a C function's definition
context The context, args_def_reversed The definition of the arguments that the C function is waiting for, stack The memory stack, env The environment
|
| matchCArgs [GenericAbstract] |
Add the abstract interpretation of a list of variables by the definition of a C function
args_def The definition of the arguments of a C function, args The list of the arithmetic expressions provided, contextToEnhance The context to update, context The context in which the arithmetic expression will be evaluated, env The environment in which the arithmetic expression will be evaluated and which will be enhanced with the new variables
|
| meet [SpecificAbstract] |
Meets two abstract domains
a1 The first abstract domain, a2 The second abstract domain
|
| minmax [Utils] |
Return the minimum and the maximum of a list.
|
N | |
| notBoolExpr [Utils] |
Apply the not function to a boolean
b The initial boolean expression
|
P | |
| postlude_asm [GenericAbstract] |
Remove the registers from a context and in the associated environment after an ASM block
context The context
|
| prelude_asm [GenericAbstract] |
Add registers to the context
context The context before the ASM block, env The environment which will be modified
|
| print_callStack [Debug] |
Print a deserialized version of a call stack
stack The reference to a call stack, env The environment
|
| print_context [Debug] |
Print a deserialized version of a context
context The context, env The environment
|
| print_environment [Debug] |
Print a deserialized version of an environment
env The environment
|
| print_memoryStack [Debug] |
Print a deserialized version of a memory stack
stack The memory stack
|
| program2string [Debug] |
Deserialize located programs
l The entry point of program, program The C program with inline assembly
|
| ptrVar2string [Debug] |
Deserialize a pointer variable
v The pointer variable
|
R | |
| raiseException [Exceptions] |
Raise an exception
t The type of the exception, generic_stat The located statement in which the exception has been raised
|
| raiseReturn [GenericAbstract] |
Raise a return (called by return/ret statement), join the return code, the return context, the return environment and the memory stack with the last ones saved
cCall Is the statement which calls it a return (respectively ret), addReturnPossibility Do we have to wait for another return/ret, returnCode The code that has been returned, returnContext The context that has been returned, returnEnv The environment that has been returned, callStack A reference to the actual call stack, stack The memory stack to return
|
| reg2string [Debug] |
Deserialize register
reg The register
|
| removeCVariables [Utils] |
Remove the C variables from a context.
|
| removeLabelsProgram [Utils] |
Remove the labels of the program and replace them by the locations associated
program The located program
|
| reset_registers [GenericAbstract] |
Reset the value of all registers except EAX which is replaced by a specified value
context The context, env The environment which will be modified, eax_value The new value of EAX
|
S | |
| setRegisters [GenericAbstract] |
Replace the registers of a context by the registers of another one
c1 The context in which the registers will be changed, c2 The context from which the registers will be get, env The environment which will be modified
|
| stat_a2string [Debug] |
Deserialize ASM statements
stat The ASM statement, indent The initial prefix of the line
|
| stat_a_block2string [Debug] |
Deserialize block of ASM statements
block The block of ASM statements, indent The initial indent of each line
|
| stat_c2string [Debug] |
Deserialize C statement
stat The C statement, indent The initial prefix of the line
|
T | |
| type2string [Debug] |
Deserialize type
t C type of variable
|
U | |
| updateVarInContext [GenericAbstract] |
Update an existing variable in a context and returns the new context
vn The name of the variable, value The value of the variable that we want to set, context The context, env The environment
|
V | |
| var_id [GenericAbstract] |
The last id used in an environment
|
| verbose [Options] |
Do we have to print backtrace when an exception is encountered
|
W | |
| widening [SpecificAbstract] |
The widening function which ensure termination of lfp
a1 The first abstract domain, a2 The second abstract domain
|
| wideningOnEnvironments [GenericAbstract] |
Apply widening on two environments by applying the widening to all the abstract domains of their ids.
|
| withoutLocs [Options] |
Do we have to hide locations in the printed version of the program
|
| withoutWidening1 [Options] |
Do we have to remove the widening and to compute the lfp by enlarging abstract domains
|
| withoutWidening2 [Options] |
Do we have to remove the widening and to compute the lfp by excluding cases and then join all the cases
|