Legacy compilers

Workflow runs for Legacy compilers

• CBMC: Use constant quantifier ranges in some loop invariants

  skipped:
  Legacy compilers#1247:Pull request#1495synchronizebymkannwischer
  cbmc-bounded-invariants

  Oct 26, 20261s
  More actions for workflow run 1247

• CBMC: Use constant quantifier ranges in some loop invariants

  skipped:
  Legacy compilers#1246:Pull request#1495synchronizebymkannwischer
  cbmc-bounded-invariants

  Oct 26, 20261s
  More actions for workflow run 1246

• Various small fixes and improvements

  skipped:
  Legacy compilers#1245:Pull request#1468synchronizebyhanno-becker
  mjk/config-guards

  Oct 26, 20261s
  More actions for workflow run 1245

• HOL-Light: Minor clean-ups

  skipped:
  Legacy compilers#1244:Pull request#1502labeledbymkannwischer
  hol-speedup-followup

  Oct 26, 20261s
  More actions for workflow run 1244

• HOL-Light: Minor clean-ups

  skipped:
  Legacy compilers#1243:Pull request#1502openedbymkannwischer
  hol-speedup-followup

  Oct 26, 20262s
  More actions for workflow run 1243

• CBMC: Add CaDiCaL proofs using constant array-bound ranges

  skipped:
  Legacy compilers#1242:Pull request#1501openedbymkannwischer
  cbmc-native-and-sampling-second-solvers

  Oct 26, 20261s
  More actions for workflow run 1242

• CBMC: Add a second solver for 2 slow proofs

  skipped:
  Legacy compilers#1241:Pull request#1496synchronizebymkannwischer
  cbmc-slow-second-solvers

  Oct 26, 20261s
  More actions for workflow run 1241

• HOL-Light: Tweaks for better proof performance

  skipped:
  Legacy compilers#1240:Pull request#1499labeledbyhanno-becker
  hol-speedup

  Oct 26, 20261s
  More actions for workflow run 1240

• HOL-Light: Tweaks for better proof performance

  skipped:
  Legacy compilers#1239:Pull request#1499labeledbyhanno-becker
  hol-speedup

  Oct 26, 20261s
  More actions for workflow run 1239

• CBMC: Add cvc5 as a second solver for polyvecl_chknorm

  skipped:
  Legacy compilers#1238:Pull request#1500openedbymkannwischer
  cbmc-polyvecl-chknorm-cvc5

  Oct 26, 20268s
  More actions for workflow run 1238

• HOL-Light: Tweaks for better proof performance

  skipped:
  Legacy compilers#1237:Pull request#1499labeledbyhanno-becker
  hol-speedup

  Oct 26, 20261s
  More actions for workflow run 1237

• Zeroize stack in assembly routines spilling to the stack

  skipped:
  Legacy compilers#1236:Pull request#1498labeledbymkannwischer
  asm-zeroize

  Oct 26, 20266s
  More actions for workflow run 1236

• Legacy compilers

  completed successfully:
  Legacy compilers#1235:Scheduled
  main

  Oct 26, 202652m 46s
  More actions for workflow run 1235

• CBMC: Add a second solver for 8 more proofs

  skipped:
  Legacy compilers#1234:Pull request#1493synchronizebyhanno-becker
  cbmc-more-second-solvers

  Oct 25, 20269s
  More actions for workflow run 1234

• RV32-IM: Unroll proofs to allow for later SLOTHY-fication

  skipped:
  Legacy compilers#1233:Pull request#1475synchronizebyhanno-becker
  rv-unroll

  Oct 25, 20261s
  More actions for workflow run 1233

• HOL-Light: Tweaks for better proof performance

  skipped:
  Legacy compilers#1232:Pull request#1499synchronizebyhanno-becker
  hol-speedup

  Oct 25, 20261s
  More actions for workflow run 1232

• HOL-Light: Tweaks for better proof performance

  skipped:
  Legacy compilers#1231:Pull request#1499openedbyhanno-becker
  hol-speedup

  Oct 25, 20261s
  More actions for workflow run 1231

• RV32-IM: Unroll proofs to allow for later SLOTHY-fication

  skipped:
  Legacy compilers#1230:Pull request#1475synchronizebyhanno-becker
  rv-unroll

  Oct 25, 20261s
  More actions for workflow run 1230

• CBMC: Add CaDiCaL SAT profile

  skipped:
  Legacy compilers#1229:Pull request#1492synchronizebyhanno-becker
  cbmc-cadical-proofs

  Oct 25, 20261s
  More actions for workflow run 1229

• Zeroize stack in assembly routines spilling to the stack

  skipped:
  Legacy compilers#1228:Pull request#1498labeledbymkannwischer
  asm-zeroize

  Oct 25, 20267s
  More actions for workflow run 1228

• Zeroize stack in assembly routines spilling to the stack

  skipped:
  Legacy compilers#1227:Pull request#1498openedbymkannwischer
  asm-zeroize

  Oct 25, 20261s
  More actions for workflow run 1227

• HOL Light: Fail bytecode update if a proof's bytecode is not dumped

  skipped:
  Legacy compilers#1226:Pull request#1497labeledbymkannwischer
  bytecode-autogen

  Oct 25, 20267s
  More actions for workflow run 1226

• HOL Light: Fail bytecode update if a proof's bytecode is not dumped

  skipped:
  Legacy compilers#1225:Pull request#1497synchronizebymkannwischer
  bytecode-autogen

  Oct 25, 20261s
  More actions for workflow run 1225

• HOL Light: Fail bytecode update if a proof's bytecode is not dumped

  skipped:
  Legacy compilers#1224:Pull request#1497openedbymkannwischer
  bytecode-autogen

  Oct 25, 20268s
  More actions for workflow run 1224

• CBMC: Add a second solver for 2 slow proofs

  skipped:
  Legacy compilers#1223:Pull request#1496openedbymkannwischer
  cbmc-slow-second-solvers

  Oct 25, 20261s
  More actions for workflow run 1223