# Frama-C Analysis Framework Critic Framework

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.

## Frama-C Analysis Evaluation Areas

### 1. Static Analysis Soundness and Precision
**What to Look For:**
- Soundness of analysis results (no false negatives for safety properties)
- Precision of analysis (minimizing false positives)
- Correct handling of undefined behavior and implementation-defined behavior
- Proper modeling of memory layout, aliasing, and pointer arithmetic
- Adequate coverage of execution paths and program states

**Common Problems:**
- Unsound analysis that misses real bugs or violations
- Overly conservative analysis producing too many false positives
- Incorrect modeling of C language semantics
- Missing analysis of undefined behavior scenarios
- Incomplete path coverage or state space exploration

**Evaluation Questions:**
- Is the analysis sound for the properties being checked?
- Are false positives minimized while maintaining soundness?
- Is undefined behavior properly detected and handled?
- Are all relevant execution paths analyzed?
- Does the analysis scale to realistic program sizes?

### 2. Annotation Quality and Completeness
**What to Look For:**
- Comprehensive ACSL (ANSI/ISO C Specification Language) annotations
- Correct preconditions, postconditions, and loop invariants
- Proper use of ghost variables and logic functions
- Complete specification of function contracts and data invariants
- Appropriate abstraction levels for verification goals

**Common Problems:**
- Missing or incomplete function contracts
- Incorrect preconditions that don't match implementation
- Weak or overly strong postconditions
- Missing loop invariants causing verification failures
- Inconsistent annotations across related functions

**Evaluation Questions:**
- Are all functions properly annotated with contracts?
- Do preconditions accurately reflect function requirements?
- Are postconditions strong enough for verification goals?
- Are loop invariants complete and correct?
- Are annotations consistent and maintainable?

### 3. Formal Verification Correctness
**What to Look For:**
- Successful proof of safety and functional properties
- Correct use of verification tools (WP, EVA, etc.)
- Proper handling of complex data structures and algorithms
- Adequate proof strategies and lemma development
- Integration of multiple analysis techniques

**Common Problems:**
- Failed proof attempts without adequate strategies
- Over-reliance on single analysis technique
- Insufficient lemma development for complex properties
- Ignoring verification of critical safety properties
- Poor integration between different analysis tools

**Evaluation Questions:**
- Are critical safety properties formally verified?
- Are proof strategies appropriate for the verification goals?
- Is the verification approach scalable and maintainable?
- Are multiple analysis techniques properly integrated?
- Are verification results properly documented and reviewed?

### 4. Tool Integration and Workflow
**What to Look For:**
- Effective use of Frama-C plugins and analysis tools
- Proper configuration of analysis parameters
- Integration with development workflow and CI/CD
- Appropriate use of different analysis modes (batch, interactive)
- Effective reporting and result interpretation

**Common Problems:**
- Poor tool configuration leading to missed issues
- Ineffective integration with development processes
- Lack of automation in analysis workflow
- Poor result reporting and interpretation
- Inadequate tool selection for analysis goals

**Evaluation Questions:**
- Are the right Frama-C plugins selected for analysis goals?
- Is the analysis workflow integrated with development?
- Are analysis results effectively communicated?
- Is the tool configuration appropriate for the codebase?
- Are analysis results properly interpreted and acted upon?

### 5. Code Quality and Analysis Readiness
**What to Look For:**
- Code structured for effective static analysis
- Clear separation of concerns and modularity
- Proper error handling and resource management
- Consistent coding standards and practices
- Analysis-friendly code organization

**Common Problems:**
- Code structure that impedes effective analysis
- Complex control flow that confuses analysis tools
- Inconsistent error handling patterns
- Poor modularity limiting analysis scope
- Code that doesn't follow analysis-friendly practices

**Evaluation Questions:**
- Is the code structured for effective static analysis?
- Are error handling patterns consistent and analyzable?
- Does the code follow analysis-friendly practices?
- Is the modularity appropriate for analysis goals?
- Are coding standards consistently applied?

## Frama-C Analysis-Specific Criticism Process

### Step 1: Static Analysis Soundness Assessment
1. **Check Analysis Coverage**: Are all relevant code paths and states analyzed?
2. **Evaluate Soundness**: Does the analysis guarantee no false negatives for safety properties?
3. **Assess Precision**: Are false positives minimized while maintaining soundness?
4. **Review Undefined Behavior Handling**: Are all undefined behaviors properly detected?

### Step 2: Annotation Quality Analysis
1. **Audit Function Contracts**: Are all functions properly annotated with contracts?
2. **Check Precondition Accuracy**: Do preconditions match implementation requirements?
3. **Evaluate Postcondition Strength**: Are postconditions adequate for verification goals?
4. **Assess Loop Invariant Completeness**: Are all loops properly annotated?

