Operational Model Workload Estimate and Tracking

We need to adapt our C++ OMs for the new Clang-based C++ frontend. This page tracks the progress of OM fixes - number of issues/PRs for each OM.

Get LOCs for all OMs in descending order:

In src/cpp/library run the following commands:

find . -name "*" -type f -not -path "./Qt/*" -not -path "./boost/*" -exec wc -l {} \; > file.txt
awk '{print $NF,$0}' file.txt | sort -nr -k2 | cut -d' ' -f2- > output.txt
sed 's/ \+/,/g' output.txt > output.csv

Workload estimate and progress tracking:

• 27/03 - 29/04: Completed 15/64 OMs, enabled 150 ish TCs, 3-4 OMs completed per week
• [Completed] Blocker ticket https://github.com/esbmc/esbmc/issues/989: 2-3 weeks to support Templates and resolve this umbrella ticker
  • Original Estimate: upto 3w, Actually Logged: 2w4d (see timestamps of the comments in issue 989)
• 11/07: Completed 41/64 OMs, 23 remain to fix. The remaining OMs are categorized below based on the size:
  • Group 1 with LOC > 1000:
    • string, algorithm, map, list, set​
  • Group 2 with 100 < LOC < 1000:
    • deque, vector, cstdlib, locale, iterator, functional, valarray, tags, fstream, cstdlib, sstream, queue, memory, numeric
  • Group 3 with LOC < 100:
    • complex, stack, bitset, typeinfo
• 05/04/2024: Completed 58/64 OMs, 6 remain to fix. The remaining OMs are categorized below based on the size:
  • Group 1 with LOC > 1000:
    • string, algorithm, map, list, set​
  • Group 2 with 100 < LOC < 1000:
    • deque, vector, cstdlib, locale, iterator, functional, valarray, fstream, cstdlib, sstream, queue, memory, numeric
  • Group 3 with LOC < 100:
    • complex, stack, bitset, typeinfo
• 27/06/2024: Completed 63/64 OMs, 1 remain to fix. The remaining OMs are categorized below based on the size:
  • Group 1 with LOC > 1000:
    • string, algorithm, map, list, set​
  • Group 2 with 100 < LOC < 1000:
    • deque, vector, cstdlib, locale, iterator, functional, valarray, fstream, cstdlib, sstream, queue, memory, numeric
  • Group 3 with LOC < 100:
    • complex, stack, bitset, typeinfo

CUDA verification progress tracking:

CUDA OM issues:

• https://github.com/esbmc/esbmc/issues/1126
• https://github.com/esbmc/esbmc/issues/1176