Skip to content

Commit 3b5a08c

Browse files
committed
cbmc-library/Float* cleanup: rename or move to cbmc/
In cbmc-library/, we organise regression tests by the name of the library function they are exercising. Rename these tests with the library function they exercise. For those not focussing on library functions, move them to cbmc/ instead. As those tests are also run past the cprover SMT solver, three tests newly demonstrated issues in the SMT back-end.
1 parent 94cdc0d commit 3b5a08c

File tree

32 files changed

+162
-300
lines changed

32 files changed

+162
-300
lines changed

regression/cbmc-library/Float-div1-refine/main.c

Lines changed: 0 additions & 53 deletions
This file was deleted.

regression/cbmc-library/Float-div1/main.c

Lines changed: 0 additions & 53 deletions
This file was deleted.

regression/cbmc-library/Float-flags-no-simp1/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

regression/cbmc-library/Float-flags-simp1/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

regression/cbmc-library/Float-no-simp8/main.c

Lines changed: 0 additions & 19 deletions
This file was deleted.

regression/cbmc-library/Float-to-double1/main.c

Lines changed: 0 additions & 19 deletions
This file was deleted.

regression/cbmc-library/Float21/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

regression/cbmc-library/Float_lib1/main.c

Lines changed: 0 additions & 55 deletions
This file was deleted.

regression/cbmc-library/Float_lib1/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

regression/cbmc-library/Float_lib2/main.c

Lines changed: 0 additions & 33 deletions
This file was deleted.

0 commit comments

Comments
 (0)