### Step 3: Formal Verification Assessment
1. **Check Proof Success**: Are critical properties successfully verified?
2. **Evaluate Proof Strategies**: Are appropriate strategies used for verification goals?
3. **Assess Lemma Development**: Are sufficient lemmas developed for complex properties?
4. **Review Tool Integration**: Are multiple analysis techniques properly integrated?

## Frama-C Analysis-Specific Criticism Guidelines

### Focus on Static Analysis Correctness
**Good Criticism:**
- "This analysis is unsound because it doesn't track the null pointer dereference in the error path."
- "The abstract interpretation fails to prove array bounds safety due to imprecise interval analysis."
- "The analysis misses the undefined behavior in this signed integer overflow."
- "The pointer analysis is too imprecise, causing false positives in this alias analysis."

**Poor Criticism:**
- "This analysis seems incomplete."
- "I don't like how this handles pointers."
- "This might miss some bugs."

### Emphasize Formal Verification Soundness
**Good Criticism:**
- "The loop invariant is too weak to prove array bounds safety."
- "The function contract doesn't specify the error conditions properly."
- "The proof strategy needs additional lemmas for this complex data structure."
- "The verification fails because the precondition doesn't account for all input states."

**Poor Criticism:**
- "This verification is incomplete."
- "This could be better proven."
- "This is not robust."

### Consider Tool Integration and Workflow
**Good Criticism:**
- "The EVA plugin configuration is too conservative for this analysis goal."
- "The WP plugin needs additional axioms for this mathematical property."
- "The analysis workflow doesn't integrate with the continuous integration pipeline."
- "The result reporting doesn't distinguish between different severity levels."

**Poor Criticism:**
- "This tool configuration is poor."
- "This might not work in practice."
- "This is not well integrated."

## Frama-C Analysis-Specific Problem Categories

### Static Analysis Problems
- **Unsound Analysis**: Analysis that misses real bugs or violations
- **Imprecise Analysis**: Analysis producing too many false positives
- **Incomplete Coverage**: Missing analysis of relevant execution paths
- **Poor Modeling**: Incorrect modeling of C language semantics

### Annotation Problems
- **Missing Contracts**: Functions without proper ACSL annotations
- **Incorrect Preconditions**: Preconditions that don't match implementation
- **Weak Postconditions**: Postconditions insufficient for verification goals
- **Incomplete Loop Invariants**: Missing or incorrect loop annotations

### Verification Problems
- **Failed Proofs**: Unsuccessful verification of critical properties
- **Poor Proof Strategies**: Inappropriate strategies for verification goals
- **Missing Lemmas**: Insufficient lemma development for complex properties
- **Tool Integration Issues**: Poor integration between analysis techniques

### Workflow Problems
- **Poor Tool Configuration**: Inappropriate analysis parameters
- **Ineffective Integration**: Poor integration with development processes
- **Inadequate Reporting**: Poor result communication and interpretation
- **Scalability Issues**: Analysis that doesn't scale to realistic programs

## Frama-C Analysis-Specific Criticism Templates

### For Static Analysis Issues
```
Static Analysis Issue: [Specific analysis problem]
Analysis Tool: [Frama-C plugin or analysis technique]
Problem: [How this affects analysis soundness or precision]
Impact: [Missed bugs, false positives, or analysis failures]
Evidence: [Specific code examples and analysis results]
Priority: [Critical/High/Medium/Low]
```

### For Annotation Issues
```
Annotation Issue: [Specific annotation problem]
Problem: [What makes this annotation incorrect or incomplete]
Impact: [Verification failures, missed properties, or maintenance issues]
Evidence: [Specific code examples and verification results]
Priority: [Critical/High/Medium/Low]
```

### For Verification Issues
```
Verification Issue: [Specific verification problem]
Problem: [What makes this verification approach inadequate]
Impact: [Failed proofs, missed properties, or scalability issues]
Evidence: [Specific proof attempts and verification results]
Priority: [Critical/High/Medium/Low]
```

### For Workflow Issues
```
Workflow Issue: [Specific workflow problem]
Problem: [What makes this workflow ineffective or inefficient]
Impact: [Missed issues, poor integration, or scalability problems]
Evidence: [Specific workflow examples and integration issues]
Priority: [High/Medium/Low]
```

## Frama-C Analysis-Specific Criticism Best Practices

### Do's
- **Cite Analysis Results**: Always reference specific analysis outputs and verification results
- **Focus on Soundness**: Evaluate against formal verification and static analysis principles
- **Consider Tool Capabilities**: Think about Frama-C plugin limitations and capabilities
- **Emphasize Precision**: Balance soundness with precision in analysis results
- **Document Analysis Strategy**: Clearly identify analysis approach and tool configuration

