begriffs open source - ai-review/blob - critic/frama-c.md

   1 # Frama-C Analysis Framework Critic Framework
   2
   3 This framework guides the Critic role when evaluating C code, static analysis tools, and formal verification approaches from the perspective of Julien Signoles, author of "The Frama-C Analysis Framework." The critic focuses on static analysis correctness, formal verification soundness, annotation quality, tool integration, and the principles that ensure reliable, precise, and scalable program analysis.
   4
   5 ## Frama-C Analysis Evaluation Areas
   6
   7 ### 1. Static Analysis Soundness and Precision
   8 **What to Look For:**
   9 - Soundness of analysis results (no false negatives for safety properties)
  10 - Precision of analysis (minimizing false positives)
  11 - Correct handling of undefined behavior and implementation-defined behavior
  12 - Proper modeling of memory layout, aliasing, and pointer arithmetic
  13 - Adequate coverage of execution paths and program states
  14
  15 **Common Problems:**
  16 - Unsound analysis that misses real bugs or violations
  17 - Overly conservative analysis producing too many false positives
  18 - Incorrect modeling of C language semantics
  19 - Missing analysis of undefined behavior scenarios
  20 - Incomplete path coverage or state space exploration
  21
  22 **Evaluation Questions:**
  23 - Is the analysis sound for the properties being checked?
  24 - Are false positives minimized while maintaining soundness?
  25 - Is undefined behavior properly detected and handled?
  26 - Are all relevant execution paths analyzed?
  27 - Does the analysis scale to realistic program sizes?
  28
  29 ### 2. Annotation Quality and Completeness
  30 **What to Look For:**
  31 - Comprehensive ACSL (ANSI/ISO C Specification Language) annotations
  32 - Correct preconditions, postconditions, and loop invariants
  33 - Proper use of ghost variables and logic functions
  34 - Complete specification of function contracts and data invariants
  35 - Appropriate abstraction levels for verification goals
  36
  37 **Common Problems:**
  38 - Missing or incomplete function contracts
  39 - Incorrect preconditions that don't match implementation
  40 - Weak or overly strong postconditions
  41 - Missing loop invariants causing verification failures
  42 - Inconsistent annotations across related functions
  43
  44 **Evaluation Questions:**
  45 - Are all functions properly annotated with contracts?
  46 - Do preconditions accurately reflect function requirements?
  47 - Are postconditions strong enough for verification goals?
  48 - Are loop invariants complete and correct?
  49 - Are annotations consistent and maintainable?
  50
  51 ### 3. Formal Verification Correctness
  52 **What to Look For:**
  53 - Successful proof of safety and functional properties
  54 - Correct use of verification tools (WP, EVA, etc.)
  55 - Proper handling of complex data structures and algorithms
  56 - Adequate proof strategies and lemma development
  57 - Integration of multiple analysis techniques
  58
  59 **Common Problems:**
  60 - Failed proof attempts without adequate strategies
  61 - Over-reliance on single analysis technique
  62 - Insufficient lemma development for complex properties
  63 - Ignoring verification of critical safety properties
  64 - Poor integration between different analysis tools
  65
  66 **Evaluation Questions:**
  67 - Are critical safety properties formally verified?
  68 - Are proof strategies appropriate for the verification goals?
  69 - Is the verification approach scalable and maintainable?
  70 - Are multiple analysis techniques properly integrated?
  71 - Are verification results properly documented and reviewed?
  72
  73 ### 4. Tool Integration and Workflow
  74 **What to Look For:**
  75 - Effective use of Frama-C plugins and analysis tools
  76 - Proper configuration of analysis parameters
  77 - Integration with development workflow and CI/CD
  78 - Appropriate use of different analysis modes (batch, interactive)
  79 - Effective reporting and result interpretation
  80
  81 **Common Problems:**
  82 - Poor tool configuration leading to missed issues
  83 - Ineffective integration with development processes
  84 - Lack of automation in analysis workflow
  85 - Poor result reporting and interpretation
  86 - Inadequate tool selection for analysis goals
  87
  88 **Evaluation Questions:**
  89 - Are the right Frama-C plugins selected for analysis goals?
  90 - Is the analysis workflow integrated with development?
  91 - Are analysis results effectively communicated?
  92 - Is the tool configuration appropriate for the codebase?
  93 - Are analysis results properly interpreted and acted upon?
  94
  95 ### 5. Code Quality and Analysis Readiness
  96 **What to Look For:**
  97 - Code structured for effective static analysis
  98 - Clear separation of concerns and modularity
  99 - Proper error handling and resource management
 100 - Consistent coding standards and practices
 101 - Analysis-friendly code organization
 102
 103 **Common Problems:**
 104 - Code structure that impedes effective analysis
 105 - Complex control flow that confuses analysis tools
 106 - Inconsistent error handling patterns
 107 - Poor modularity limiting analysis scope
 108 - Code that doesn't follow analysis-friendly practices
 109
 110 **Evaluation Questions:**
 111 - Is the code structured for effective static analysis?
 112 - Are error handling patterns consistent and analyzable?
 113 - Does the code follow analysis-friendly practices?
 114 - Is the modularity appropriate for analysis goals?
 115 - Are coding standards consistently applied?
 116
 117 ## Frama-C Analysis-Specific Criticism Process
 118
 119 ### Step 1: Static Analysis Soundness Assessment
 120 1. **Check Analysis Coverage**: Are all relevant code paths and states analyzed?
 121 2. **Evaluate Soundness**: Does the analysis guarantee no false negatives for safety properties?
 122 3. **Assess Precision**: Are false positives minimized while maintaining soundness?
 123 4. **Review Undefined Behavior Handling**: Are all undefined behaviors properly detected?
 124
 125 ### Step 2: Annotation Quality Analysis
 126 1. **Audit Function Contracts**: Are all functions properly annotated with contracts?
 127 2. **Check Precondition Accuracy**: Do preconditions match implementation requirements?
 128 3. **Evaluate Postcondition Strength**: Are postconditions adequate for verification goals?
 129 4. **Assess Loop Invariant Completeness**: Are all loops properly annotated?
 130
 131 ### Step 3: Formal Verification Assessment
 132 1. **Check Proof Success**: Are critical properties successfully verified?
 133 2. **Evaluate Proof Strategies**: Are appropriate strategies used for verification goals?
 134 3. **Assess Lemma Development**: Are sufficient lemmas developed for complex properties?
 135 4. **Review Tool Integration**: Are multiple analysis techniques properly integrated?
 136
 137 ## Frama-C Analysis-Specific Criticism Guidelines
 138
 139 ### Focus on Static Analysis Correctness
 140 **Good Criticism:**
 141 - "This analysis is unsound because it doesn't track the null pointer dereference in the error path."
 142 - "The abstract interpretation fails to prove array bounds safety due to imprecise interval analysis."
 143 - "The analysis misses the undefined behavior in this signed integer overflow."
 144 - "The pointer analysis is too imprecise, causing false positives in this alias analysis."
 145
 146 **Poor Criticism:**
 147 - "This analysis seems incomplete."
 148 - "I don't like how this handles pointers."
 149 - "This might miss some bugs."
 150
 151 ### Emphasize Formal Verification Soundness
 152 **Good Criticism:**
 153 - "The loop invariant is too weak to prove array bounds safety."
 154 - "The function contract doesn't specify the error conditions properly."
 155 - "The proof strategy needs additional lemmas for this complex data structure."
 156 - "The verification fails because the precondition doesn't account for all input states."
 157
 158 **Poor Criticism:**
 159 - "This verification is incomplete."
 160 - "This could be better proven."
 161 - "This is not robust."
 162
 163 ### Consider Tool Integration and Workflow
 164 **Good Criticism:**
 165 - "The EVA plugin configuration is too conservative for this analysis goal."
 166 - "The WP plugin needs additional axioms for this mathematical property."
 167 - "The analysis workflow doesn't integrate with the continuous integration pipeline."
 168 - "The result reporting doesn't distinguish between different severity levels."
 169
 170 **Poor Criticism:**
 171 - "This tool configuration is poor."
 172 - "This might not work in practice."
 173 - "This is not well integrated."
 174
 175 ## Frama-C Analysis-Specific Problem Categories
 176
 177 ### Static Analysis Problems
 178 - **Unsound Analysis**: Analysis that misses real bugs or violations
 179 - **Imprecise Analysis**: Analysis producing too many false positives
 180 - **Incomplete Coverage**: Missing analysis of relevant execution paths
 181 - **Poor Modeling**: Incorrect modeling of C language semantics
 182
 183 ### Annotation Problems
 184 - **Missing Contracts**: Functions without proper ACSL annotations
 185 - **Incorrect Preconditions**: Preconditions that don't match implementation
 186 - **Weak Postconditions**: Postconditions insufficient for verification goals
 187 - **Incomplete Loop Invariants**: Missing or incorrect loop annotations
 188
 189 ### Verification Problems
 190 - **Failed Proofs**: Unsuccessful verification of critical properties
 191 - **Poor Proof Strategies**: Inappropriate strategies for verification goals
 192 - **Missing Lemmas**: Insufficient lemma development for complex properties
 193 - **Tool Integration Issues**: Poor integration between analysis techniques
 194
 195 ### Workflow Problems
 196 - **Poor Tool Configuration**: Inappropriate analysis parameters
 197 - **Ineffective Integration**: Poor integration with development processes
 198 - **Inadequate Reporting**: Poor result communication and interpretation
 199 - **Scalability Issues**: Analysis that doesn't scale to realistic programs
 200
 201 ## Frama-C Analysis-Specific Criticism Templates
 202
 203 ### For Static Analysis Issues
 204 ```
 205 Static Analysis Issue: [Specific analysis problem]
 206 Analysis Tool: [Frama-C plugin or analysis technique]
 207 Problem: [How this affects analysis soundness or precision]
 208 Impact: [Missed bugs, false positives, or analysis failures]
 209 Evidence: [Specific code examples and analysis results]
 210 Priority: [Critical/High/Medium/Low]
 211 ```
 212
 213 ### For Annotation Issues
 214 ```
 215 Annotation Issue: [Specific annotation problem]
 216 Problem: [What makes this annotation incorrect or incomplete]
 217 Impact: [Verification failures, missed properties, or maintenance issues]
 218 Evidence: [Specific code examples and verification results]
 219 Priority: [Critical/High/Medium/Low]
 220 ```
 221
 222 ### For Verification Issues
 223 ```
 224 Verification Issue: [Specific verification problem]
 225 Problem: [What makes this verification approach inadequate]
 226 Impact: [Failed proofs, missed properties, or scalability issues]
 227 Evidence: [Specific proof attempts and verification results]
 228 Priority: [Critical/High/Medium/Low]
 229 ```
 230
 231 ### For Workflow Issues
 232 ```
 233 Workflow Issue: [Specific workflow problem]
 234 Problem: [What makes this workflow ineffective or inefficient]
 235 Impact: [Missed issues, poor integration, or scalability problems]
 236 Evidence: [Specific workflow examples and integration issues]
 237 Priority: [High/Medium/Low]
 238 ```
 239
 240 ## Frama-C Analysis-Specific Criticism Best Practices
 241
 242 ### Do's
 243 - **Cite Analysis Results**: Always reference specific analysis outputs and verification results
 244 - **Focus on Soundness**: Evaluate against formal verification and static analysis principles
 245 - **Consider Tool Capabilities**: Think about Frama-C plugin limitations and capabilities
 246 - **Emphasize Precision**: Balance soundness with precision in analysis results
 247 - **Document Analysis Strategy**: Clearly identify analysis approach and tool configuration
 248
 249 ### Don'ts
 250 - **Assume Perfect Analysis**: Don't assume static analysis catches all issues
 251 - **Ignore Tool Limitations**: Don't overlook Frama-C plugin limitations
 252 - **Accept Unsound Results**: Don't tolerate analysis that misses real bugs
 253 - **Skip Annotation Review**: Don't ignore annotation quality and completeness
 254 - **Overlook Workflow Integration**: Don't accept poor integration with development processes
 255
 256 ## Frama-C Analysis-Specific Criticism Checklist
 257
 258 ### Static Analysis Assessment
 259 - [ ] Is the analysis sound for the properties being checked?
 260 - [ ] Are false positives minimized while maintaining soundness?
 261 - [ ] Is undefined behavior properly detected and handled?
 262 - [ ] Are all relevant execution paths analyzed?
 263 - [ ] Does the analysis scale to realistic program sizes?
 264
 265 ### Annotation Assessment
 266 - [ ] Are all functions properly annotated with contracts?
 267 - [ ] Do preconditions accurately reflect function requirements?
 268 - [ ] Are postconditions strong enough for verification goals?
 269 - [ ] Are loop invariants complete and correct?
 270 - [ ] Are annotations consistent and maintainable?
 271
 272 ### Verification Assessment
 273 - [ ] Are critical safety properties formally verified?
 274 - [ ] Are proof strategies appropriate for verification goals?
 275 - [ ] Is the verification approach scalable and maintainable?
 276 - [ ] Are multiple analysis techniques properly integrated?
 277 - [ ] Are verification results properly documented and reviewed?
 278
 279 ### Workflow Assessment
 280 - [ ] Are the right Frama-C plugins selected for analysis goals?
 281 - [ ] Is the analysis workflow integrated with development?
 282 - [ ] Are analysis results effectively communicated?
 283 - [ ] Is the tool configuration appropriate for the codebase?
 284 - [ ] Are analysis results properly interpreted and acted upon?
 285
 286 ## Frama-C Analysis-Specific Evaluation Questions
 287
 288 ### For Any C Code Analysis
 289 1. **Is the static analysis sound for the safety properties being checked?**
 290 2. **Are all functions properly annotated with ACSL contracts?**
 291 3. **Are critical safety properties formally verified?**
 292 4. **Is the analysis workflow integrated with development processes?**
 293 5. **Are analysis results effectively communicated and acted upon?**
 294 6. **Is the tool configuration appropriate for the analysis goals?**
 295 7. **Are multiple analysis techniques properly integrated?**
 296 8. **Is the analysis approach scalable to realistic program sizes?**
 297 9. **Are undefined behaviors properly detected and handled?**
 298 10. **Is the code structured for effective static analysis?**
 299
 300 ### For Library or System Code Analysis
 301 1. **Are all public interfaces documented with formal contracts?**
 302 2. **Is thread safety properly specified and verified?**
 303 3. **Are all error conditions properly specified in contracts?**
 304 4. **Is the API design consistent with formal verification principles?**
 305 5. **Are all resources and exceptional states properly managed?**
 306
 307 ## Frama-C Analysis Principles Applied
 308
 309 ### "Provide Sound Static Analysis"
 310 - Ensure no false negatives for safety properties
 311 - Balance soundness with precision in analysis results
 312 - Use appropriate analysis techniques for verification goals
 313
 314 ### "Support Formal Verification"
 315 - Develop comprehensive ACSL annotations
 316 - Use appropriate proof strategies and lemma development
 317 - Integrate multiple analysis techniques effectively
 318
 319 ### "Enable Scalable Analysis"
 320 - Structure code for effective static analysis
 321 - Use appropriate tool configuration and workflow integration
 322 - Balance analysis precision with performance requirements
 323
 324 ### "Balance Automation and Precision"
 325 - Use automated analysis where possible
 326 - Provide manual guidance for complex verification goals
 327 - Integrate analysis with development workflow
 328
 329 ### "Document and Control Analysis Dependencies"
 330 - Clearly document analysis approach and tool configuration
 331 - Use appropriate abstraction levels for verification goals
 332 - Avoid over-reliance on single analysis technique
 333
 334 ## Frama-C Plugin and Analysis Tool Evaluation Criteria
 335
 336 ### Core Analysis Plugins
 337 - **EVA (Evolved Value Analysis)**: Sound abstract interpretation, precision, scalability
 338 - **WP (Weakest Precondition)**: Proof strategy effectiveness, lemma development, verification success
 339 - **Slicing**: Path coverage, dependency analysis, slicing criteria appropriateness
 340 - **From**: Call graph analysis, function pointer resolution, interprocedural analysis
 341
 342 ### Specialized Analysis Plugins
 343 - **Mthread**: Thread safety analysis, race condition detection, synchronization verification
 344 - **Splug**: Security analysis, vulnerability detection, attack vector identification
 345 - **RTE (Runtime Error Analysis)**: Undefined behavior detection, error condition analysis
 346 - **Aoraï**: Performance analysis, resource usage verification, timing analysis
 347
 348 ### Verification and Proof Tools
 349 - **Alt-Ergo**: SMT solver integration, proof automation, strategy effectiveness
 350 - **CVC4**: Alternative SMT solver, proof performance, strategy comparison
 351 - **Coq**: Interactive theorem proving, complex property verification, lemma development
 352 - **Z3**: Microsoft SMT solver, proof automation, strategy effectiveness
 353
 354 ### Workflow and Integration Tools
 355 - **Frama-C GUI**: Interactive analysis, result visualization, workflow integration
 356 - **Frama-C Batch Mode**: Automated analysis, CI/CD integration, result reporting
 357 - **Frama-C API**: Programmatic analysis, custom plugin development, tool integration
 358 - **Frama-C Report Generation**: Result communication, issue tracking, documentation