API Documentation
We explain the main APIs used in writing the specification and configuring RGSE.
Functions for making a variable symbolic
makeConcolicInteger("sym_m", "a"): This function will make an integer variable symbolic (denoted as sym_m), and initialize it to the concrete integer value a.
makeConcolicChar("sym_c", "c"): This function will make a char variable symbolic (denoted as sym_c), and initialize it to the concrete char c.
Function for building the FSA
FiniteStateAutomaton getForwardFSA() : This function is used to specify the regular property as a deterministic finite state automaton (FSA).
Functions in class FiniteStateAutomaton
(1). FiniteStateAutomaton() : The construction function of the class FiniteStateAutomaton , and it will return an empty finite state automaton.
(2). createState(Point p) : Create a state in FSA. The parameter p is a point that specifies a location in the coordinate space.
(3). addTransition(Transition t) : Add a transition to the FSA, and parameter t is the transition to be added. Specifically, a transition can be constructed by invoking function "new FSATransition(s0, s1, "I")", which means executing event I can drive state s0 to state s1.
Functions in class MonitorWithDFA
The functions in class MonitorWithDFA are used to build a Java monitor.
(1). MonitorWithDFA(FiniteStateAutomaton fsa) : Construct a monitor according to the given FiniteStateAutomaton fsa.
(2). addSensitiveEvent(String typeName, String methodName) : Suppose the monitor is constructed by an FSA fsa, then this function is used to describe the transition events in fsa. For example, suppose instruction instr is a method call instruction, if the class name of the invoked method equals parameter typeName and the method name equals parameter methodName, then instr is a sensitive event of the regular property.
(3). addMethodNameChar(String methodName, Char ch) : This function associates a sensitive method named methodName with the transition label ch in the FiniteStateAutomaton fsa. For example, suppose the FiniteStateAutomaton fsa has a transition (s0, s1, "I"), if we invoked addMethodNameChar("init", "I"), then when we encouter a instruction that invoked a method named init, state s0 will be updated to state s1.
Function for initializing arguments.
initArgs(String[] args) : This function sets the running configuration. The parameter args is an array with seven string elements, and they represent call string bound, property guided, refinement flag, iteration number, iteration period, result file name, and slicing flag, respectively. For example, suppose the args equals {"1", "1", "0", "-1", "0,0,100,0","","0"}, then the call string bound is 1, and RGSE will run in the guiding mode with no refinement, no iteration threshold, 100 seconds time threshold (the types of the four elements are hour, minute, second, millisecond, respectively), empty result file, and no slicing.