### Don'ts
- **Assume Perfect Analysis**: Don't assume static analysis catches all issues
- **Ignore Tool Limitations**: Don't overlook Frama-C plugin limitations
- **Accept Unsound Results**: Don't tolerate analysis that misses real bugs
- **Skip Annotation Review**: Don't ignore annotation quality and completeness
- **Overlook Workflow Integration**: Don't accept poor integration with development processes

## Frama-C Analysis-Specific Criticism Checklist

### Static Analysis Assessment
- [ ] Is the analysis sound for the properties being checked?
- [ ] Are false positives minimized while maintaining soundness?
- [ ] Is undefined behavior properly detected and handled?
- [ ] Are all relevant execution paths analyzed?
- [ ] Does the analysis scale to realistic program sizes?

### Annotation Assessment
- [ ] Are all functions properly annotated with contracts?
- [ ] Do preconditions accurately reflect function requirements?
- [ ] Are postconditions strong enough for verification goals?
- [ ] Are loop invariants complete and correct?
- [ ] Are annotations consistent and maintainable?

### Verification Assessment
- [ ] Are critical safety properties formally verified?
- [ ] Are proof strategies appropriate for verification goals?
- [ ] Is the verification approach scalable and maintainable?
- [ ] Are multiple analysis techniques properly integrated?
- [ ] Are verification results properly documented and reviewed?

### Workflow Assessment
- [ ] Are the right Frama-C plugins selected for analysis goals?
- [ ] Is the analysis workflow integrated with development?
- [ ] Are analysis results effectively communicated?
- [ ] Is the tool configuration appropriate for the codebase?
- [ ] Are analysis results properly interpreted and acted upon?

## Frama-C Analysis-Specific Evaluation Questions

### For Any C Code Analysis
1. **Is the static analysis sound for the safety properties being checked?**
2. **Are all functions properly annotated with ACSL contracts?**
3. **Are critical safety properties formally verified?**
4. **Is the analysis workflow integrated with development processes?**
5. **Are analysis results effectively communicated and acted upon?**
6. **Is the tool configuration appropriate for the analysis goals?**
7. **Are multiple analysis techniques properly integrated?**
8. **Is the analysis approach scalable to realistic program sizes?**
9. **Are undefined behaviors properly detected and handled?**
10. **Is the code structured for effective static analysis?**

### For Library or System Code Analysis
1. **Are all public interfaces documented with formal contracts?**
2. **Is thread safety properly specified and verified?**
3. **Are all error conditions properly specified in contracts?**
4. **Is the API design consistent with formal verification principles?**
5. **Are all resources and exceptional states properly managed?**

## Frama-C Analysis Principles Applied

### "Provide Sound Static Analysis"
- Ensure no false negatives for safety properties
- Balance soundness with precision in analysis results
- Use appropriate analysis techniques for verification goals

### "Support Formal Verification"
- Develop comprehensive ACSL annotations
- Use appropriate proof strategies and lemma development
- Integrate multiple analysis techniques effectively

### "Enable Scalable Analysis"
- Structure code for effective static analysis
- Use appropriate tool configuration and workflow integration
- Balance analysis precision with performance requirements

### "Balance Automation and Precision"
- Use automated analysis where possible
- Provide manual guidance for complex verification goals
- Integrate analysis with development workflow

### "Document and Control Analysis Dependencies"
- Clearly document analysis approach and tool configuration
- Use appropriate abstraction levels for verification goals
- Avoid over-reliance on single analysis technique

## Frama-C Plugin and Analysis Tool Evaluation Criteria

### Core Analysis Plugins
- **EVA (Evolved Value Analysis)**: Sound abstract interpretation, precision, scalability
- **WP (Weakest Precondition)**: Proof strategy effectiveness, lemma development, verification success
- **Slicing**: Path coverage, dependency analysis, slicing criteria appropriateness
- **From**: Call graph analysis, function pointer resolution, interprocedural analysis

### Specialized Analysis Plugins
- **Mthread**: Thread safety analysis, race condition detection, synchronization verification
- **Splug**: Security analysis, vulnerability detection, attack vector identification
- **RTE (Runtime Error Analysis)**: Undefined behavior detection, error condition analysis
- **Aoraï**: Performance analysis, resource usage verification, timing analysis

### Verification and Proof Tools
- **Alt-Ergo**: SMT solver integration, proof automation, strategy effectiveness
- **CVC4**: Alternative SMT solver, proof performance, strategy comparison
- **Coq**: Interactive theorem proving, complex property verification, lemma development
- **Z3**: Microsoft SMT solver, proof automation, strategy effectiveness

### Workflow and Integration Tools
- **Frama-C GUI**: Interactive analysis, result visualization, workflow integration
- **Frama-C Batch Mode**: Automated analysis, CI/CD integration, result reporting
- **Frama-C API**: Programmatic analysis, custom plugin development, tool integration
- **Frama-C Report Generation**: Result communication, issue tracking, documentation