Skip to content

regression

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History
 
 

regression

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
acceleration
acceleration
 
 
ansi-c
ansi-c
 
 
array-refinement-with-incr
array-refinement-with-incr
 
 
array-refinement
array-refinement
 
 
cbmc-concurrency
cbmc-concurrency
 
 
cbmc-cover
cbmc-cover
 
 
cbmc-cpp
cbmc-cpp
 
 
cbmc-incr-oneloop
cbmc-incr-oneloop
 
 
cbmc-incr
cbmc-incr
 
 
cbmc-library
cbmc-library
 
 
cbmc-primitives
cbmc-primitives
 
 
cbmc-sequentialization
cbmc-sequentialization
 
 
cbmc-with-incr
cbmc-with-incr
 
 
cbmc
cbmc
 
 
contracts
contracts
 
 
cpp-linter
cpp-linter
 
 
cpp
cpp
 
 
extract_type_header
extract_type_header
 
 
fault-localization
fault-localization
 
 
goto-analyzer-simplify
goto-analyzer-simplify
 
 
goto-analyzer-taint
goto-analyzer-taint
 
 
goto-analyzer
goto-analyzer
 
 
goto-cc-cbmc-shared-options
goto-cc-cbmc-shared-options
 
 
goto-cc-cbmc
goto-cc-cbmc
 
 
goto-cc-file-local
goto-cc-file-local
 
 
goto-cc-goto-analyzer
goto-cc-goto-analyzer
 
 
goto-cc-multi-file
goto-cc-multi-file
 
 
goto-cc-regression-gh-issue-5380
goto-cc-regression-gh-issue-5380
 
 
goto-cl
goto-cl
 
 
goto-diff
goto-diff
 
 
goto-gcc
goto-gcc
 
 
goto-harness-multi-file-project
goto-harness-multi-file-project
 
 
goto-harness
goto-harness
 
 
goto-instrument-typedef
goto-instrument-typedef
 
 
goto-instrument-wmm-core
goto-instrument-wmm-core
 
 
goto-instrument
goto-instrument
 
 
goto-interpreter
goto-interpreter
 
 
goto-ld
goto-ld
 
 
invariants
invariants
 
 
k-induction
k-induction
 
 
linking-goto-binaries
linking-goto-binaries
 
 
memory-analyzer
memory-analyzer
 
 
smt2_solver
smt2_solver
 
 
smt2_strings
smt2_strings
 
 
snapshot-harness
snapshot-harness
 
 
solver-hardness
solver-hardness
 
 
statement-list
statement-list
 
 
strings
strings
 
 
symtab2gb
symtab2gb
 
 
systemc
systemc
 
 
test-script
test-script
 
 
validate-trace-xml-schema
validate-trace-xml-schema
 
 
.gitignore
.gitignore
 
 
CMakeLists.txt
CMakeLists.txt
 
 
Makefile
Makefile
 
 
readme.md
readme.md
 
 
test.pl
test.pl
 
 

readme.md

CProver Regression Tests

This folder contains the CProver regression test-suite.

Tags

Backend

  • smt-backend: These tests require the SMT backend and do not work with the SAT backend. For example, quantified predicates are not fully supported in SAT.
  • broken-smt-backend: These tests are blocked on missing / buggy goto -> SMT translation rules, and therefore do not work with any SMT solver.
  • thorough-smt-backend: These tests are too slow to be run in CI with the SMT backend.

Solver

  • broken-cprover-smt-backend: These tests are known to not work with CPROVER SMT2.
  • thorough-cprover-smt-backend: These tests are too slow to be run in CI with CPROVER SMT2.
  • broken-z3-smt-backend: These tests are known to not work with Z3 (the version running on our CI).
  • thorough-z3-smt-backend: These tests are too slow to be run in CI with Z3.

Platform

  • winbug: These tests are currently known to be failing on Windows, but passing on other platforms. The reason for this is not known, and it's currently being investigated. This was discovered during work done to port CI from Travis and AWS CodeBuild to GitHub Actions. Worth noting that those tests were not being run on Windows before.