Paper - STS
Contents
1.2. Table 2 2 DFA Result of the May Analysis Example For a may analysis the result of our example is different In a may analysis an expression just needs to be active on one path In the first block 1 x is calculated and set active As before the expression is not active after executing the while loop However after combining the branches in the second block the expression is active since it is active on the path from the first statement Now we propagate to the third and fifth block that 1 x is active Tab 2 2 shows the result of the may analysis In nearly every block the expression is active and may be calculated Thus the expression 1 x may be calculated already at every occasion but the first 2 Dataflow Analysis May Must Forwards Backwards Table 2 3 Possible DFA Classification The other two classification criteria are forward and backward analyses The difference is in which direction we go through the CFG To be more precise we go either from the unique entry to the exit of the program or the other way around i e from the exit to the entry Combining these possible analyses we have four basic types of DFA Tab depicts the four basic types of DFA 2 2 3 Formal Definition A DFA is in general defined by its dataflow equations 4 The dataflow equations for a forwards analysis look as follows For each block n in the CFG transfer inn out Ma joiNpepredn OU
3. 1 rx actual forwards transfer function for our analysis 2 for each instruction we match the instruction if it is a set operation a b 3 In case of a set operation we go on with our analysis and see if a warning is involved and so on 4 So far a call is not implemented Therefore we can not handle a call of a different function by now 5 Assemebly is also not supported 6 x 7let dolnstr _stmt instr flowval 8 match instr with 9 Set lval exp 10 Dataflow Done calculate next flow data lval exp flowval Params myWarnings _stmt 11 Call _ gt Self warning Function call not implemented setting to unsafe Dataflow Default 12 Asm _ Self warning Assembler Really Dataflow Default 13 gt Self result Instr t Extlib swap Cil_datatype Instr pretty instr 14 Dataflow Default 15 16 returns all variables of an exp x 17 let rec find lvals exp match exp enode with 18 Lval lval gt lval 27 Appendix 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 SizeOfE exp gt find lvals exp AlignOfE exp gt find_lvals exp UnOp _ exp gt find_lvals exp BinOp expl exp2 find_lvals expl find lvals exp2 CastE _ exp gt find lvals exp AddrOf lval lval StartOf lval lval Info exp gt find lvals exp gt
4. Frama C is a framework to statically analyze C code One possible way of using Frama C is to try to automatically verify C code The value analysis is a Frama C plug in that tries to verify C code However in the progress of verifying the C code one can encounter a number of warnings Reviewing them all by hand can be quite cumbersome Therefore we would like to reduce the number of warnings displayed to the Frama C user To understand how we can reduce the number of warnings displayed let us have a look at a simple example 1 void fl int x 2 int h 1 x 3 h 1 x 4 Listing 1 1 Short C Example In Lst 1 1 we see a short C program The program simply calculates the expression 1 x twice However since in the code the variable x is passed as an argument Frama C does not know the value of the variable by looking at the function The variable x could have the value 0 Hence it could be a division by zero That is not allowed for integers in C and yields a warning in the value analysis of Frama C 1 void fl int x 2 assert Value division by zero x 0 3 int h 1 x 4 assert Value division_by_zero x 0 5 h 1 x 6 3 Listing 1 2 Short C Example with All Warnings Running the value analysis of Frama C on the code in Lst gives us exactly what we expect The value analysis tries to verify the code Nonetheless it cannot guarantee that x is not equal to 0 since the range of the variable is not restr
5. xx Here we check if in the current statement either a warning is thrown in that case we add it to our list of expressions if it a new exp otherwise we add it to the redudandant warnings or if a variable of any exp is newly assigned in that case we kill all expressions with that variable x let calculate_next_flow_data lval exp flowval warn removes myWarnings _stmt let is_warning is_there_current_warning myWarnings _stmt sid in let new flow new_warn new_removes match is warning with false gt flowval warn removes true when exp exists in flowdata flowval exp flowval insert warning warn get current code annot myWarnings stmt sid removes true when check for annots get current code annot myWarnings _stmt sid warn gt Cil datatype ExpStructEqg Set add exp flowval warn insert warning removes get current code annot myWarnings stmt sid true gt Cil datatype ExpStructEq Set add exp flowval warn removes in let kill set check for lval Cil_datatype ExpStructEq Set elements new flow lval in remove flowdata kill set new flow new warn new removes xx returns true of for a given expression it contains a certain variable x let rec lval is in exp exps lval match exps with false x when Cil_datatype LvalStructEq equal x lval gt true _ Index e when lval_is_in_exp find lvals e lval gt true 28 46 _ xs gt lval_is_i
6. 1 1 1 1 2 1 1 2 1 3 1 4 1 2 1 Reassignment 3 2 2 If 1 1 1 2 Else 2 1 2 3 While 1 2 Works Y Y Y Y Y Y Statement Order Warning 1 21 1 2 1 23 1 21 1 2 1 3 1 2 1 3 2 4 1 1 2 1 3 Reassignment 2 2 2 2 3 1 If 2 1 Else 3 While 2 2 2 2 Works Y Y Y Y Y Y Table 3 2 Combinations of Statements Let us first go through a few combinations to understand the notation In Tab we have two tables each with six different combinations The first combination of the first table has two sequential statements A warning is thrown in the first statement followed by a statement throwing the same warning The implemented plug in removes the second warning correctly Hence in the Tab 3 2 we mark the combination as working The next combination is a test on reassignment We have two statements with warn ings followed by a reassignment Afterwards there are two more statements containing warnings The plug in removes the second and fourth warning correctly We have a reassignment before the third warning Therefore the expression corresponding to the warnings is not in the flow data anymore and the plug in does not remove the third warning Looking at the output of the plug in for this combination we see the expected result Thus we mark that combination as working 20 3 3 Evaluation Until now we had no flow altering statements The next combination has an if condition which alters the flow as first s
7. 4 8 assert Value division by zero t A 0 9 y 1 x 10 x 1 11 12 else 13 assert Value division_by_zero x 0 14 assert Value signed_overflow 1 1 lt 2147483647 15 assert Value signed overflow 2147483648 lt 1 x 16 via 7 x 17 18 b 19 20 if x 21 assert Value division by zero x 0 22 vela 23 24 else 25 assert Value division by zero x 0 26 assert Value signed_overflow 1 1 lt 2147483647 27 assert Value signed_overflow 2147483648 lt 1 1 28 y 1 x 29 30 Listing 3 4 Combination of Statements In case we removed the reassignment in line 11 the implemented plug in would remove nearly all warnings The combination correlates to the second combination in Tab 8 3 Without the reassignment 1 x would still be active after combining the if branches Therefore 1 x would also be active when we combine the predecessors of the while loop and we would not have to enter the while loop again Now 1 z is active reaching the if condition in line 20 Here we remove the warnings in the branches of the if block Consequently the plug in would remove every warning but the very first In case the very first warning is a false positive the reviewing effort would be reduced drastically 22 4 Future Work amp Conclusion 4 1 Future Work The whole approach by Muske et al consists of a combination of backwards ana
8. apply the algorithm automatically to our source code In the next chapter we use that knowledge and take a look at the implemented plug in and a few more examples 12 3 Plug In to Remove Redundant Warnings Frama C provides functionality to statically analyze C code Further it helps developers to implement a DFA For example the developer does not have to implement how the transfer function is applied in the analysis Therefore the must reaching analyses is implemented using the Frama C framework In this chapter we first take a closer look at Frama C After knowing how Frama C can help us we explain our implementation Lastly we ensure that the implementation works as expected and evaluate it 3 1 Frama C Frama C is an open source platform independent framework to statically analyze C code The whole framework is written in OCaml OCaml is a functional programming language It has influenced languages such as F and Scala The Frama C framework consists of different plug ins for different tasks and analyses These plug ins can be used in combination to analyze C code 2 In the process of analyzing C code these plug ins annotate the Frama C internal representation of the C code namely CIL The annotations have a unique id to distinct them Further they consist of what the plug ins could conclude analyzing the code The plug ins can see what the other plug ins annotated and work with that information Thereby one can call di
9. More precisely we test that we handle loops and their fix point iteration correctly Let us now have a look at different combinations The code in Lst 3 4 combines a number of flow changing statements with warnings and reassignments It correlates to the fourth combination in Tab 3 3 However the code in Lst 3 4 is missing the last if block compared to the fourth combination in Tab 3 3 Applying the implemented plug in to that code we see that the plug in cannot remove any warnings The plug in first sets 1 x active before the while loop and enters it with 1 x active In the while loop the plug in first removes the warnings in each branch However since we reassign x in one branch 1 x is not active anymore after combining the if branches Combining the edge from the while loop which has no warnings active and the one from line 6 we get that no warnings are active Now we have to go through the while loop again In the third block the plug in sees that it should not 21 3 Plug In to Remove Redundant Warnings have removed the warnings and adds them again by removing the annotation from the flow data We reach the if condition in line 20 with no warnings active Therefore we cannot remove any of the warnings in the branches After combining the branches 1 x is active but no warning follows 1 void fl int x 2 int b y 3 b 1 4 assert Value division by zero x 0 5 D 6 while b lt 10 7 if x 0
10. a while loop condition and therefore we have two branches in the CFG 2 Dataflow Analysis If we enter the while loop we execute the statements in line 4 and 5 Afterwards we combine the branches again The statement in line 7 is reachable in case the condition of the while loop evaluates to false The rest of the CFG is straightforward There are no more statements that influence the flow The remaining statements are now executed sequentially Further each block in the CFG has a labeling number to identify it Having the CFG we now have a graph that shows us every possible way through the program To be more precise we can track data knowing every possible way it can take through the code To know how we can track data we take a look at DFA in general 2 2 Dataflow Analysis in General In a DFA we want to have a notion of what the data can look like at certain points in the program To familiarize oneself with how and what information we can track we start by taking a look at a little example of a DFA Let us say in our DFA we want to know if an expression must have been calculated already in the current point of the program An expression is calculated if an expression has been calculated before and no variable of the expression has been newly assigned on any path reaching the current point We can apply the DFA to the CFG in Fig 2 1 2 2 1 Example In the beginning no expressions are calculated Every time an expression is
11. by exactly the same expression We also do not have to track what kind of warning it is since we save the whole expression Nevertheless there are also a few drawbacks If the array length is the same it would be nice to group the warnings together if they have the same index On the other hand the value analysis of Frama C is already good when it comes to AIOB warnings If two arrays have the same length the value analysis only throws one warning A second drawback in the implementation we compare expressions to be structurally equal The comparison yields that 1 A 2 Therefore two division by zero warnings end up in different baskets if they have different numerators However if two warnings are in the same set we are sure that they belong together Hence we use the whole expression 17 3 Plug In to Remove Redundant Warnings There is another point in which the implementation differs from the description from Muske et al in 6 The code in Lst 3 2 has an if condition In both branches a warning is thrown and we set the expression 1 x active Combining the branches we take the intersection of both branches Since 1 x is active on both branches taking the intersection of it gives us 1 x When we reach the warning after the if block the expression 1 x is active Therefore applying our tool removes the last warning Muske et al require for each redundant set one most general warning In our case we allow a warning in each branch t
12. by having a look at how the plug in calculates the result for the annotated code given in Lst 2 2 Afterwards we have a look at the properties that have to hold for the plug in Lastly we evaluate the plug in by testing it 3 3 1 Example First of all the plug in goes through the IR and collects the four annotated warnings The plug in passes the warnings to the analysis and starts the analysis using the worklist algorithm to compute the solution In the beginning the set of flow data is empty Therefore no expressions are active when the analysis starts and no warnings are to be removed The worklist contains every edge of the CFG from Fig 2 1 The first set instructionish 1 x from the first block Now the plug in has to go through the flow equations from F ig 2 4 First it calculates the gen set Hence the plug in has to check if the statement throws a warning To check if a statement throws a warning the plug in needs to access the information about the warnings passed in the beginning For our statement it sees that a warning corresponds to that statement Thus it can add the expression 1 x of the statement to the gen set Afterwards the plug in has to calculate the kill set To calculate the kill set the plug in has to take the 1val of the statement h 1 x and intersect it with the variables of the active expressions The lval of h 1 x is h and intersecting that with the only variable in the active expressions x we ge
13. by zero x 0 5 h 1 x 6 while y 7 assert Value division_by_zero x 0 8 k i 9 x y 10 11 assert Value division by zero x 0 12 h 1 x 13 assert Value division by zero x 0 14 h ay e 15 Listing 2 2 Example Code with Redundant Warnings We start with an empty set In the first block a warning is thrown Thus the gen set consists of the expression 1 x That set is propagated to the next block In the 2 3 Dataflow Analysis to Find Equivalent Warnings second block neither a warning is thrown nor a variable is reassigned resulting in no changes Another 1 x expression is generated in the third block In the fourth block x is reassigned Therefore we have to kill 1 x generated in the third block again Having both paths that enter the second block we can calculate the information in the second block From the first block we get the set with the expression 1 x and from the fourth block we get the empty set Intersecting these sets since a warning has to be active on all paths leaves us with the empty set Since there is no expression active in the second block we do not have to enter the while loop another time Going on to the fifth block we generate the expression 1 x again In the sixth block we see that the same expression throws a warning again Since the expression throwing the warning was active before we know that the warning is redundant The result is
14. fifth block we set 1 x active That information reaches the sixth block in which 1 x is calculated again In the sixth block we do not have to recalculate the expression we know that the expression is active On all the other occurrences we have to calculate Lx Block 1 3 4 2 5 6 In 0 0 1 x 0 0 1 2 Out 1 2 1 2 0 1 a 1 2 Already Calculated Y Table 2 1 DFA Result of the Must Analysis Example 2 2 2 General In general we have a few choices when it comes to a DFA The class of DFAs consists of have a must or a may or a forwards or backwards analysis Due to branching we have to decide what to do when we combine branches again That decision results in either a must or may analysis The difference between a must or a may analysis is how to combine predecessors In a must analysis we combine the sets of data with an intersection Hence in a must analysis information must be true on all paths to still hold after combining predecessors For a may analysis the predecessors are combined with a union A may analysis only requires that the information is true in one of these paths Since we cannot be certain that the program will take the path the information is true on the information may be true after the combination thus a may analysis Block 1 3 4 2 5 6 In 0 1 a 1 2 1 2 1 2 1 2 Out 0 23 1 23 0 0 23 1 2 1 2 Already Calculated Y Y Y
15. is exactly what the flow equations define An expression is killed by removing it from the flow data After removing the expression it is not active anymore Next we need to find redundant warnings In case an expression throws a warning and is not active we set the expression active by adding it to our set of expressions in the flow data but leave the annotations unchanged If the expression is active and the expression throws a warning we do not add the expression again but add the annotations to the to be removed set However it can be the case that we later realize the warning was not redundant Then we have to remove the annotation from the to be removed set We only add annotations of already active expressions to it Thereby we ensure that the first warning with a path to the other warnings is the one being displayed 14 3 3 Evaluation Now we have the result of the DFA and the warnings that can be removed The last step is to remove the warnings For this we have to go through the IR again In contrast to the first walkthrough we do not retrieve all the warnings but remove the warnings that we classify redundant Each annotation has a unique id While the plug in goes through the IR it checks for the ids of annotations we classified as redundant In case the plug in finds a corresponding annotation in the IR it removes it In the next section we take a look at how the plug in performs 3 3 Evaluation We start the evaluation
16. 1 x from the gen set is already active and thus the plug in saves the warning as redundant Step Block Gen Set Kill Set Expressions Warnings to be Removed 1 1 1 x 0 1 x 0 2 2 o 0 1 2 0 3 3 1 x 0 e Warning 2 4 4 Lia 0 Warning 2 5 2 0 0 0 Warning 2 6 3 1 x 0 1 5 0 7 4 0 1 x 0 0 8 2 0 0 0 9 5 1 x N 1 x 0 10 6 1 z 0 iz Warning 4 Table 3 1 Example Computation using the Plug In Tab 3 1 shows each step of computation The set of expressions and warnings to be removed are the flow data at the exit point of the block Now we have to remove the fourth warning To remove the warning the plug in goes through the IR When it finds the annotation with the same id as the one to be removed it removes that annotation from the IR Frama C now displays exactly what we see in Lst 2 3 16 3 3 Evaluation 3 3 2 Properties of the Tool Let us have a look at the properties of the plug in First of all we need another Frama C plug in to annotate the IR with warnings We use the value analysis to annotate the warnings However our plug in should work with every other Frama C plug in that annotates the IR with warnings Further the plug in checks the whole expression that throws a warning for structurally equality to group them It also allows a combination of warnings to make up the most general warning According to the aforementioned definition of EOI we use the whole expression to trac
17. ENSON L MONATE B PREVOSTO V AND PUCCETTI A Experience report Ocaml for an industrial strength static analysis framework SIGPLAN Not 44 9 Aug 2009 281 286 3 FLEMMING NIELSEN H N AND HANKIN C Principles of Program Analysis 2nd ed Springer 2005 4 KILDALL G A A unified approach to global program optimization In Proceedings of the 1st Annual ACM SIGACT SIGPLAN Symposium on Principles of Program ming Languages New York NY USA 1973 POPL 73 ACM pp 194 206 5 Lo c CORRENSON PASCAL CUOQ F K V P A P J S AND YAKOBOWSKI B Frama C user manual http frama c com download frama c user manual Accessed 2014 01 6 MuskE T B BAID A AND SANAS T Review efforts reduction by partitioning of static analysis warnings In IEEE 13th International Working Conference on Source Code Analysis and Manipulation SCAM 2013 2013 IEEE pp 106 115 25 Appendix 1 combine two branches 2 Take the intersection of the expressions gt MUST 3 Take the union of the warnings all need to be removed to be able to remove an annotation the third list is added x 4 let combinePredecessors _ old new 5 let a b c old in 6 let d e f new in 7 if equal a b c d e f then None else Some Cil datatype ExpStructEq Set inter a d Cil datatype Code annotation Set union b e Cil datatype Code annotation Set union c f Listing 3 combinePredecessors
18. TUHH Hamburg University of Technology Project Work Marcel Gehrke A Frama C Plug In for Finding Equal Valued Expressions Using Dataflow Analysis January 30 2014 supervised by Prof Dr Sibylle Schupp Sven Mattsen Hamburg University of Technology TUHH STS Technische Universitat Hamburg Harburg Institute for Software Systems E Software 21073 Hamburg gt a Systems UE Eidesstattliche Erkl rung Ich versichere an Eides statt dass ich die vorliegende Projektarbeit selbstst ndig verfasst und keine anderen als die angegebenen Quellen und Hilfsmittel verwendet habe Die Arbeit wurde in dieser oder hnlicher Form noch keiner Pr fungskommission vorgelegt Hamburg den 30 Januar 2014 Marcel Gehrke ili Contents Contents 1 Introduction 2 1 Control Flow Graph 2 2 2222 2 Con nn nn 2 2 Dataflow Analysis in General 22 22 Co Coon nn ua RO q do o a et ee Bere er ces 2 2 2 Gener ll E E di e a ee o e a o a a Ee Be ae G O eee 23 1 Example si e o a Sursee ana an a E Oe Ga id eee PRS eR ge ag 31 ramas Olea A nn STE NE fo Bs da eee ce sach Mae Be 3 se ie GR Be ee eee A Bo ee a in beet E SO ge ee toe ae aa GS q ae ee eee ee ae 3 3 1 Examplel ee 3 3 2 Properties of the Tool 0 o o e pe 3 34 Evaluation of Different Combinations 4 1 F t re Work ud E a OE OA a a Sa as Dia do a ia Sk en a da A a Bi
19. bliography List of Figures List of Figures 2 1 CFG of the Example Codel o o 020 0000 04 2b ee 2 2 Dataflow Equations of a Must Analysis o 2 0 Worklist Algorithm Gi 2440 05 estirados aan 2 4 Forwards Dataflow Equations to Find Equivalent Warnings 6 List of Tables nes dales IEA A a ca ae a a ae a Age An eo 2 5 DFA Result of the Warning Example without the Reassignment 2 6 Dataflow Equations Applied to Our Example 3 1 Example Computation using the Plug In 3 2 Combinations of Statementsl Cm m mn m nn 3 3 Combinations of Statements 22m m nn nn Listings 1 1 Short C Example 2 22 22 CL oo nn 1 2 Short C Example with All Warnings 2 2 2222 1 3 Short C Example with All Needed Warnings 2 1 Example Code ae s soros oea dooa ca ae ea da g a a a a a 2 2 Example Code with Redundant Warnings 2 3 Example Code without Redundant Warnings 3 1 Array Example Code ooa aaa a 3 2 Example Code for Combing Branches ooa a 3 3 Too Many Warnings Example Code 008004 3 4 Combination of Statements 2 2 2 HC e 4 1 Path Sensitivity Example o o o 4 2 Assignment Tracking Example o o e e 3 combinePredecessorsl A vii Listings RI a a A A e ae ee 27 viii 1 Introduction
20. calculated we start to track it by adding it to a set of active expressions If one of the variables of an active expression is reassigned we remove that expression from the set and stop tracking it Our DFA goes through the CFG as follows e First block The expression 1 x is calculated Thus 1 x is now active We do not reassign any variables of active expressions Hence all active expressions stay active e Third block We calculate the expression 1 x and set it active e Fourth block The statement consists of a reassignment of x 1 x is active coming from the third block We reassign a variable of an active expression Therefore we have to remove it from the set of active expressions e Second block The condition of the while loop has two predecessors in this case the first and the fourth block Since the expressions must be active on every path and 1 x is only active on one path there are no active expressions reaching the second block e Fifth block In the statement we calculate the expression 1 x and set it active once more e Sixth block The last statement also consists of the calculation of the expression Lie 2 2 Dataflow Analysis in General The code in Lst 2 1 calculates the expression 1 x four times Tab 2 1 depicts the result of the DFA i e what expression is active and already calculated in a block From the result we can see that the expression is only active once when it is calculated In the
21. code Knowing how data can flow we can track information of interest For our purpose of finding equivalent warnings to group them warnings are the information of interest To be more precise we want to know if a warning at a certain point in the program is redundant to a warning thrown before In this chapter we will first have a look at what exactly a CFG is Afterwards we use the CFG in a DFA and have a closer look at DFA in general to know how we can track information of interest Knowing how a DFA can look like we will apply it to our case and track warnings 2 1 Control Flow Graph In this section we define what a CFG is and have a look at a little example of a CFG The example will be used throughout this chapter 1 void fl int x int y NES 2 int h 1 2 3 while y 4 h 1 x 5 de 6 T h 1 x 8 h 1 x 9 Listing 2 1 Example Code Figure 2 1 CFG of the Example Code Fig 2 1 shows us how a CFG for the code in Lst 2 1 looks A CFG is a directed graph The edges show how we can traverse through the code The nodes of the graph correspond to blocks in the code Each block consists of one statement Thus there cannot be any kind of branching in a block Branching can be achieved by e g if conditions or while loops To see how the program code and the CFG correlate we start by mapping it First of all we have the first statement of the code int h 1 x The first statement is followed by
22. decessors function From the first block the plug in gets the information that the flow data consist of the ex pression 1 x and from the fourth that the flow data is empty Intersecting the sets of information it gets that no expressions are in the flow data entering the second block Now the plug in has to add the edges 2 3 and 2 5 to the worklist again to propagate the information that actually no expressions are in the flow data Going into the while loop a second time the plug in sees again that it has 1 x in the gen set This time there is no active expression Therefore the expression is put in the gen set However the plug in marked that warning as redundant before but it now knows that this warning is not redundant Hence it has to remove that warning from the set of redundant warnings in the flow data The rest is exactly the same as explained above for the while loop Entering the second block again the plug in applies the combinePredecessors function It gets the same result as before and does not have to propagate anything new The next edge in the worklist is the edge 2 5 Entering the fifth block the plug in has no expression active The gen set of the fifth block consists of 1 x and the plug in does not kill anything Leaving the fifth block the expression 1 x is in the flow data and the plug in propagates it to the sixth block The sixth block has the set instruction h 1 x with a corresponding warning The expression
23. depicted in Tab Block 1 3 4 2 5 6 In 0 0 1 2 0 0 1 2 Out 1 2 1 x 0 1 2 1 z Redundant Warning Y Table 2 4 DFA Result of the Warning Example 1 void fl int x int y a 3 int h 4 assert Value division by zero x 0 5 h 1 x 6 while y 7 assert Value division by zero x 0 8 9 h 1 a x y 10 11 assert Value division by zero x 0 x 12 h 1 x 13 h 1 ur 14 Listing 2 3 Example Code without Redundant Warnings In this example we could only remove one of the four warnings However that is still 25 of the warnings Lst 2 3 shows the result of the DFA without the reassignment in the fourth block e First block The expression 1 x throws a warning Thus 1 x is now active e Third block We set the expression 1 x active since it throws a warning e Second block The intersection of the edges from the first and third block yields 1 x as active Without the reassignment the expression 1 2 survives the intersection 2 Dataflow Analysis e Fifth block In the statement the expression 1 x which is already active throws another warning e Sixth block The last statement also consists of the active expression 1 x throwing a warning Block 1 3 2 5 6 In 0 1 2 1 2 1 2 1 2 Out 1 2 1 2 0 0 1 2 1 2 Redundant Warning Y Y Y Table 2 5 DFA Result of t
24. e worklist information is calculated as specified by the dataflow equations Every time we calculate new information for an edge 1 1 we add all possible edges 1 1 to the worklist If there is new information we have to propagate we make sure that we pass it on Thereby we ensure that every time we add new information we have a look if it influences any other statement One can prove that the iteration reaches a fixed point meaning the worklist algorithm stabilizes terminates and computes the least solution 3 Until now we have presented a general DFA Further we provided the means to compute the result of a DFA automatically Let us now have a look at a DFA described by Muske et al in 6 to find equivalent warnings to remove redundant warnings 2 3 Dataflow Analysis to Find Equivalent Warnings The main idea of the DFA is similar to the must analysis presented in the last section Now the warnings become the information of interest In case an expression throws a warning we put it in the gen set If an expression is in the gen set but not in the kill set we set it active We store all expressions that have at least one variable reassigned in the kill set and set them not active 2 3 1 Example Lst 2 2 shows the program of Lst annotated with all warnings thrown Using infor mation about warnings we have we can apply the DFA to find equivalent warnings 1 void fl int x int y E 3 int h 4 assert Value division
25. ew more warnings and is more precise Lst 3 2 contains another example where the output of the plug ins differ The built in function is not able to remove the warning corresponding to line 12 As aforementioned the plug in does remove that warning and is more precise in this case 1 void fl int x 2 int h 3 assert Value division_by_zero x 0 4 he 17x 5 if x 0 6 assert Value division by zero x 0 7 h 1 x 8 else 9 assert Value division_by_zero x 0 10 assert Value signed_overflow 1 1 lt 2147483647 11 assert Value signed_overflow 2147483648 lt 1 1 12 h 1 x 13 Listing 3 3 Too Many Warnings Example Code The last difference is that sometimes an expression throws additional signed overflow warnings in a branch due to over approximation An example of that shows Lst 3 3 The plug in removes these additional warnings if it has a redundant warning for that expression In case an expression is active and throws a warning again the plug in adds all annotations of that expression to the to be removed set Therefore it removes these warnings The built in plug in cannot remove the warnings because they have other predicates and are not redundant to another warning The expression probably should not have thrown these additional warnings to start with In the else branch the valuation of can only be restricted That means that the x in the else branch cannot obtain a
26. fferent plug ins in combination Further Frama C provides the means to register new plug ins A newly written plug in can then be combined with already existing plug ins One of the probably most widely used Frama C plug in is the value analysis The value analysis plug in is a correct static analyzer 5 Correct means that if anywhere at run time a bug can occur it warns about it The value analysis can be used to verify C code against provided specifications In case one does not provide any specifications the value analysis only tries to find common run time bugs e g division by zero or array index out of bounds To analyze the code it is transformed into the CIL intermediate representation IR If the value analysis or many other plug ins find a possible bug they annotate the IR with a warning The framework also provides a number of modules with functionalities to help the user implement their own plugin One of the modules provides functions for either a forwards or backwards DFA To use that module one only has to define the transfer function and the join A function to implement the join is how to combine predecessors After we specify these functions Frama C applies the DFA to the C code While applying the DFA Frama C uses a worklist algorithm to compute a solution to the dataflow equations 3 2 Implementation of the Plug In As Frama C is written in OCaml the new plug in is also written in Ocaml We imple mented the plug in us
27. hat can be removed In case a statement throws a warning we save everything to the right of the equal sign as expression That means that if h 1 x throws a warning we save the expression 1 x In case b a 1 x throws a warning we save the expression a 1 z Now we can start with the analysis Initially we pass the analysis all the annotations that belong to warnings The most interesting functions for us are combinePredecessors and doInstr In the combinePredecessors function the join we specify that we have a must and not a may analysis Therefore we use the intersection on the expressions we track in the combinePredecessors function The transfer function is implemented in the doInstr function Every time we see a set instruction e g h x we go through the flow equations from Fig 2 4 First of all the plug in checks the annotations retrieved early and passed to the analysis if we find an annotation corresponding to the statement of the instruction If the plug in finds an annotation it knows the expression of the statement throws a warning Otherwise the statement does not throw any warning If the plug in finds any annotation that relates to the statement the expression of the statement makes up the gen set that is then added to the flow data For the kill set the plug in has to check the left value lvals of every instruction Knowing the lval the plug in kills every expression of the flow data that contains the lval That
28. he Warning Example without the Reassignment Now the warning is active in every block after the first block as ca be seen in Tab Therefore every but the first warning is redundant and could be removed Without the reassignment we could remove 75 of the warnings 2 3 2 Formal Definition Until now we explained the algorithm for the DFA by means of an example Fig 2 4 depicts the formal definition of the forwards dataflow equations 6 The analysis is called must reaching expression analysis It tracks equal valued expressions to find redundant warnings Hence the expression must reach the current point in the program from every path The equations use n for the corresponding node in the CFG EOI stands for expression of interest The EOI can be defined differently for different types of warnings An example would be to only use the denominator for a devision by zero warning However we track the whole expression To understand the equations one has to recall that statements are translated to nodes in a CFG The entry of node n is called In and the exit Out Let us show that the formal definition coincides with the explanation above The first equation in Fig 2 4 defines the entry of each block Starting the DFA we cannot have any active warning Hence if we have the first block we start with the empty set Otherwise we are in the CFG and we take the intersection of all the predecessors to calculate In The data we have exiting a bloc
29. here assignment tracking could help us Tracking that y x we can conclude that the warnings corresponding to line 2 and 4 are actually redundant Still even though there are a few topics open the plug in already is a working prototype 23 4 Future Work amp Conclusion 4 2 Conclusion The goal of this project has been to reduce the efforts of reviewing warnings To that end a plug in for Frama C was implemented The plug in is based on the forwards analysis described by Muske et al in 6 For the plug in to work it needs another Frama C plug in to annotate the IR with warnings first To remove redundant warnings the plug in finds equal valued expressions that throw warnings using a DFA Having the set of equal valued expression and the corresponding warnings the plug in has to display the most general warning for each set of equal valued expression We tested the plug in to ensure that we only remove warnings that can be removed To be more precise we handle the fix point finding for loop iterations correctly By displaying fewer warnings while still providing the same information the reviewing effort of the user is reduced in most cases Therefore using the plug in can be of great help for the user 24 Bibliography 1 Cuoq P Minimizing alarms http blog frama c com index php post 2012 03 12 Minimizing alarms Jan 2014 Accessed 2014 01 2 Cuoq P SIGNOLES J BAUDIN P BONICHON R CANET G CORR
30. icted Thus Frama C annotates the code as depicted in Lst 1 2 The assertions in line 2 and 4 originate from warnings The assertion in line 2 and line 4 are redundant They are redundant since the warnings are thrown by equal valued expressions In this case the warnings are thrown by the same expression without any of its variables being reassigned in between the warnings Further when the user reviews these warnings it is sufficient for him to look at either of these redundant warnings Therefore Frama C could display only the annotation in line 2 In Lst 1 3 we see the version where the redundant warning in line 4 is removed One idea to reduce the number of warnings displayed is to group redundant warnings Redundant warnings are warnings thrown by equal valued expressions T Muske A Baid and T Sanas present an approach to group redundant warnings in their paper 1 Introduction Review Efforts Reduction by Partitioning of Static Analysis Warnings 6 The idea is to track equal valued expression in case they throw a warning Equal valued expressions evaluate to the same result during run time Warnings of equal valued expressions can be grouped together in a redundant set Showing just one warning of each redundant set can reduce the overall number of displayed warnings However Frama C cannot display just any warning of the redundant set but has to display the most general warning The most general warning has a path in
31. ill it Concluding the formal definition coincides with the informal explanation Next we can apply the equations to our CFG to see how these work Starting with the first block we get that the In is the empty set since it is the entry block In the first block we have a warning Therefore the gen set contains the expression 1 x Now we have to check the kill set The variable h is modified in the first block Though no expression of Gen Ini which evaluates to 1 x contains h Thus the intersection of h and x is empty and we do not kill anything At the exit of the first block we have Out 1 2 Assuming that Ing is the empty set we get that Outs is 1 x with the same ar gumentation as in the first block Iny is the intersection of all its predecessors The fourth block has the third block as the only predecessor leaving us with Out3 Ina The fourth block has no warning so the gen set is empty However we modify the variable x The set modified Vars contains the left side of the statement namely x In tersecting the set containing x with the variables of 1 x results in the non empty set x Therefore 1 x is in the kill set The set at the exit of block four is therefore Out 1 xr 1 2 0 Now we can calculate Ina It is the intersection of Out and Outy Intersecting 1 x with leaves us with The second block has no warning and we do not modify any variable Therefore we have Ing Out Knowing that Ou
32. ing Frama C Fluorine 20130601 on a Mac OSX 10 8 with Ocaml 13 3 Plug In to Remove Redundant Warnings version 4 00 1 To implement the DFA described by Muske et al in 6 the plug in needs to know the expressions that throw a warning As aforementioned Frama C plug ins such as the value analysis can annotate the internal representation with the warnings they threw Therefore we first need to be able to go through that IR and retrieve all the warnings other plug ins annotated To that end Frama C provides the in place visitor module Such an in place visitor can be used to go through the IR We now have to collect all the annotations that are warnings from the IR Collecting the annotations we also get the information which statement the annotation belongs to Having the prerequisites for the analysis we can start to implement it To implement the analysis we use the Dataflow module of Frama C The Dataflow module provides a module for a forwards analysis and a backwards analysis We are interested in the module for a forwards analysis To use the module all its functions need to be specified That means we need to provide the implementation for every function of the module The functions that we have to specify correlate to the join and transfer functions Further we need to specify our flow data Flow data are our information of interest However the flow data consists not only of a set of expressions but also of a set of annotations t
33. iteratively compute the result of the dataflow equations Fig 2 3 depicts the algorithm In the algorithm W is the worklist and F is the flow Stepl Initialization of W and Analysis W nil for all 1 1 in F do W cons l 1 W for all l in F or E do if l E then Analysisll else Analysis l Lr Step2 Iteration updating W and Analysis while W 4 nil do l fst head W l snd head W W tail W if fi Analysis Z Analysis l then Analysis l Analysis l U fi Analysis l for all 1 with 1 17 in F do W cons I 1 W Step3 Presenting the result for all l in F or E do MFPentry l Analysisll MF Persall f Analysisl Figure 2 3 Worklist Algorithm The flow consists of the edges of the CFG The edges can be directed in either a forwards or a backwards manner Further E stands for the unique entry point of the analysis specifies the initial or final analysis information We specified it to be the empty set because our analysis starts with no calculated expressions The transfer function is fi f Analysis l computes the information for the block l Lastly we still need the join from the dataflow equations LI is the join and can either be an intersection or a union 2 Dataflow Analysis In the worklist algorithm we find every part as defined in the dataflow equations We start with all edges included in the CFG in the worklist Going through the edges of th
34. k is defined by what we had entering the block as well as what needs to be generated or killed during the block To know what needs to be generated we need to have a look at the definition of Genn The gen set contains the EOI if the current block has a warning Otherwise the gen set is empty Therefore we only set an expression as active if that expression throws a warning Finally we have a look at the kill set In case no variable is modified or reassigned in the block we kill nothing Otherwise we search for all the expressions that are active and contain any modified variables The expressions returned by the killInfo are all those with a modified variable To find these we take the intersection of the modified variables with the variables used in each active expression If the intersection 10 2 3 Dataflow Analysis to Find Equivalent Warnings 0 n is the entry block Inn N Out otherwise pEpredecessors n Out Genn Inn Kill Genn Inn e n has a warning with e as its EOI Gen 0 otherwise killlnfo X n n modifies at least one variable 0 no variable is modified by n Kill X killlnfo X n fee X usedVars e N modi fiedVars n 0 usedV ars e r values from expression e modifiedVars n l values from program statement n Figure 2 4 Forwards Dataflow Equations to Find Equivalent Warnings 6 is not empty we know that the expression contains the modified variable and we need to k
35. k it Muske et al track only the denominator for a division by zero or the index of an array for an array index out of bound AIOB warning However one has to save what kind of warning the EOI referred to For the division by zero that approach should work well Saving only the index for an array for AIOB warning can lead to a problem 1 void fl int x 2 const int a 0 1 2 3 4 5 6 7 8 9 3 const int b 0 1 2 3 4 4 assert Value index bound 0 lt x 5 assert Value index bound x lt 10 x 6 int h alx 7 assert Value index bound x lt 5 8 int h b x 9 5 Listing 3 1 Array Example Code The example of Lst 3 1 illustrates the problem In case we only save the x as EOI we might group these warnings together However we access arrays of different sizes Removing the second warning would be unsound but is possible by following the flow equations of Fig 2 4 Removing the second warning we would run into problems if x 5 9 In that case we would conclude that the first warning is a false positive but the second warning s fault occurs However since the first is a false positive we would not look at the second warning If we would only save the denominator for a division by zero and the index for an AIOB we could not differentiate between a x and 1 x since we would save x in both cases Saving the whole expression however ensures that we only compare warnings thrown
36. l has all the crucial information seeing only the most general warning To sum it up the described algorithm can reduce the effort of reviewing the warnings The user has to check whether a warning is a false positive or can lead to an actual fault As mentioned before showing the most general warning to be a false positive the user does not have to look at the other warnings of the redundant set If the fault of the warning can occur the user will also have to have a look at the warnings that are redundant individually Using this algorithm Frama C does not only show less warnings to the user while still providing him with all the information he had before but also reduce the effort of the user to review warnings In the following we will first take a look at dataflow analysis in Chapter 2 A dataflow analysis is the method we apply to find redundant warnings as proposed by Muske et al in 6 After this theoretical part we will have a look at the implemented tool and how it performs in Chapter 3 Lastly in Chapter 4 we have a look at possible improvements 2 Dataflow Analysis A dataflow analysis DFA is a class of methods to statically analyze code Using a DFA one tries to gain information about the state at a certain point in the program To be able to gain the information we need to know how the data can possibly flow through the program A control flow graph CFG of a program provides the details how the data can flow in the
37. lysis and forwards analysis to find redundant warnings So far the plug in implements the forwards analysis but the backwards analysis is missing Combining these analyses one can find larger sets of redundant warnings Therefore fewer warnings need to be displayed which could reduce the reviewing efforts even more Further using Frama C it might be better to use annotations instead of expressions Tracking annotations we can compare them by their predicates Using these predicates we probably can group more annotations together as we do now However it could be harder to find the annotations we need to kill without saving the expressions 1 void fl int x 2 int h 3 if x 0 4 h 17x 5 else 6 h 1 x 7 Listing 4 1 Path Sensitivity Example Having the analysis as described by Muske et al there is still room for improvements We could add some path sensitivity to the analysis Lst 4 1 is an example where path sensitivity can improve the result of the analysis In case the condition of the if holds we know that the expression in line 4 cannot be a division by zero fault Here we can propagate that x 0 to the then branch Therefore we do not have to display a division by zero warning in the then branch unless we reassign x to 0 Further we could try to track assignments 1 void fl int x int y 2 int h 1 x 3 y X 4 h 1 y 5 7 Listing 4 2 Assignment Tracking Example Lst 4 2 shows an example w
38. n_exp xs lval 47 48 let lval in exp exp lval 49 let lvals of exp find lvals exp in 50 Ival_is_in_exp lvals of exp lval 51 52 xx check if a variable is contained in an expression and contain a list of all exp that contain that variable x 53 let rec check for lval flowval lval match flowval with Zul 55 x xs when lval_in exp x lval x check for lval xs lval 56 _ xs check for lval xs lval 57 58 xx remove the expressions from the flow data in which a newly assigned variable is x 59 let rec remove_flowdata kill_set flowval match kill_set with 60 flowval 61 x xs gt xSelf result kill a Cil datatype ExpStructEq pretty xz remove flowdata xs Cil_datatype ExpStructEq Set remove x flowval 62 63 xx insert a list of annotations in a set of annotations 64 let rec insert_warning old new match new_ with 65 old 66 x xs insert warning Cil_datatype Code_annotation Set add x old xs 67 xx remove a warning from the set x 68 let rec remove warning old new match new with 69 old 70 x xs gt remove warning Cil_datatype Code_annotation Set remove x old xs 71 ex check if annotation is in the set x 72 let rec check_for_annots annots flow match annots with 713 false 74 x _ when Cil_datatype Code_annotation Set mem x flow gt true 75 2x gt check_for_annots xs flow Listing 4 dolnstr 29
39. ny value that is not possible before the if block Hence either that warning should be also displayed before the if block or should not be possible in the branch The outputs of both plug ins are correct we however are more precise We reported the superfluous signed overflow warnings and they will not appear in the next version of the value analysis anymore 19 3 Plug In to Remove Redundant Warnings 3 3 4 Evaluation of Different Combinations So far in this chapter we have provided an overview of the implementation and compared it to a built in plug in The results of the comparison are promising Both plug ins return about the same result Further the few differences can be explained by the implementation Furthermore the outputs of both plug ins are sound they only differ in precision In this subsection we want to evaluate the correctness of the implemented plug in To evaluate it we conduct a case study In the case study we test different possible combinations of C statements Tab 3 2 and Tab 3 3 depict the combinations tested The statements are ordered as they occur in the code In case a warning appears in a while loop we attach that warning to the loop In terms of labeling that means if a while loop is the first statement then it has the number 1 If a warning is the first statement in the while loop we label it with 1 1 and so on Statement Order Warning Laia AL
40. o combine to the most general warning 1 void fl int x 2 int h 3 if x 0 4 assert Value division by zero x 0 5 Ros 1 8 6 else 7 assert Value division_by_zero x 0 8 assert Value signed_overflow 1 1 lt 2147483647 9 assert Value signed_overflow 2147483648 lt 1 1 10 h 1 3 11 assert Value division_by_zero x 0 12 h 1 x 13 Listing 3 2 Example Code for Combing Branches Combining the branches we have the same predicate that has to hold in each branch Showing the warnings in the branches we have to make sure that the predicate holds in every branch If it holds in every branch it also holds after combining the branches Therefore we can remove the warning after the if block with the same predicate Warn ings thrown by the same expression produce annotations with same predicates Further displaying the warnings in the branches also works if x is reassigned in a branch and afterwards the same expressions throws a warning again In this case we still have the same predicate in each branch and if it holds in each branch it also holds after the if block Hence as long as we have the same predicate in every branch we can assume that it also have to hold after the combination of the branches Having an idea of how the plug in works and it properties we still need to see how it performs 3 3 3 Evaluation Against a Built In Function To see how the implemented pl
41. t is the empty set we also know that our assumption for Ing holds and that we do not have to enter it again The fifth and sixth block are still not calculated Outa defines Ins that is the empty 11 2 Dataflow Analysis set In the fifth block we generate the expression 1 x again and kill nothing Ing is equal to Outs since it is its only predecessor In block six we generate 1 2 again but since it already is in the active set it is not added again Further we do not kill anything Therefore we know that we can group the warning from block 5 and 6 together Furthermore the warning from the fifth block has a path to the warning in the sixth block but not the other way around Earlier we defined the most general warning as the one having a path to all others Knowing that the warning from the fifth block is the more general one we can remove the warning in the sixth block Hence we get the same result as depicted in Lst 2 3 Tab 2 6 depicts the application of the dataflow equations to our example from Fig 2 1 Further the results depicted in Tab 2 4 and Tab 2 6 are the same Therefore the informal and the formal definition compute the same result Block 1 3 4 2 5 6 In 0 0 1 2 0 0 1 x Out 0 23 1 23 0 0 1 a 1 2 Redundant Warning Y Table 2 6 Dataflow Equations Applied to Our Example Now we know the theoretical background to find equivalent warnings and how to
42. t an empty set Since the intersection is empty our kill set is empty as well Therefore the flow data consist of the expression 1 x after the first block The worklist algorithm propagates that information onwards to the next block Since the information on the edge 1 2 changes from the empty set to 1 x the plug in adds the edges 2 3 and 2 5 to the worklist In the second block it does not have to do anything at the moment Going on with the edge 2 3 the plug in enters the while loop and has the expression 1 x in the flow data The third block has the set instructionh 1 x Further the statement has a corresponding warning Putting the expression 1 x in the gen set the plug in sees that the expression is already active Therefore it marks that annotation as redundant by adding to the to be removed set in the flow data For the same reason as in the first block the kill set is empty in the third block Taking the next edge to the fourth block the flow data still consists of the expression 1 x 15 3 Plug In to Remove Redundant Warnings The set instruction of the fourth block is x y There is no corresponding warning to that statement Therefore the gen set is empty The lval of the expression is x Intersecting that x with the variable of 1 x we get x Thus the kill set consists of 1 x Removing the expression 1 x from the flow data results in an empty set Entering the second block again we apply the combinePre
43. tatement We split up the if block into the if branch which is actually the then branch and the else branch Therefore the first statement is the then branch of the if block In the then branch the first statement includes a warning denoted by 1 1 In case we had another statement in the then branch it would get the label 1 2 The else branch is the next statement and contains one warning After the if then else block we have another warning in the last statement The plug in removes the last warning correctly as explained in subsection when we looked at the example in Lst Statement Order Warning 1 1 1 1 2 1 2 1 3 1 4 1 5 1 1 2 1 1 2 2 1 3 1 4 1 6 1 7 1 Reassignment 5 If 1 1 2 4 2 1 3 6 Else 1 2 3 5 2 2 4 7 While 1 2 Works Y Y Statement Order Warning 1 1 1 2 1 1 3 1 2 1 3 1 4 1 5 1 1 2 1 1 2 2 1 3 1 4 1 6 1 7 1 Reassignment 2 1 2 5 If 1 2 2 4 2 1 3 6 Else 1 3 3 5 2 2 4 7 While 1 2 Works Y Y Table 3 3 Combinations of Statements We test different combinations of warnings and reassignments composed with state ments that can alter the flow All of these tests return the expected result Further we include only the while loop but not also the for loop as a statement because the for loop gets translated into a while loop internally at least in the value analysis of Frama C Mainly we test that an expression has to be active on every path
44. the code to all other warnings of the redundant set In the analysis we apply which we explain in depth in Chapter 2 we always have a most general warning or at least a combination of warnings that make up the most general warning Displaying the most general warning provides all crucial information to the user 1 void fl int x assert Value division by zero x 0 int h 1 x h 1 x or Wh Listing 1 3 Short C Example with All Needed Warnings Let us now check that the user still has all the necessary information There are two possibilities for the most general warning Either it is a false positive or the fault can actually occur In our example if the warning is a false positive the second warning will be one as well In that case the first warning is sufficient for the user False positive in this case means that Frama C throws a warning of a fault that will not occur If the warning s fault occurs the user also has to look at the other warnings of the set In our case both warnings would lead to a fault Fixing the warning in line 2 would result in both warnings to disappear Another possibility is that only the first warning s fault occurs and the second is a false positive An example of that would be a branch that restricts the valuation of x to be not equal to zero Then the second warning would be a false positive and could be removed even though the first warning could lead to a fault Hence the user stil
45. tn The transfer function defines what we do in a block Hence the transfer function specifies what kind of information we generate and what information we kill 0 n is the entry block Iin N Out otherwise pepredecessors n Out Gen Inn Kill Gen Inn Ca e ifn compute 0 otherwise Kill X m n n modifies at least one variable 0 no variable is modified by n killlnfo X n fee X usedVars e NmodifiedVars n 0 usedV ars e r values from expression e modifiedVars n l values from program statement n Figure 2 2 Dataflow Equations of a Must Analysis 2 2 Dataflow Analysis in General To differentiate between a may and must analysis the join function is either the intersection or union For a backwards analysis out and in are exchanged Further we join the successors and not the predecessors Fig 2 2 shows the dataflow equations of the must analysis from subsection 2 2 1 The join is the intersection defined in the In equation We define how to track data using the transfer function in Out Genn Inn Kill Genn Inn In the transfer function we generate arithmetic expressions We kill expressions in case a variable of that expression is modified Dataflow equations also provide us with the means to compute a DFA automatically 2 2 4 Worklist Algorithm To automatically compute the result of a DFA one can use a worklist algorithm The worklist algorithm is a way to
46. ug in performs we compare the output of the plug in against the output of a built in plug in of the value analysis The value analysis has a not very well known option remove redundant alarms 1 The option has the goal to remove redundant alarms Therefore it has the same goal as our analysis but it only works in combination with the value analysis From what we understand the remove redundant alarms option is tracking the annotations and the modification point of that annotation Further if two annotations have the same modification point the built in 18 3 3 Evaluation function compares the predicates of the annotations That means if two annotations have the same modification point and both have a warning with the same predicate let us say x 0 then they remove a warning They analyze the code in a forward manner Now we can provide both plug ins with the same C code to analyze and compare the output While we apply different examples to the plug ins and compare the outputs of both analyses we can see that they return nearly the same result However there are a few differences that can be explained by the way the warnings are tracked The built in option groups warnings thrown by expressions like 1 x and 2 x together because the annotations have the same predicate The implemented plug in does not group them together because it tests on structural equality for the whole expression Therefore the built in function can remove a f
Download Pdf Manuals
Related Search