#!/usr/bin/env python3
"""
Demo code generator for CBMC SpecGen web interface
This creates a demonstration of CBMC assertion generation without API calls
"""

import os
import sys
import re
from datetime import datetime

def add_cbmc_assertions(code):
    """Add CBMC assertions to C code (demo version)"""

    # Simple patterns for common functions
    patterns = {
        r'int\s+(\w+)\s*\([^)]*\)\s*\{': [
            '    // Preconditions\n',
            '    // Function body\n'
        ],
        r'for\s*\([^)]+\)\s*\{': [
            '        // Loop invariant\n',
            '        // Bounds checking\n'
        ],
        r'if\s*\([^)]+\)\s*\{': [
            '        // Condition check\n'
        ],
        r'int\s+\w+\s*\[\s*(\w+)\s*\]': [
            '    // Array bounds checking\n'
        ],
        r'return\s+\w+;': [
            '    // Postcondition check\n'
        ]
    }

    # Add basic assertions
    result = code

    # Add includes
    if '#include <stdio.h>' in result:
        result = result.replace('#include <stdio.h>', '#include <stdio.h>\n// CBMC assertions\n#include <assert.h>\n')

    # Add some basic assertions for demo
    if 'main()' in result:
        result = result.replace('int main() {', 'int main() {\n    // Entry point assertion\n    assert(1 == 1); // Basic sanity check')

    if 'printf' in result:
        result = result.replace('printf(', '// Output operation\n    printf(')

    return result

def create_demo_verification_result():
    """Create a demo CBMC verification result"""
    return """CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing demo.c
Converting
Type-checking demo
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking

** Results:
demo.c function main
[main.assertion.1] line 8 main: basic sanity check: SUCCESS
[main.assertion.2] line 15 main: valid computation: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL
**** WARNING: Use --unwinding-assertions to obtain sound verification results"""

def generate_demo_result(input_code):
    """Generate a complete demo result"""

    # Generate assertions
    generated_code = add_cbmc_assertions(input_code)

    # Create verification result
    verification_result = create_demo_verification_result()

    # Count assertions (simple count)
    assertion_count = generated_code.count('assert') + generated_code.count('__CPROVER_')

    return {
        'generated_code': generated_code,
        'verification_result': {
            'success': True,
            'output': verification_result,
            'assertion_count': assertion_count,
            'failed_count': 0
        },
        'summary': {
            'total_assertions': assertion_count,
            'passed_assertions': assertion_count,
            'failed_assertions': 0,
            'verification_success': True
        }
    }

if __name__ == "__main__":
    # Test the demo generator
    test_code = '''#include <stdio.h>

int add(int a, int b) {
    return a + b;
}

int main() {
    int result = add(3, 4);
    printf("Result: %d\\n", result);
    return 0;
}'''

    result = generate_demo_result(test_code)
    print("Generated Code:")
    print(result['generated_code'])
    print("\nVerification Result:")
    print(result['verification_result']['output'])