TEXT   198
Removal of function pointers and virtual functions
Guest on 23rd December 2024 02:17:16 AM


  1. Removal of function pointers and virtual functions
  2. Partial Inlining
  3. Generic Property Instrumentation
  4. Starting Bounded Model Checking
  5. Unwinding loop t1.0 iteration 1 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  6. Unwinding loop t1.0 iteration 2 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  7. Unwinding loop t1.0 iteration 3 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  8. Unwinding loop t1.0 iteration 4 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  9. Unwinding loop t1.0 iteration 5 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  10. Unwinding loop t1.0 iteration 6 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  11. Unwinding loop t1.0 iteration 7 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  12. Unwinding loop t1.0 iteration 8 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
  13. Unwinding loop t2.0 iteration 1 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  14. Unwinding loop t2.0 iteration 2 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  15. Unwinding loop t2.0 iteration 3 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  16. Unwinding loop t2.0 iteration 4 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  17. Unwinding loop t2.0 iteration 5 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  18. Unwinding loop t2.0 iteration 6 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  19. Unwinding loop t2.0 iteration 7 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  20. Unwinding loop t2.0 iteration 8 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
  21. size of program expression: 6673 steps
  22. simple slicing removed 3 assignments
  23. Generated 1 VCC(s), 1 remaining after simplification
  24. Passing problem to propositional reduction
  25. converting SSA
  26. Running propositional reduction
  27. Post-processing
  28. Solving with MiniSAT 2.2.1 with simplifier
  29. 259564 variables, 1147015 clauses
  30. SAT checker: instance is UNSATISFIABLE
  31. Runtime decision procedure: 44.482s
  32.  
  33. ** Results:
  34. [main.assertion.1] assertion (signed int)__CS_error != 1: SUCCESS
  35.  
  36. ** 0 of 1 failed (1 iteration)
  37. VERIFICATION SUCCESSFUL
Raw Paste

Login or Register to edit or fork this paste. It's free.