diff --git a/regression/cbmc-library/CreateThread-01/main.c b/regression/cbmc-library/CreateThread/main.c similarity index 100% rename from regression/cbmc-library/CreateThread-01/main.c rename to regression/cbmc-library/CreateThread/main.c diff --git a/regression/cbmc-library/CreateThread-01/test.desc b/regression/cbmc-library/CreateThread/test.desc similarity index 100% rename from regression/cbmc-library/CreateThread-01/test.desc rename to regression/cbmc-library/CreateThread/test.desc diff --git a/regression/cbmc-library/ExitThread-01/main.c b/regression/cbmc-library/ExitThread/main.c similarity index 100% rename from regression/cbmc-library/ExitThread-01/main.c rename to regression/cbmc-library/ExitThread/main.c diff --git a/regression/cbmc-library/ExitThread-01/test.desc b/regression/cbmc-library/ExitThread/test.desc similarity index 100% rename from regression/cbmc-library/ExitThread-01/test.desc rename to regression/cbmc-library/ExitThread/test.desc diff --git a/regression/cbmc-library/QueryPerformanceFrequency-01/main.c b/regression/cbmc-library/QueryPerformanceFrequency/main.c similarity index 100% rename from regression/cbmc-library/QueryPerformanceFrequency-01/main.c rename to regression/cbmc-library/QueryPerformanceFrequency/main.c diff --git a/regression/cbmc-library/QueryPerformanceFrequency-01/test.desc b/regression/cbmc-library/QueryPerformanceFrequency/test.desc similarity index 100% rename from regression/cbmc-library/QueryPerformanceFrequency-01/test.desc rename to regression/cbmc-library/QueryPerformanceFrequency/test.desc diff --git a/regression/cbmc-library/_Exit-01/main.c b/regression/cbmc-library/_Exit/main.c similarity index 100% rename from regression/cbmc-library/_Exit-01/main.c rename to regression/cbmc-library/_Exit/main.c diff --git a/regression/cbmc-library/_Exit-01/test.desc b/regression/cbmc-library/_Exit/test.desc similarity index 100% rename from regression/cbmc-library/_Exit-01/test.desc rename to regression/cbmc-library/_Exit/test.desc diff --git a/regression/cbmc-library/_InterlockedAdd-01/main.c b/regression/cbmc-library/_InterlockedAdd/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedAdd-01/main.c rename to regression/cbmc-library/_InterlockedAdd/main.c diff --git a/regression/cbmc-library/_InterlockedAdd-01/test.desc b/regression/cbmc-library/_InterlockedAdd/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedAdd-01/test.desc rename to regression/cbmc-library/_InterlockedAdd/test.desc diff --git a/regression/cbmc-library/_InterlockedAddLargeStatistic-01/main.c b/regression/cbmc-library/_InterlockedAddLargeStatistic/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedAddLargeStatistic-01/main.c rename to regression/cbmc-library/_InterlockedAddLargeStatistic/main.c diff --git a/regression/cbmc-library/_InterlockedAddLargeStatistic-01/test.desc b/regression/cbmc-library/_InterlockedAddLargeStatistic/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedAddLargeStatistic-01/test.desc rename to regression/cbmc-library/_InterlockedAddLargeStatistic/test.desc diff --git a/regression/cbmc-library/_InterlockedAnd-01/main.c b/regression/cbmc-library/_InterlockedAnd/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedAnd-01/main.c rename to regression/cbmc-library/_InterlockedAnd/main.c diff --git a/regression/cbmc-library/_InterlockedAnd-01/test.desc b/regression/cbmc-library/_InterlockedAnd/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedAnd-01/test.desc rename to regression/cbmc-library/_InterlockedAnd/test.desc diff --git a/regression/cbmc-library/_InterlockedAnd16-01/main.c b/regression/cbmc-library/_InterlockedAnd16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedAnd16-01/main.c rename to regression/cbmc-library/_InterlockedAnd16/main.c diff --git a/regression/cbmc-library/_InterlockedAnd16-01/test.desc b/regression/cbmc-library/_InterlockedAnd16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedAnd16-01/test.desc rename to regression/cbmc-library/_InterlockedAnd16/test.desc diff --git a/regression/cbmc-library/_InterlockedAnd8-01/main.c b/regression/cbmc-library/_InterlockedAnd8/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedAnd8-01/main.c rename to regression/cbmc-library/_InterlockedAnd8/main.c diff --git a/regression/cbmc-library/_InterlockedAnd8-01/test.desc b/regression/cbmc-library/_InterlockedAnd8/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedAnd8-01/test.desc rename to regression/cbmc-library/_InterlockedAnd8/test.desc diff --git a/regression/cbmc-library/_InterlockedCompareExchange-01/main.c b/regression/cbmc-library/_InterlockedCompareExchange/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange-01/main.c rename to regression/cbmc-library/_InterlockedCompareExchange/main.c diff --git a/regression/cbmc-library/_InterlockedCompareExchange-01/test.desc b/regression/cbmc-library/_InterlockedCompareExchange/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange-01/test.desc rename to regression/cbmc-library/_InterlockedCompareExchange/test.desc diff --git a/regression/cbmc-library/_InterlockedCompareExchange16-01/main.c b/regression/cbmc-library/_InterlockedCompareExchange16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange16-01/main.c rename to regression/cbmc-library/_InterlockedCompareExchange16/main.c diff --git a/regression/cbmc-library/_InterlockedCompareExchange16-01/test.desc b/regression/cbmc-library/_InterlockedCompareExchange16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange16-01/test.desc rename to regression/cbmc-library/_InterlockedCompareExchange16/test.desc diff --git a/regression/cbmc-library/_InterlockedCompareExchange64-01/main.c b/regression/cbmc-library/_InterlockedCompareExchange64/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange64-01/main.c rename to regression/cbmc-library/_InterlockedCompareExchange64/main.c diff --git a/regression/cbmc-library/_InterlockedCompareExchange64-01/test.desc b/regression/cbmc-library/_InterlockedCompareExchange64/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange64-01/test.desc rename to regression/cbmc-library/_InterlockedCompareExchange64/test.desc diff --git a/regression/cbmc-library/_InterlockedCompareExchange8-01/main.c b/regression/cbmc-library/_InterlockedCompareExchange8/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange8-01/main.c rename to regression/cbmc-library/_InterlockedCompareExchange8/main.c diff --git a/regression/cbmc-library/_InterlockedCompareExchange8-01/test.desc b/regression/cbmc-library/_InterlockedCompareExchange8/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedCompareExchange8-01/test.desc rename to regression/cbmc-library/_InterlockedCompareExchange8/test.desc diff --git a/regression/cbmc-library/_InterlockedDecrement-01/main.c b/regression/cbmc-library/_InterlockedDecrement/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedDecrement-01/main.c rename to regression/cbmc-library/_InterlockedDecrement/main.c diff --git a/regression/cbmc-library/_InterlockedDecrement-01/test.desc b/regression/cbmc-library/_InterlockedDecrement/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedDecrement-01/test.desc rename to regression/cbmc-library/_InterlockedDecrement/test.desc diff --git a/regression/cbmc-library/_InterlockedDecrement16-01/main.c b/regression/cbmc-library/_InterlockedDecrement16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedDecrement16-01/main.c rename to regression/cbmc-library/_InterlockedDecrement16/main.c diff --git a/regression/cbmc-library/_InterlockedDecrement16-01/test.desc b/regression/cbmc-library/_InterlockedDecrement16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedDecrement16-01/test.desc rename to regression/cbmc-library/_InterlockedDecrement16/test.desc diff --git a/regression/cbmc-library/_InterlockedExchange-01/main.c b/regression/cbmc-library/_InterlockedExchange/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedExchange-01/main.c rename to regression/cbmc-library/_InterlockedExchange/main.c diff --git a/regression/cbmc-library/_InterlockedExchange-01/test.desc b/regression/cbmc-library/_InterlockedExchange/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedExchange-01/test.desc rename to regression/cbmc-library/_InterlockedExchange/test.desc diff --git a/regression/cbmc-library/_InterlockedExchange16-01/main.c b/regression/cbmc-library/_InterlockedExchange16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedExchange16-01/main.c rename to regression/cbmc-library/_InterlockedExchange16/main.c diff --git a/regression/cbmc-library/_InterlockedExchange16-01/test.desc b/regression/cbmc-library/_InterlockedExchange16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedExchange16-01/test.desc rename to regression/cbmc-library/_InterlockedExchange16/test.desc diff --git a/regression/cbmc-library/_InterlockedExchange8-01/main.c b/regression/cbmc-library/_InterlockedExchange8/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedExchange8-01/main.c rename to regression/cbmc-library/_InterlockedExchange8/main.c diff --git a/regression/cbmc-library/_InterlockedExchange8-01/test.desc b/regression/cbmc-library/_InterlockedExchange8/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedExchange8-01/test.desc rename to regression/cbmc-library/_InterlockedExchange8/test.desc diff --git a/regression/cbmc-library/_InterlockedExchangeAdd-01/main.c b/regression/cbmc-library/_InterlockedExchangeAdd/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedExchangeAdd-01/main.c rename to regression/cbmc-library/_InterlockedExchangeAdd/main.c diff --git a/regression/cbmc-library/_InterlockedExchangeAdd-01/test.desc b/regression/cbmc-library/_InterlockedExchangeAdd/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedExchangeAdd-01/test.desc rename to regression/cbmc-library/_InterlockedExchangeAdd/test.desc diff --git a/regression/cbmc-library/_InterlockedExchangeAdd16-01/main.c b/regression/cbmc-library/_InterlockedExchangeAdd16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedExchangeAdd16-01/main.c rename to regression/cbmc-library/_InterlockedExchangeAdd16/main.c diff --git a/regression/cbmc-library/_InterlockedExchangeAdd16-01/test.desc b/regression/cbmc-library/_InterlockedExchangeAdd16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedExchangeAdd16-01/test.desc rename to regression/cbmc-library/_InterlockedExchangeAdd16/test.desc diff --git a/regression/cbmc-library/_InterlockedExchangeAdd8-01/main.c b/regression/cbmc-library/_InterlockedExchangeAdd8/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedExchangeAdd8-01/main.c rename to regression/cbmc-library/_InterlockedExchangeAdd8/main.c diff --git a/regression/cbmc-library/_InterlockedExchangeAdd8-01/test.desc b/regression/cbmc-library/_InterlockedExchangeAdd8/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedExchangeAdd8-01/test.desc rename to regression/cbmc-library/_InterlockedExchangeAdd8/test.desc diff --git a/regression/cbmc-library/_InterlockedIncrement16-01/main.c b/regression/cbmc-library/_InterlockedIncrement16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedIncrement16-01/main.c rename to regression/cbmc-library/_InterlockedIncrement16/main.c diff --git a/regression/cbmc-library/_InterlockedIncrement16-01/test.desc b/regression/cbmc-library/_InterlockedIncrement16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedIncrement16-01/test.desc rename to regression/cbmc-library/_InterlockedIncrement16/test.desc diff --git a/regression/cbmc-library/_InterlockedOr-01/main.c b/regression/cbmc-library/_InterlockedOr/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedOr-01/main.c rename to regression/cbmc-library/_InterlockedOr/main.c diff --git a/regression/cbmc-library/_InterlockedOr-01/test.desc b/regression/cbmc-library/_InterlockedOr/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedOr-01/test.desc rename to regression/cbmc-library/_InterlockedOr/test.desc diff --git a/regression/cbmc-library/_InterlockedOr16-01/main.c b/regression/cbmc-library/_InterlockedOr16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedOr16-01/main.c rename to regression/cbmc-library/_InterlockedOr16/main.c diff --git a/regression/cbmc-library/_InterlockedOr16-01/test.desc b/regression/cbmc-library/_InterlockedOr16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedOr16-01/test.desc rename to regression/cbmc-library/_InterlockedOr16/test.desc diff --git a/regression/cbmc-library/_InterlockedOr8-01/main.c b/regression/cbmc-library/_InterlockedOr8/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedOr8-01/main.c rename to regression/cbmc-library/_InterlockedOr8/main.c diff --git a/regression/cbmc-library/_InterlockedOr8-01/test.desc b/regression/cbmc-library/_InterlockedOr8/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedOr8-01/test.desc rename to regression/cbmc-library/_InterlockedOr8/test.desc diff --git a/regression/cbmc-library/_InterlockedXor-01/main.c b/regression/cbmc-library/_InterlockedXor/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedXor-01/main.c rename to regression/cbmc-library/_InterlockedXor/main.c diff --git a/regression/cbmc-library/_InterlockedXor-01/test.desc b/regression/cbmc-library/_InterlockedXor/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedXor-01/test.desc rename to regression/cbmc-library/_InterlockedXor/test.desc diff --git a/regression/cbmc-library/_InterlockedXor16-01/main.c b/regression/cbmc-library/_InterlockedXor16/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedXor16-01/main.c rename to regression/cbmc-library/_InterlockedXor16/main.c diff --git a/regression/cbmc-library/_InterlockedXor16-01/test.desc b/regression/cbmc-library/_InterlockedXor16/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedXor16-01/test.desc rename to regression/cbmc-library/_InterlockedXor16/test.desc diff --git a/regression/cbmc-library/_InterlockedXor8-01/main.c b/regression/cbmc-library/_InterlockedXor8/main.c similarity index 100% rename from regression/cbmc-library/_InterlockedXor8-01/main.c rename to regression/cbmc-library/_InterlockedXor8/main.c diff --git a/regression/cbmc-library/_InterlockedXor8-01/test.desc b/regression/cbmc-library/_InterlockedXor8/test.desc similarity index 100% rename from regression/cbmc-library/_InterlockedXor8-01/test.desc rename to regression/cbmc-library/_InterlockedXor8/test.desc diff --git a/regression/cbmc-library/_ReadBarrier-01/main.c b/regression/cbmc-library/_ReadBarrier/main.c similarity index 100% rename from regression/cbmc-library/_ReadBarrier-01/main.c rename to regression/cbmc-library/_ReadBarrier/main.c diff --git a/regression/cbmc-library/_ReadBarrier-01/test.desc b/regression/cbmc-library/_ReadBarrier/test.desc similarity index 100% rename from regression/cbmc-library/_ReadBarrier-01/test.desc rename to regression/cbmc-library/_ReadBarrier/test.desc diff --git a/regression/cbmc-library/_ReadWriteBarrier-01/main.c b/regression/cbmc-library/_ReadWriteBarrier/main.c similarity index 100% rename from regression/cbmc-library/_ReadWriteBarrier-01/main.c rename to regression/cbmc-library/_ReadWriteBarrier/main.c diff --git a/regression/cbmc-library/_ReadWriteBarrier-01/test.desc b/regression/cbmc-library/_ReadWriteBarrier/test.desc similarity index 100% rename from regression/cbmc-library/_ReadWriteBarrier-01/test.desc rename to regression/cbmc-library/_ReadWriteBarrier/test.desc diff --git a/regression/cbmc-library/_WriteBarrier-01/main.c b/regression/cbmc-library/_WriteBarrier/main.c similarity index 100% rename from regression/cbmc-library/_WriteBarrier-01/main.c rename to regression/cbmc-library/_WriteBarrier/main.c diff --git a/regression/cbmc-library/_WriteBarrier-01/test.desc b/regression/cbmc-library/_WriteBarrier/test.desc similarity index 100% rename from regression/cbmc-library/_WriteBarrier-01/test.desc rename to regression/cbmc-library/_WriteBarrier/test.desc diff --git a/regression/cbmc-library/__CPROVER_danger_execute-01/main.c b/regression/cbmc-library/__CPROVER_danger_execute/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_danger_execute-01/main.c rename to regression/cbmc-library/__CPROVER_danger_execute/main.c diff --git a/regression/cbmc-library/__CPROVER_danger_execute-01/test.desc b/regression/cbmc-library/__CPROVER_danger_execute/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_danger_execute-01/test.desc rename to regression/cbmc-library/__CPROVER_danger_execute/test.desc diff --git a/regression/cbmc-library/__CPROVER_isgreaterd-01/main.c b/regression/cbmc-library/__CPROVER_isgreaterd/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterd-01/main.c rename to regression/cbmc-library/__CPROVER_isgreaterd/main.c diff --git a/regression/cbmc-library/__CPROVER_isgreaterd-01/test.desc b/regression/cbmc-library/__CPROVER_isgreaterd/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterd-01/test.desc rename to regression/cbmc-library/__CPROVER_isgreaterd/test.desc diff --git a/regression/cbmc-library/__CPROVER_isgreaterequald-01/main.c b/regression/cbmc-library/__CPROVER_isgreaterequald/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterequald-01/main.c rename to regression/cbmc-library/__CPROVER_isgreaterequald/main.c diff --git a/regression/cbmc-library/__CPROVER_isgreaterequald-01/test.desc b/regression/cbmc-library/__CPROVER_isgreaterequald/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterequald-01/test.desc rename to regression/cbmc-library/__CPROVER_isgreaterequald/test.desc diff --git a/regression/cbmc-library/__CPROVER_isgreaterequalf-01/main.c b/regression/cbmc-library/__CPROVER_isgreaterequalf/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterequalf-01/main.c rename to regression/cbmc-library/__CPROVER_isgreaterequalf/main.c diff --git a/regression/cbmc-library/__CPROVER_isgreaterequalf-01/test.desc b/regression/cbmc-library/__CPROVER_isgreaterequalf/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterequalf-01/test.desc rename to regression/cbmc-library/__CPROVER_isgreaterequalf/test.desc diff --git a/regression/cbmc-library/__CPROVER_isgreaterf-01/main.c b/regression/cbmc-library/__CPROVER_isgreaterf/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterf-01/main.c rename to regression/cbmc-library/__CPROVER_isgreaterf/main.c diff --git a/regression/cbmc-library/__CPROVER_isgreaterf-01/test.desc b/regression/cbmc-library/__CPROVER_isgreaterf/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_isgreaterf-01/test.desc rename to regression/cbmc-library/__CPROVER_isgreaterf/test.desc diff --git a/regression/cbmc-library/__CPROVER_islessd-01/main.c b/regression/cbmc-library/__CPROVER_islessd/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_islessd-01/main.c rename to regression/cbmc-library/__CPROVER_islessd/main.c diff --git a/regression/cbmc-library/__CPROVER_islessd-01/test.desc b/regression/cbmc-library/__CPROVER_islessd/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_islessd-01/test.desc rename to regression/cbmc-library/__CPROVER_islessd/test.desc diff --git a/regression/cbmc-library/__CPROVER_islessequald-01/main.c b/regression/cbmc-library/__CPROVER_islessequald/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_islessequald-01/main.c rename to regression/cbmc-library/__CPROVER_islessequald/main.c diff --git a/regression/cbmc-library/__CPROVER_islessequald-01/test.desc b/regression/cbmc-library/__CPROVER_islessequald/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_islessequald-01/test.desc rename to regression/cbmc-library/__CPROVER_islessequald/test.desc diff --git a/regression/cbmc-library/__CPROVER_islessequalf-01/main.c b/regression/cbmc-library/__CPROVER_islessequalf/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_islessequalf-01/main.c rename to regression/cbmc-library/__CPROVER_islessequalf/main.c diff --git a/regression/cbmc-library/__CPROVER_islessequalf-01/test.desc b/regression/cbmc-library/__CPROVER_islessequalf/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_islessequalf-01/test.desc rename to regression/cbmc-library/__CPROVER_islessequalf/test.desc diff --git a/regression/cbmc-library/__CPROVER_islessf-01/main.c b/regression/cbmc-library/__CPROVER_islessf/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_islessf-01/main.c rename to regression/cbmc-library/__CPROVER_islessf/main.c diff --git a/regression/cbmc-library/__CPROVER_islessf-01/test.desc b/regression/cbmc-library/__CPROVER_islessf/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_islessf-01/test.desc rename to regression/cbmc-library/__CPROVER_islessf/test.desc diff --git a/regression/cbmc-library/__CPROVER_islessgreaterd-01/main.c b/regression/cbmc-library/__CPROVER_islessgreaterd/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_islessgreaterd-01/main.c rename to regression/cbmc-library/__CPROVER_islessgreaterd/main.c diff --git a/regression/cbmc-library/__CPROVER_islessgreaterd-01/test.desc b/regression/cbmc-library/__CPROVER_islessgreaterd/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_islessgreaterd-01/test.desc rename to regression/cbmc-library/__CPROVER_islessgreaterd/test.desc diff --git a/regression/cbmc-library/__CPROVER_islessgreaterf-01/main.c b/regression/cbmc-library/__CPROVER_islessgreaterf/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_islessgreaterf-01/main.c rename to regression/cbmc-library/__CPROVER_islessgreaterf/main.c diff --git a/regression/cbmc-library/__CPROVER_islessgreaterf-01/test.desc b/regression/cbmc-library/__CPROVER_islessgreaterf/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_islessgreaterf-01/test.desc rename to regression/cbmc-library/__CPROVER_islessgreaterf/test.desc diff --git a/regression/cbmc-library/__CPROVER_isunorderedd-01/main.c b/regression/cbmc-library/__CPROVER_isunorderedd/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_isunorderedd-01/main.c rename to regression/cbmc-library/__CPROVER_isunorderedd/main.c diff --git a/regression/cbmc-library/__CPROVER_isunorderedd-01/test.desc b/regression/cbmc-library/__CPROVER_isunorderedd/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_isunorderedd-01/test.desc rename to regression/cbmc-library/__CPROVER_isunorderedd/test.desc diff --git a/regression/cbmc-library/__CPROVER_isunorderedf-01/main.c b/regression/cbmc-library/__CPROVER_isunorderedf/main.c similarity index 100% rename from regression/cbmc-library/__CPROVER_isunorderedf-01/main.c rename to regression/cbmc-library/__CPROVER_isunorderedf/main.c diff --git a/regression/cbmc-library/__CPROVER_isunorderedf-01/test.desc b/regression/cbmc-library/__CPROVER_isunorderedf/test.desc similarity index 100% rename from regression/cbmc-library/__CPROVER_isunorderedf-01/test.desc rename to regression/cbmc-library/__CPROVER_isunorderedf/test.desc diff --git a/regression/cbmc-library/__InterlockedIncrement-01/main.c b/regression/cbmc-library/__InterlockedIncrement/main.c similarity index 100% rename from regression/cbmc-library/__InterlockedIncrement-01/main.c rename to regression/cbmc-library/__InterlockedIncrement/main.c diff --git a/regression/cbmc-library/__InterlockedIncrement-01/test.desc b/regression/cbmc-library/__InterlockedIncrement/test.desc similarity index 100% rename from regression/cbmc-library/__InterlockedIncrement-01/test.desc rename to regression/cbmc-library/__InterlockedIncrement/test.desc diff --git a/regression/cbmc-library/___errno-01/main.c b/regression/cbmc-library/___errno/main.c similarity index 100% rename from regression/cbmc-library/___errno-01/main.c rename to regression/cbmc-library/___errno/main.c diff --git a/regression/cbmc-library/___errno-01/test.desc b/regression/cbmc-library/___errno/test.desc similarity index 100% rename from regression/cbmc-library/___errno-01/test.desc rename to regression/cbmc-library/___errno/test.desc diff --git a/regression/cbmc-library/__acrt_iob_func-01/main.c b/regression/cbmc-library/__acrt_iob_func/main.c similarity index 100% rename from regression/cbmc-library/__acrt_iob_func-01/main.c rename to regression/cbmc-library/__acrt_iob_func/main.c diff --git a/regression/cbmc-library/__acrt_iob_func-01/test.desc b/regression/cbmc-library/__acrt_iob_func/test.desc similarity index 100% rename from regression/cbmc-library/__acrt_iob_func-01/test.desc rename to regression/cbmc-library/__acrt_iob_func/test.desc diff --git a/regression/cbmc-library/__asm_fldcw-01/main.c b/regression/cbmc-library/__asm_fldcw/main.c similarity index 100% rename from regression/cbmc-library/__asm_fldcw-01/main.c rename to regression/cbmc-library/__asm_fldcw/main.c diff --git a/regression/cbmc-library/__asm_fldcw-01/test.desc b/regression/cbmc-library/__asm_fldcw/test.desc similarity index 100% rename from regression/cbmc-library/__asm_fldcw-01/test.desc rename to regression/cbmc-library/__asm_fldcw/test.desc diff --git a/regression/cbmc-library/__asm_fnstcw-01/main.c b/regression/cbmc-library/__asm_fnstcw/main.c similarity index 100% rename from regression/cbmc-library/__asm_fnstcw-01/main.c rename to regression/cbmc-library/__asm_fnstcw/main.c diff --git a/regression/cbmc-library/__asm_fnstcw-01/test.desc b/regression/cbmc-library/__asm_fnstcw/test.desc similarity index 100% rename from regression/cbmc-library/__asm_fnstcw-01/test.desc rename to regression/cbmc-library/__asm_fnstcw/test.desc diff --git a/regression/cbmc-library/__asm_fstcw-01/main.c b/regression/cbmc-library/__asm_fstcw/main.c similarity index 100% rename from regression/cbmc-library/__asm_fstcw-01/main.c rename to regression/cbmc-library/__asm_fstcw/main.c diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.desc b/regression/cbmc-library/__asm_fstcw/msvc.desc similarity index 100% rename from regression/cbmc-library/__asm_fstcw-01/msvc.desc rename to regression/cbmc-library/__asm_fstcw/msvc.desc diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.i b/regression/cbmc-library/__asm_fstcw/msvc.i similarity index 100% rename from regression/cbmc-library/__asm_fstcw-01/msvc.i rename to regression/cbmc-library/__asm_fstcw/msvc.i diff --git a/regression/cbmc-library/__asm_fstcw-01/test.desc b/regression/cbmc-library/__asm_fstcw/test.desc similarity index 100% rename from regression/cbmc-library/__asm_fstcw-01/test.desc rename to regression/cbmc-library/__asm_fstcw/test.desc diff --git a/regression/cbmc-library/__asm_lfence-01/main.c b/regression/cbmc-library/__asm_lfence/main.c similarity index 100% rename from regression/cbmc-library/__asm_lfence-01/main.c rename to regression/cbmc-library/__asm_lfence/main.c diff --git a/regression/cbmc-library/__asm_lfence-01/test.desc b/regression/cbmc-library/__asm_lfence/test.desc similarity index 100% rename from regression/cbmc-library/__asm_lfence-01/test.desc rename to regression/cbmc-library/__asm_lfence/test.desc diff --git a/regression/cbmc-library/__asm_mfence-01/main.c b/regression/cbmc-library/__asm_mfence/main.c similarity index 100% rename from regression/cbmc-library/__asm_mfence-01/main.c rename to regression/cbmc-library/__asm_mfence/main.c diff --git a/regression/cbmc-library/__asm_mfence-01/test.desc b/regression/cbmc-library/__asm_mfence/test.desc similarity index 100% rename from regression/cbmc-library/__asm_mfence-01/test.desc rename to regression/cbmc-library/__asm_mfence/test.desc diff --git a/regression/cbmc-library/__asm_sfence-01/main.c b/regression/cbmc-library/__asm_sfence/main.c similarity index 100% rename from regression/cbmc-library/__asm_sfence-01/main.c rename to regression/cbmc-library/__asm_sfence/main.c diff --git a/regression/cbmc-library/__asm_sfence-01/test.desc b/regression/cbmc-library/__asm_sfence/test.desc similarity index 100% rename from regression/cbmc-library/__asm_sfence-01/test.desc rename to regression/cbmc-library/__asm_sfence/test.desc diff --git a/regression/cbmc-library/__atomic_always_lock_free-01/main.c b/regression/cbmc-library/__atomic_always_lock_free/main.c similarity index 100% rename from regression/cbmc-library/__atomic_always_lock_free-01/main.c rename to regression/cbmc-library/__atomic_always_lock_free/main.c diff --git a/regression/cbmc-library/__atomic_always_lock_free-01/test.desc b/regression/cbmc-library/__atomic_always_lock_free/test.desc similarity index 100% rename from regression/cbmc-library/__atomic_always_lock_free-01/test.desc rename to regression/cbmc-library/__atomic_always_lock_free/test.desc diff --git a/regression/cbmc-library/__atomic_clear-01/main.c b/regression/cbmc-library/__atomic_clear/main.c similarity index 100% rename from regression/cbmc-library/__atomic_clear-01/main.c rename to regression/cbmc-library/__atomic_clear/main.c diff --git a/regression/cbmc-library/__atomic_clear-01/test.desc b/regression/cbmc-library/__atomic_clear/test.desc similarity index 100% rename from regression/cbmc-library/__atomic_clear-01/test.desc rename to regression/cbmc-library/__atomic_clear/test.desc diff --git a/regression/cbmc-library/__atomic_is_lock_free-01/main.c b/regression/cbmc-library/__atomic_is_lock_free/main.c similarity index 100% rename from regression/cbmc-library/__atomic_is_lock_free-01/main.c rename to regression/cbmc-library/__atomic_is_lock_free/main.c diff --git a/regression/cbmc-library/__atomic_is_lock_free-01/test.desc b/regression/cbmc-library/__atomic_is_lock_free/test.desc similarity index 100% rename from regression/cbmc-library/__atomic_is_lock_free-01/test.desc rename to regression/cbmc-library/__atomic_is_lock_free/test.desc diff --git a/regression/cbmc-library/__atomic_signal_fence-01/main.c b/regression/cbmc-library/__atomic_signal_fence/main.c similarity index 100% rename from regression/cbmc-library/__atomic_signal_fence-01/main.c rename to regression/cbmc-library/__atomic_signal_fence/main.c diff --git a/regression/cbmc-library/__atomic_signal_fence-01/test.desc b/regression/cbmc-library/__atomic_signal_fence/test.desc similarity index 100% rename from regression/cbmc-library/__atomic_signal_fence-01/test.desc rename to regression/cbmc-library/__atomic_signal_fence/test.desc diff --git a/regression/cbmc-library/__atomic_test_and_set-01/main.c b/regression/cbmc-library/__atomic_test_and_set/main.c similarity index 100% rename from regression/cbmc-library/__atomic_test_and_set-01/main.c rename to regression/cbmc-library/__atomic_test_and_set/main.c diff --git a/regression/cbmc-library/__atomic_test_and_set-01/test.desc b/regression/cbmc-library/__atomic_test_and_set/test.desc similarity index 100% rename from regression/cbmc-library/__atomic_test_and_set-01/test.desc rename to regression/cbmc-library/__atomic_test_and_set/test.desc diff --git a/regression/cbmc-library/__atomic_thread_fence-01/main.c b/regression/cbmc-library/__atomic_thread_fence/main.c similarity index 100% rename from regression/cbmc-library/__atomic_thread_fence-01/main.c rename to regression/cbmc-library/__atomic_thread_fence/main.c diff --git a/regression/cbmc-library/__atomic_thread_fence-01/test.desc b/regression/cbmc-library/__atomic_thread_fence/test.desc similarity index 100% rename from regression/cbmc-library/__atomic_thread_fence-01/test.desc rename to regression/cbmc-library/__atomic_thread_fence/test.desc diff --git a/regression/cbmc-library/__builtin___memcpy_chk-01/main.c b/regression/cbmc-library/__builtin___memcpy_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___memcpy_chk-01/main.c rename to regression/cbmc-library/__builtin___memcpy_chk/main.c diff --git a/regression/cbmc-library/__builtin___memcpy_chk-01/test.desc b/regression/cbmc-library/__builtin___memcpy_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___memcpy_chk-01/test.desc rename to regression/cbmc-library/__builtin___memcpy_chk/test.desc diff --git a/regression/cbmc-library/__builtin___memmove_chk-01/main.c b/regression/cbmc-library/__builtin___memmove_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___memmove_chk-01/main.c rename to regression/cbmc-library/__builtin___memmove_chk/main.c diff --git a/regression/cbmc-library/__builtin___memmove_chk-01/test.desc b/regression/cbmc-library/__builtin___memmove_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___memmove_chk-01/test.desc rename to regression/cbmc-library/__builtin___memmove_chk/test.desc diff --git a/regression/cbmc-library/__builtin___memset_chk-01/main.c b/regression/cbmc-library/__builtin___memset_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___memset_chk-01/main.c rename to regression/cbmc-library/__builtin___memset_chk/main.c diff --git a/regression/cbmc-library/__builtin___memset_chk-01/test.desc b/regression/cbmc-library/__builtin___memset_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___memset_chk-01/test.desc rename to regression/cbmc-library/__builtin___memset_chk/test.desc diff --git a/regression/cbmc-library/__builtin___strcat_chk-01/main.c b/regression/cbmc-library/__builtin___strcat_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___strcat_chk-01/main.c rename to regression/cbmc-library/__builtin___strcat_chk/main.c diff --git a/regression/cbmc-library/__builtin___strcat_chk-01/test.desc b/regression/cbmc-library/__builtin___strcat_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___strcat_chk-01/test.desc rename to regression/cbmc-library/__builtin___strcat_chk/test.desc diff --git a/regression/cbmc-library/__builtin___strcpy_chk-01/main.c b/regression/cbmc-library/__builtin___strcpy_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___strcpy_chk-01/main.c rename to regression/cbmc-library/__builtin___strcpy_chk/main.c diff --git a/regression/cbmc-library/__builtin___strcpy_chk-01/test.desc b/regression/cbmc-library/__builtin___strcpy_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___strcpy_chk-01/test.desc rename to regression/cbmc-library/__builtin___strcpy_chk/test.desc diff --git a/regression/cbmc-library/__builtin___strncat_chk-01/main.c b/regression/cbmc-library/__builtin___strncat_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___strncat_chk-01/main.c rename to regression/cbmc-library/__builtin___strncat_chk/main.c diff --git a/regression/cbmc-library/__builtin___strncat_chk-01/test.desc b/regression/cbmc-library/__builtin___strncat_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___strncat_chk-01/test.desc rename to regression/cbmc-library/__builtin___strncat_chk/test.desc diff --git a/regression/cbmc-library/__builtin___strncpy_chk-01/main.c b/regression/cbmc-library/__builtin___strncpy_chk/main.c similarity index 100% rename from regression/cbmc-library/__builtin___strncpy_chk-01/main.c rename to regression/cbmc-library/__builtin___strncpy_chk/main.c diff --git a/regression/cbmc-library/__builtin___strncpy_chk-01/test.desc b/regression/cbmc-library/__builtin___strncpy_chk/test.desc similarity index 100% rename from regression/cbmc-library/__builtin___strncpy_chk-01/test.desc rename to regression/cbmc-library/__builtin___strncpy_chk/test.desc diff --git a/regression/cbmc-library/__builtin_abs-01/main.c b/regression/cbmc-library/__builtin_abs/main.c similarity index 100% rename from regression/cbmc-library/__builtin_abs-01/main.c rename to regression/cbmc-library/__builtin_abs/main.c diff --git a/regression/cbmc-library/__builtin_abs-01/test.desc b/regression/cbmc-library/__builtin_abs/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_abs-01/test.desc rename to regression/cbmc-library/__builtin_abs/test.desc diff --git a/regression/cbmc-library/__builtin_fabs-01/main.c b/regression/cbmc-library/__builtin_fabs/main.c similarity index 100% rename from regression/cbmc-library/__builtin_fabs-01/main.c rename to regression/cbmc-library/__builtin_fabs/main.c diff --git a/regression/cbmc-library/__builtin_fabs-01/test.desc b/regression/cbmc-library/__builtin_fabs/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_fabs-01/test.desc rename to regression/cbmc-library/__builtin_fabs/test.desc diff --git a/regression/cbmc-library/__builtin_fabsf-01/main.c b/regression/cbmc-library/__builtin_fabsf/main.c similarity index 100% rename from regression/cbmc-library/__builtin_fabsf-01/main.c rename to regression/cbmc-library/__builtin_fabsf/main.c diff --git a/regression/cbmc-library/__builtin_fabsf-01/test.desc b/regression/cbmc-library/__builtin_fabsf/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_fabsf-01/test.desc rename to regression/cbmc-library/__builtin_fabsf/test.desc diff --git a/regression/cbmc-library/__builtin_fabsl-01/main.c b/regression/cbmc-library/__builtin_fabsl/main.c similarity index 100% rename from regression/cbmc-library/__builtin_fabsl-01/main.c rename to regression/cbmc-library/__builtin_fabsl/main.c diff --git a/regression/cbmc-library/__builtin_fabsl-01/test.desc b/regression/cbmc-library/__builtin_fabsl/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_fabsl-01/test.desc rename to regression/cbmc-library/__builtin_fabsl/test.desc diff --git a/regression/cbmc-library/__builtin_flt_rounds-01/main.c b/regression/cbmc-library/__builtin_flt_rounds/main.c similarity index 100% rename from regression/cbmc-library/__builtin_flt_rounds-01/main.c rename to regression/cbmc-library/__builtin_flt_rounds/main.c diff --git a/regression/cbmc-library/__builtin_flt_rounds-01/test.desc b/regression/cbmc-library/__builtin_flt_rounds/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_flt_rounds-01/test.desc rename to regression/cbmc-library/__builtin_flt_rounds/test.desc diff --git a/regression/cbmc-library/__builtin_huge_val-01/main.c b/regression/cbmc-library/__builtin_huge_val/main.c similarity index 100% rename from regression/cbmc-library/__builtin_huge_val-01/main.c rename to regression/cbmc-library/__builtin_huge_val/main.c diff --git a/regression/cbmc-library/__builtin_huge_val-01/test.desc b/regression/cbmc-library/__builtin_huge_val/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_huge_val-01/test.desc rename to regression/cbmc-library/__builtin_huge_val/test.desc diff --git a/regression/cbmc-library/__builtin_huge_valf-01/main.c b/regression/cbmc-library/__builtin_huge_valf/main.c similarity index 100% rename from regression/cbmc-library/__builtin_huge_valf-01/main.c rename to regression/cbmc-library/__builtin_huge_valf/main.c diff --git a/regression/cbmc-library/__builtin_huge_valf-01/test.desc b/regression/cbmc-library/__builtin_huge_valf/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_huge_valf-01/test.desc rename to regression/cbmc-library/__builtin_huge_valf/test.desc diff --git a/regression/cbmc-library/__builtin_huge_vall-01/main.c b/regression/cbmc-library/__builtin_huge_vall/main.c similarity index 100% rename from regression/cbmc-library/__builtin_huge_vall-01/main.c rename to regression/cbmc-library/__builtin_huge_vall/main.c diff --git a/regression/cbmc-library/__builtin_huge_vall-01/test.desc b/regression/cbmc-library/__builtin_huge_vall/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_huge_vall-01/test.desc rename to regression/cbmc-library/__builtin_huge_vall/test.desc diff --git a/regression/cbmc-library/__builtin_ia32_lfence-01/main.c b/regression/cbmc-library/__builtin_ia32_lfence/main.c similarity index 100% rename from regression/cbmc-library/__builtin_ia32_lfence-01/main.c rename to regression/cbmc-library/__builtin_ia32_lfence/main.c diff --git a/regression/cbmc-library/__builtin_ia32_lfence-01/test.desc b/regression/cbmc-library/__builtin_ia32_lfence/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_ia32_lfence-01/test.desc rename to regression/cbmc-library/__builtin_ia32_lfence/test.desc diff --git a/regression/cbmc-library/__builtin_ia32_mfence-01/main.c b/regression/cbmc-library/__builtin_ia32_mfence/main.c similarity index 100% rename from regression/cbmc-library/__builtin_ia32_mfence-01/main.c rename to regression/cbmc-library/__builtin_ia32_mfence/main.c diff --git a/regression/cbmc-library/__builtin_ia32_mfence-01/test.desc b/regression/cbmc-library/__builtin_ia32_mfence/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_ia32_mfence-01/test.desc rename to regression/cbmc-library/__builtin_ia32_mfence/test.desc diff --git a/regression/cbmc-library/__builtin_ia32_sfence-01/main.c b/regression/cbmc-library/__builtin_ia32_sfence/main.c similarity index 100% rename from regression/cbmc-library/__builtin_ia32_sfence-01/main.c rename to regression/cbmc-library/__builtin_ia32_sfence/main.c diff --git a/regression/cbmc-library/__builtin_ia32_sfence-01/test.desc b/regression/cbmc-library/__builtin_ia32_sfence/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_ia32_sfence-01/test.desc rename to regression/cbmc-library/__builtin_ia32_sfence/test.desc diff --git a/regression/cbmc-library/__builtin_isinf-01/main.c b/regression/cbmc-library/__builtin_isinf/main.c similarity index 100% rename from regression/cbmc-library/__builtin_isinf-01/main.c rename to regression/cbmc-library/__builtin_isinf/main.c diff --git a/regression/cbmc-library/__builtin_isinf-01/test.desc b/regression/cbmc-library/__builtin_isinf/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_isinf-01/test.desc rename to regression/cbmc-library/__builtin_isinf/test.desc diff --git a/regression/cbmc-library/__builtin_isinff-01/main.c b/regression/cbmc-library/__builtin_isinff/main.c similarity index 100% rename from regression/cbmc-library/__builtin_isinff-01/main.c rename to regression/cbmc-library/__builtin_isinff/main.c diff --git a/regression/cbmc-library/__builtin_isinff-01/test.desc b/regression/cbmc-library/__builtin_isinff/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_isinff-01/test.desc rename to regression/cbmc-library/__builtin_isinff/test.desc diff --git a/regression/cbmc-library/__builtin_isnan-01/main.c b/regression/cbmc-library/__builtin_isnan/main.c similarity index 100% rename from regression/cbmc-library/__builtin_isnan-01/main.c rename to regression/cbmc-library/__builtin_isnan/main.c diff --git a/regression/cbmc-library/__builtin_isnan-01/test.desc b/regression/cbmc-library/__builtin_isnan/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_isnan-01/test.desc rename to regression/cbmc-library/__builtin_isnan/test.desc diff --git a/regression/cbmc-library/__builtin_isnanf-01/main.c b/regression/cbmc-library/__builtin_isnanf/main.c similarity index 100% rename from regression/cbmc-library/__builtin_isnanf-01/main.c rename to regression/cbmc-library/__builtin_isnanf/main.c diff --git a/regression/cbmc-library/__builtin_isnanf-01/test.desc b/regression/cbmc-library/__builtin_isnanf/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_isnanf-01/test.desc rename to regression/cbmc-library/__builtin_isnanf/test.desc diff --git a/regression/cbmc-library/__builtin_labs-01/main.c b/regression/cbmc-library/__builtin_labs/main.c similarity index 100% rename from regression/cbmc-library/__builtin_labs-01/main.c rename to regression/cbmc-library/__builtin_labs/main.c diff --git a/regression/cbmc-library/__builtin_labs-01/test.desc b/regression/cbmc-library/__builtin_labs/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_labs-01/test.desc rename to regression/cbmc-library/__builtin_labs/test.desc diff --git a/regression/cbmc-library/__builtin_llabs-01/main.c b/regression/cbmc-library/__builtin_llabs/main.c similarity index 99% rename from regression/cbmc-library/__builtin_llabs-01/main.c rename to regression/cbmc-library/__builtin_llabs/main.c index 6a0f074faaa..8d81b8c0633 100644 --- a/regression/cbmc-library/__builtin_llabs-01/main.c +++ b/regression/cbmc-library/__builtin_llabs/main.c @@ -1,5 +1,4 @@ #include - #include #ifndef __GNUC__ diff --git a/regression/cbmc-library/__builtin_llabs-01/test.desc b/regression/cbmc-library/__builtin_llabs/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_llabs-01/test.desc rename to regression/cbmc-library/__builtin_llabs/test.desc diff --git a/regression/cbmc-library/__builtin_memset-01/main.c b/regression/cbmc-library/__builtin_memset/main.c similarity index 100% rename from regression/cbmc-library/__builtin_memset-01/main.c rename to regression/cbmc-library/__builtin_memset/main.c diff --git a/regression/cbmc-library/__builtin_memset-01/test.desc b/regression/cbmc-library/__builtin_memset/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_memset-01/test.desc rename to regression/cbmc-library/__builtin_memset/test.desc diff --git a/regression/cbmc-library/__builtin_nan-01/main.c b/regression/cbmc-library/__builtin_nan/main.c similarity index 100% rename from regression/cbmc-library/__builtin_nan-01/main.c rename to regression/cbmc-library/__builtin_nan/main.c diff --git a/regression/cbmc-library/__builtin_nan-01/test.desc b/regression/cbmc-library/__builtin_nan/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_nan-01/test.desc rename to regression/cbmc-library/__builtin_nan/test.desc diff --git a/regression/cbmc-library/__builtin_nanf-01/main.c b/regression/cbmc-library/__builtin_nanf/main.c similarity index 100% rename from regression/cbmc-library/__builtin_nanf-01/main.c rename to regression/cbmc-library/__builtin_nanf/main.c diff --git a/regression/cbmc-library/__builtin_nanf-01/test.desc b/regression/cbmc-library/__builtin_nanf/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_nanf-01/test.desc rename to regression/cbmc-library/__builtin_nanf/test.desc diff --git a/regression/cbmc-library/__builtin_powi-01/main.c b/regression/cbmc-library/__builtin_powi/main.c similarity index 100% rename from regression/cbmc-library/__builtin_powi-01/main.c rename to regression/cbmc-library/__builtin_powi/main.c diff --git a/regression/cbmc-library/__builtin_powi-01/test.desc b/regression/cbmc-library/__builtin_powi/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_powi-01/test.desc rename to regression/cbmc-library/__builtin_powi/test.desc diff --git a/regression/cbmc-library/__builtin_powif-01/main.c b/regression/cbmc-library/__builtin_powif/main.c similarity index 100% rename from regression/cbmc-library/__builtin_powif-01/main.c rename to regression/cbmc-library/__builtin_powif/main.c diff --git a/regression/cbmc-library/__builtin_powif-01/test.desc b/regression/cbmc-library/__builtin_powif/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_powif-01/test.desc rename to regression/cbmc-library/__builtin_powif/test.desc diff --git a/regression/cbmc-library/__builtin_powil-01/main.c b/regression/cbmc-library/__builtin_powil/main.c similarity index 100% rename from regression/cbmc-library/__builtin_powil-01/main.c rename to regression/cbmc-library/__builtin_powil/main.c diff --git a/regression/cbmc-library/__builtin_powil-01/test.desc b/regression/cbmc-library/__builtin_powil/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_powil-01/test.desc rename to regression/cbmc-library/__builtin_powil/test.desc diff --git a/regression/cbmc-library/__delete-01/main.c b/regression/cbmc-library/__delete/main.c similarity index 100% rename from regression/cbmc-library/__delete-01/main.c rename to regression/cbmc-library/__delete/main.c diff --git a/regression/cbmc-library/__delete-01/test.desc b/regression/cbmc-library/__delete/test.desc similarity index 100% rename from regression/cbmc-library/__delete-01/test.desc rename to regression/cbmc-library/__delete/test.desc diff --git a/regression/cbmc-library/__delete_array-01/main.c b/regression/cbmc-library/__delete_array/main.c similarity index 100% rename from regression/cbmc-library/__delete_array-01/main.c rename to regression/cbmc-library/__delete_array/main.c diff --git a/regression/cbmc-library/__delete_array-01/test.desc b/regression/cbmc-library/__delete_array/test.desc similarity index 100% rename from regression/cbmc-library/__delete_array-01/test.desc rename to regression/cbmc-library/__delete_array/test.desc diff --git a/regression/cbmc-library/__errno-01/main.c b/regression/cbmc-library/__errno/main.c similarity index 100% rename from regression/cbmc-library/__errno-01/main.c rename to regression/cbmc-library/__errno/main.c diff --git a/regression/cbmc-library/__errno-01/test.desc b/regression/cbmc-library/__errno/test.desc similarity index 100% rename from regression/cbmc-library/__errno-01/test.desc rename to regression/cbmc-library/__errno/test.desc diff --git a/regression/cbmc-library/__errno_location-01/main.c b/regression/cbmc-library/__errno_location/main.c similarity index 100% rename from regression/cbmc-library/__errno_location-01/main.c rename to regression/cbmc-library/__errno_location/main.c diff --git a/regression/cbmc-library/__errno_location-01/test.desc b/regression/cbmc-library/__errno_location/test.desc similarity index 100% rename from regression/cbmc-library/__errno_location-01/test.desc rename to regression/cbmc-library/__errno_location/test.desc diff --git a/regression/cbmc-library/__error-01/main.c b/regression/cbmc-library/__error/main.c similarity index 100% rename from regression/cbmc-library/__error-01/main.c rename to regression/cbmc-library/__error/main.c diff --git a/regression/cbmc-library/__error-01/test.desc b/regression/cbmc-library/__error/test.desc similarity index 100% rename from regression/cbmc-library/__error-01/test.desc rename to regression/cbmc-library/__error/test.desc diff --git a/regression/cbmc-library/__finite-01/main.c b/regression/cbmc-library/__finite/main.c similarity index 100% rename from regression/cbmc-library/__finite-01/main.c rename to regression/cbmc-library/__finite/main.c diff --git a/regression/cbmc-library/__finite-01/test.desc b/regression/cbmc-library/__finite/test.desc similarity index 100% rename from regression/cbmc-library/__finite-01/test.desc rename to regression/cbmc-library/__finite/test.desc diff --git a/regression/cbmc-library/__finitef-01/main.c b/regression/cbmc-library/__finitef/main.c similarity index 100% rename from regression/cbmc-library/__finitef-01/main.c rename to regression/cbmc-library/__finitef/main.c diff --git a/regression/cbmc-library/__finitef-01/test.desc b/regression/cbmc-library/__finitef/test.desc similarity index 100% rename from regression/cbmc-library/__finitef-01/test.desc rename to regression/cbmc-library/__finitef/test.desc diff --git a/regression/cbmc-library/__finitel-01/main.c b/regression/cbmc-library/__finitel/main.c similarity index 100% rename from regression/cbmc-library/__finitel-01/main.c rename to regression/cbmc-library/__finitel/main.c diff --git a/regression/cbmc-library/__finitel-01/test.desc b/regression/cbmc-library/__finitel/test.desc similarity index 100% rename from regression/cbmc-library/__finitel-01/test.desc rename to regression/cbmc-library/__finitel/test.desc diff --git a/regression/cbmc-library/__flt_rounds-01/main.c b/regression/cbmc-library/__flt_rounds/main.c similarity index 100% rename from regression/cbmc-library/__flt_rounds-01/main.c rename to regression/cbmc-library/__flt_rounds/main.c diff --git a/regression/cbmc-library/__flt_rounds-01/test.desc b/regression/cbmc-library/__flt_rounds/test.desc similarity index 100% rename from regression/cbmc-library/__flt_rounds-01/test.desc rename to regression/cbmc-library/__flt_rounds/test.desc diff --git a/regression/cbmc-library/__fpclassify-01/main.c b/regression/cbmc-library/__fpclassify/main.c similarity index 100% rename from regression/cbmc-library/__fpclassify-01/main.c rename to regression/cbmc-library/__fpclassify/main.c diff --git a/regression/cbmc-library/__fpclassify-01/refine.desc b/regression/cbmc-library/__fpclassify/refine.desc similarity index 100% rename from regression/cbmc-library/__fpclassify-01/refine.desc rename to regression/cbmc-library/__fpclassify/refine.desc diff --git a/regression/cbmc-library/__fpclassify-01/test.desc b/regression/cbmc-library/__fpclassify/test.desc similarity index 100% rename from regression/cbmc-library/__fpclassify-01/test.desc rename to regression/cbmc-library/__fpclassify/test.desc diff --git a/regression/cbmc-library/__fpclassifyd-01/main.c b/regression/cbmc-library/__fpclassifyd/main.c similarity index 100% rename from regression/cbmc-library/__fpclassifyd-01/main.c rename to regression/cbmc-library/__fpclassifyd/main.c diff --git a/regression/cbmc-library/__fpclassifyd-01/test.desc b/regression/cbmc-library/__fpclassifyd/test.desc similarity index 100% rename from regression/cbmc-library/__fpclassifyd-01/test.desc rename to regression/cbmc-library/__fpclassifyd/test.desc diff --git a/regression/cbmc-library/__fpclassifyf-01/main.c b/regression/cbmc-library/__fpclassifyf/main.c similarity index 100% rename from regression/cbmc-library/__fpclassifyf-01/main.c rename to regression/cbmc-library/__fpclassifyf/main.c diff --git a/regression/cbmc-library/__fpclassifyf-01/test.desc b/regression/cbmc-library/__fpclassifyf/test.desc similarity index 100% rename from regression/cbmc-library/__fpclassifyf-01/test.desc rename to regression/cbmc-library/__fpclassifyf/test.desc diff --git a/regression/cbmc-library/__fpclassifyl-01/main.c b/regression/cbmc-library/__fpclassifyl/main.c similarity index 100% rename from regression/cbmc-library/__fpclassifyl-01/main.c rename to regression/cbmc-library/__fpclassifyl/main.c diff --git a/regression/cbmc-library/__fpclassifyl-01/test.desc b/regression/cbmc-library/__fpclassifyl/test.desc similarity index 100% rename from regression/cbmc-library/__fpclassifyl-01/test.desc rename to regression/cbmc-library/__fpclassifyl/test.desc diff --git a/regression/cbmc-library/__isinf-01/main.c b/regression/cbmc-library/__isinf/main.c similarity index 100% rename from regression/cbmc-library/__isinf-01/main.c rename to regression/cbmc-library/__isinf/main.c diff --git a/regression/cbmc-library/__isinf-01/test.desc b/regression/cbmc-library/__isinf/test.desc similarity index 100% rename from regression/cbmc-library/__isinf-01/test.desc rename to regression/cbmc-library/__isinf/test.desc diff --git a/regression/cbmc-library/__isinff-01/main.c b/regression/cbmc-library/__isinff/main.c similarity index 100% rename from regression/cbmc-library/__isinff-01/main.c rename to regression/cbmc-library/__isinff/main.c diff --git a/regression/cbmc-library/__isinff-01/test.desc b/regression/cbmc-library/__isinff/test.desc similarity index 100% rename from regression/cbmc-library/__isinff-01/test.desc rename to regression/cbmc-library/__isinff/test.desc diff --git a/regression/cbmc-library/__isinfl-01/main.c b/regression/cbmc-library/__isinfl/main.c similarity index 100% rename from regression/cbmc-library/__isinfl-01/main.c rename to regression/cbmc-library/__isinfl/main.c diff --git a/regression/cbmc-library/__isinfl-01/test.desc b/regression/cbmc-library/__isinfl/test.desc similarity index 100% rename from regression/cbmc-library/__isinfl-01/test.desc rename to regression/cbmc-library/__isinfl/test.desc diff --git a/regression/cbmc-library/__isnan-01/main.c b/regression/cbmc-library/__isnan/main.c similarity index 100% rename from regression/cbmc-library/__isnan-01/main.c rename to regression/cbmc-library/__isnan/main.c diff --git a/regression/cbmc-library/__isnan-01/test.desc b/regression/cbmc-library/__isnan/test.desc similarity index 100% rename from regression/cbmc-library/__isnan-01/test.desc rename to regression/cbmc-library/__isnan/test.desc diff --git a/regression/cbmc-library/__isnanf-01/main.c b/regression/cbmc-library/__isnanf/main.c similarity index 100% rename from regression/cbmc-library/__isnanf-01/main.c rename to regression/cbmc-library/__isnanf/main.c diff --git a/regression/cbmc-library/__isnanf-01/test.desc b/regression/cbmc-library/__isnanf/test.desc similarity index 100% rename from regression/cbmc-library/__isnanf-01/test.desc rename to regression/cbmc-library/__isnanf/test.desc diff --git a/regression/cbmc-library/__isnanl-01/main.c b/regression/cbmc-library/__isnanl/main.c similarity index 100% rename from regression/cbmc-library/__isnanl-01/main.c rename to regression/cbmc-library/__isnanl/main.c diff --git a/regression/cbmc-library/__isnanl-01/test.desc b/regression/cbmc-library/__isnanl/test.desc similarity index 100% rename from regression/cbmc-library/__isnanl-01/test.desc rename to regression/cbmc-library/__isnanl/test.desc diff --git a/regression/cbmc-library/__isnormalf-01/main.c b/regression/cbmc-library/__isnormalf/main.c similarity index 100% rename from regression/cbmc-library/__isnormalf-01/main.c rename to regression/cbmc-library/__isnormalf/main.c diff --git a/regression/cbmc-library/__isnormalf-01/test.desc b/regression/cbmc-library/__isnormalf/test.desc similarity index 100% rename from regression/cbmc-library/__isnormalf-01/test.desc rename to regression/cbmc-library/__isnormalf/test.desc diff --git a/regression/cbmc-library/__new-01/main.c b/regression/cbmc-library/__new/main.c similarity index 100% rename from regression/cbmc-library/__new-01/main.c rename to regression/cbmc-library/__new/main.c diff --git a/regression/cbmc-library/__new-01/test.desc b/regression/cbmc-library/__new/test.desc similarity index 100% rename from regression/cbmc-library/__new-01/test.desc rename to regression/cbmc-library/__new/test.desc diff --git a/regression/cbmc-library/__new_array-01/main.c b/regression/cbmc-library/__new_array/main.c similarity index 100% rename from regression/cbmc-library/__new_array-01/main.c rename to regression/cbmc-library/__new_array/main.c diff --git a/regression/cbmc-library/__new_array-01/test.desc b/regression/cbmc-library/__new_array/test.desc similarity index 100% rename from regression/cbmc-library/__new_array-01/test.desc rename to regression/cbmc-library/__new_array/test.desc diff --git a/regression/cbmc-library/__placement_new-01/main.c b/regression/cbmc-library/__placement_new/main.c similarity index 100% rename from regression/cbmc-library/__placement_new-01/main.c rename to regression/cbmc-library/__placement_new/main.c diff --git a/regression/cbmc-library/__placement_new-01/test.desc b/regression/cbmc-library/__placement_new/test.desc similarity index 100% rename from regression/cbmc-library/__placement_new-01/test.desc rename to regression/cbmc-library/__placement_new/test.desc diff --git a/regression/cbmc-library/__signbit-01/main.c b/regression/cbmc-library/__signbit/main.c similarity index 100% rename from regression/cbmc-library/__signbit-01/main.c rename to regression/cbmc-library/__signbit/main.c diff --git a/regression/cbmc-library/__signbit-01/test.desc b/regression/cbmc-library/__signbit/test.desc similarity index 100% rename from regression/cbmc-library/__signbit-01/test.desc rename to regression/cbmc-library/__signbit/test.desc diff --git a/regression/cbmc-library/__signbitd-01/main.c b/regression/cbmc-library/__signbitd/main.c similarity index 100% rename from regression/cbmc-library/__signbitd-01/main.c rename to regression/cbmc-library/__signbitd/main.c diff --git a/regression/cbmc-library/__signbitd-01/test.desc b/regression/cbmc-library/__signbitd/test.desc similarity index 100% rename from regression/cbmc-library/__signbitd-01/test.desc rename to regression/cbmc-library/__signbitd/test.desc diff --git a/regression/cbmc-library/__signbitf-01/main.c b/regression/cbmc-library/__signbitf/main.c similarity index 100% rename from regression/cbmc-library/__signbitf-01/main.c rename to regression/cbmc-library/__signbitf/main.c diff --git a/regression/cbmc-library/__signbitf-01/test.desc b/regression/cbmc-library/__signbitf/test.desc similarity index 100% rename from regression/cbmc-library/__signbitf-01/test.desc rename to regression/cbmc-library/__signbitf/test.desc diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_remainder/main.c similarity index 100% rename from regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c rename to regression/cbmc-library/__sort_of_CPROVER_remainder/main.c diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_remainder/test.desc similarity index 100% rename from regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc rename to regression/cbmc-library/__sort_of_CPROVER_remainder/test.desc diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_remainderf/main.c similarity index 100% rename from regression/cbmc-library/__sort_of_CPROVER_remainderf-01/main.c rename to regression/cbmc-library/__sort_of_CPROVER_remainderf/main.c diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_remainderf/test.desc similarity index 100% rename from regression/cbmc-library/__sort_of_CPROVER_remainderf-01/test.desc rename to regression/cbmc-library/__sort_of_CPROVER_remainderf/test.desc diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_remainderl/main.c similarity index 100% rename from regression/cbmc-library/__sort_of_CPROVER_remainderl-01/main.c rename to regression/cbmc-library/__sort_of_CPROVER_remainderl/main.c diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_remainderl/test.desc similarity index 100% rename from regression/cbmc-library/__sort_of_CPROVER_remainderl-01/test.desc rename to regression/cbmc-library/__sort_of_CPROVER_remainderl/test.desc diff --git a/regression/cbmc-library/__stdio_common_vfprintf-01/main.c b/regression/cbmc-library/__stdio_common_vfprintf/main.c similarity index 100% rename from regression/cbmc-library/__stdio_common_vfprintf-01/main.c rename to regression/cbmc-library/__stdio_common_vfprintf/main.c diff --git a/regression/cbmc-library/__stdio_common_vfprintf-01/test.desc b/regression/cbmc-library/__stdio_common_vfprintf/test.desc similarity index 100% rename from regression/cbmc-library/__stdio_common_vfprintf-01/test.desc rename to regression/cbmc-library/__stdio_common_vfprintf/test.desc diff --git a/regression/cbmc-library/__sync_synchronize-01/main.c b/regression/cbmc-library/__sync_synchronize/main.c similarity index 100% rename from regression/cbmc-library/__sync_synchronize-01/main.c rename to regression/cbmc-library/__sync_synchronize/main.c diff --git a/regression/cbmc-library/__sync_synchronize-01/test.desc b/regression/cbmc-library/__sync_synchronize/test.desc similarity index 100% rename from regression/cbmc-library/__sync_synchronize-01/test.desc rename to regression/cbmc-library/__sync_synchronize/test.desc diff --git a/regression/cbmc-library/_beginthread-01/main.c b/regression/cbmc-library/_beginthread/main.c similarity index 100% rename from regression/cbmc-library/_beginthread-01/main.c rename to regression/cbmc-library/_beginthread/main.c diff --git a/regression/cbmc-library/_beginthread-01/test.desc b/regression/cbmc-library/_beginthread/test.desc similarity index 100% rename from regression/cbmc-library/_beginthread-01/test.desc rename to regression/cbmc-library/_beginthread/test.desc diff --git a/regression/cbmc-library/_beginthreadex-01/main.c b/regression/cbmc-library/_beginthreadex/main.c similarity index 100% rename from regression/cbmc-library/_beginthreadex-01/main.c rename to regression/cbmc-library/_beginthreadex/main.c diff --git a/regression/cbmc-library/_beginthreadex-01/test.desc b/regression/cbmc-library/_beginthreadex/test.desc similarity index 100% rename from regression/cbmc-library/_beginthreadex-01/test.desc rename to regression/cbmc-library/_beginthreadex/test.desc diff --git a/regression/cbmc-library/_close-01/main.c b/regression/cbmc-library/_close/main.c similarity index 100% rename from regression/cbmc-library/_close-01/main.c rename to regression/cbmc-library/_close/main.c diff --git a/regression/cbmc-library/_close-01/test.desc b/regression/cbmc-library/_close/test.desc similarity index 100% rename from regression/cbmc-library/_close-01/test.desc rename to regression/cbmc-library/_close/test.desc diff --git a/regression/cbmc-library/_controlfp-01/main.c b/regression/cbmc-library/_controlfp/main.c similarity index 100% rename from regression/cbmc-library/_controlfp-01/main.c rename to regression/cbmc-library/_controlfp/main.c diff --git a/regression/cbmc-library/_controlfp-01/test.desc b/regression/cbmc-library/_controlfp/test.desc similarity index 100% rename from regression/cbmc-library/_controlfp-01/test.desc rename to regression/cbmc-library/_controlfp/test.desc diff --git a/regression/cbmc-library/_dclass-01/main.c b/regression/cbmc-library/_dclass/main.c similarity index 100% rename from regression/cbmc-library/_dclass-01/main.c rename to regression/cbmc-library/_dclass/main.c diff --git a/regression/cbmc-library/_dclass-01/test.desc b/regression/cbmc-library/_dclass/test.desc similarity index 100% rename from regression/cbmc-library/_dclass-01/test.desc rename to regression/cbmc-library/_dclass/test.desc diff --git a/regression/cbmc-library/_dsign-01/main.c b/regression/cbmc-library/_dsign/main.c similarity index 100% rename from regression/cbmc-library/_dsign-01/main.c rename to regression/cbmc-library/_dsign/main.c diff --git a/regression/cbmc-library/_dsign-01/test.desc b/regression/cbmc-library/_dsign/test.desc similarity index 100% rename from regression/cbmc-library/_dsign-01/test.desc rename to regression/cbmc-library/_dsign/test.desc diff --git a/regression/cbmc-library/_errno-01/main.c b/regression/cbmc-library/_errno/main.c similarity index 100% rename from regression/cbmc-library/_errno-01/main.c rename to regression/cbmc-library/_errno/main.c diff --git a/regression/cbmc-library/_errno-01/test.desc b/regression/cbmc-library/_errno/test.desc similarity index 100% rename from regression/cbmc-library/_errno-01/test.desc rename to regression/cbmc-library/_errno/test.desc diff --git a/regression/cbmc-library/_fdclass-01/main.c b/regression/cbmc-library/_fdclass/main.c similarity index 100% rename from regression/cbmc-library/_fdclass-01/main.c rename to regression/cbmc-library/_fdclass/main.c diff --git a/regression/cbmc-library/_fdclass-01/test.desc b/regression/cbmc-library/_fdclass/test.desc similarity index 100% rename from regression/cbmc-library/_fdclass-01/test.desc rename to regression/cbmc-library/_fdclass/test.desc diff --git a/regression/cbmc-library/_fdopen-01/main.c b/regression/cbmc-library/_fdopen/main.c similarity index 100% rename from regression/cbmc-library/_fdopen-01/main.c rename to regression/cbmc-library/_fdopen/main.c diff --git a/regression/cbmc-library/_fdopen-01/test.desc b/regression/cbmc-library/_fdopen/test.desc similarity index 100% rename from regression/cbmc-library/_fdopen-01/test.desc rename to regression/cbmc-library/_fdopen/test.desc diff --git a/regression/cbmc-library/_fdsign-01/main.c b/regression/cbmc-library/_fdsign/main.c similarity index 100% rename from regression/cbmc-library/_fdsign-01/main.c rename to regression/cbmc-library/_fdsign/main.c diff --git a/regression/cbmc-library/_fdsign-01/test.desc b/regression/cbmc-library/_fdsign/test.desc similarity index 100% rename from regression/cbmc-library/_fdsign-01/test.desc rename to regression/cbmc-library/_fdsign/test.desc diff --git a/regression/cbmc-library/_isnan-01/main.c b/regression/cbmc-library/_isnan/main.c similarity index 100% rename from regression/cbmc-library/_isnan-01/main.c rename to regression/cbmc-library/_isnan/main.c diff --git a/regression/cbmc-library/_isnan-01/test.desc b/regression/cbmc-library/_isnan/test.desc similarity index 100% rename from regression/cbmc-library/_isnan-01/test.desc rename to regression/cbmc-library/_isnan/test.desc diff --git a/regression/cbmc-library/_ldclass-01/main.c b/regression/cbmc-library/_ldclass/main.c similarity index 100% rename from regression/cbmc-library/_ldclass-01/main.c rename to regression/cbmc-library/_ldclass/main.c diff --git a/regression/cbmc-library/_ldclass-01/test.desc b/regression/cbmc-library/_ldclass/test.desc similarity index 100% rename from regression/cbmc-library/_ldclass-01/test.desc rename to regression/cbmc-library/_ldclass/test.desc diff --git a/regression/cbmc-library/_ldsign-01/main.c b/regression/cbmc-library/_ldsign/main.c similarity index 100% rename from regression/cbmc-library/_ldsign-01/main.c rename to regression/cbmc-library/_ldsign/main.c diff --git a/regression/cbmc-library/_ldsign-01/test.desc b/regression/cbmc-library/_ldsign/test.desc similarity index 100% rename from regression/cbmc-library/_ldsign-01/test.desc rename to regression/cbmc-library/_ldsign/test.desc diff --git a/regression/cbmc-library/_longjmp-01/main.c b/regression/cbmc-library/_longjmp/main.c similarity index 100% rename from regression/cbmc-library/_longjmp-01/main.c rename to regression/cbmc-library/_longjmp/main.c diff --git a/regression/cbmc-library/_longjmp-01/test.desc b/regression/cbmc-library/_longjmp/test.desc similarity index 100% rename from regression/cbmc-library/_longjmp-01/test.desc rename to regression/cbmc-library/_longjmp/test.desc diff --git a/regression/cbmc-library/_mm_lfence-01/main.c b/regression/cbmc-library/_mm_lfence/main.c similarity index 100% rename from regression/cbmc-library/_mm_lfence-01/main.c rename to regression/cbmc-library/_mm_lfence/main.c diff --git a/regression/cbmc-library/_mm_lfence-01/test.desc b/regression/cbmc-library/_mm_lfence/test.desc similarity index 100% rename from regression/cbmc-library/_mm_lfence-01/test.desc rename to regression/cbmc-library/_mm_lfence/test.desc diff --git a/regression/cbmc-library/_mm_mfence-01/main.c b/regression/cbmc-library/_mm_mfence/main.c similarity index 100% rename from regression/cbmc-library/_mm_mfence-01/main.c rename to regression/cbmc-library/_mm_mfence/main.c diff --git a/regression/cbmc-library/_mm_mfence-01/test.desc b/regression/cbmc-library/_mm_mfence/test.desc similarity index 100% rename from regression/cbmc-library/_mm_mfence-01/test.desc rename to regression/cbmc-library/_mm_mfence/test.desc diff --git a/regression/cbmc-library/_pthread_join-01/main.c b/regression/cbmc-library/_pthread_join/main.c similarity index 100% rename from regression/cbmc-library/_pthread_join-01/main.c rename to regression/cbmc-library/_pthread_join/main.c diff --git a/regression/cbmc-library/_pthread_join-01/test.desc b/regression/cbmc-library/_pthread_join/test.desc similarity index 100% rename from regression/cbmc-library/_pthread_join-01/test.desc rename to regression/cbmc-library/_pthread_join/test.desc diff --git a/regression/cbmc-library/_read-01/main.c b/regression/cbmc-library/_read/main.c similarity index 100% rename from regression/cbmc-library/_read-01/main.c rename to regression/cbmc-library/_read/main.c diff --git a/regression/cbmc-library/_read-01/test.desc b/regression/cbmc-library/_read/test.desc similarity index 100% rename from regression/cbmc-library/_read-01/test.desc rename to regression/cbmc-library/_read/test.desc diff --git a/regression/cbmc-library/_sleep-01/main.c b/regression/cbmc-library/_sleep/main.c similarity index 100% rename from regression/cbmc-library/_sleep-01/main.c rename to regression/cbmc-library/_sleep/main.c diff --git a/regression/cbmc-library/_sleep-01/test.desc b/regression/cbmc-library/_sleep/test.desc similarity index 100% rename from regression/cbmc-library/_sleep-01/test.desc rename to regression/cbmc-library/_sleep/test.desc diff --git a/regression/cbmc-library/_status87-01/main.c b/regression/cbmc-library/_status87/main.c similarity index 100% rename from regression/cbmc-library/_status87-01/main.c rename to regression/cbmc-library/_status87/main.c diff --git a/regression/cbmc-library/_status87-01/test.desc b/regression/cbmc-library/_status87/test.desc similarity index 100% rename from regression/cbmc-library/_status87-01/test.desc rename to regression/cbmc-library/_status87/test.desc diff --git a/regression/cbmc-library/_statusfp-01/main.c b/regression/cbmc-library/_statusfp/main.c similarity index 100% rename from regression/cbmc-library/_statusfp-01/main.c rename to regression/cbmc-library/_statusfp/main.c diff --git a/regression/cbmc-library/_statusfp-01/test.desc b/regression/cbmc-library/_statusfp/test.desc similarity index 100% rename from regression/cbmc-library/_statusfp-01/test.desc rename to regression/cbmc-library/_statusfp/test.desc diff --git a/regression/cbmc-library/_statusfp2-01/main.c b/regression/cbmc-library/_statusfp2/main.c similarity index 100% rename from regression/cbmc-library/_statusfp2-01/main.c rename to regression/cbmc-library/_statusfp2/main.c diff --git a/regression/cbmc-library/_statusfp2-01/test.desc b/regression/cbmc-library/_statusfp2/test.desc similarity index 100% rename from regression/cbmc-library/_statusfp2-01/test.desc rename to regression/cbmc-library/_statusfp2/test.desc diff --git a/regression/cbmc-library/_strftime-01/main.c b/regression/cbmc-library/_strftime/main.c similarity index 100% rename from regression/cbmc-library/_strftime-01/main.c rename to regression/cbmc-library/_strftime/main.c diff --git a/regression/cbmc-library/_strftime-01/test.desc b/regression/cbmc-library/_strftime/test.desc similarity index 100% rename from regression/cbmc-library/_strftime-01/test.desc rename to regression/cbmc-library/_strftime/test.desc diff --git a/regression/cbmc-library/_usleep-01/main.c b/regression/cbmc-library/_usleep/main.c similarity index 100% rename from regression/cbmc-library/_usleep-01/main.c rename to regression/cbmc-library/_usleep/main.c diff --git a/regression/cbmc-library/_usleep-01/test.desc b/regression/cbmc-library/_usleep/test.desc similarity index 100% rename from regression/cbmc-library/_usleep-01/test.desc rename to regression/cbmc-library/_usleep/test.desc diff --git a/regression/cbmc-library/_write-01/main.c b/regression/cbmc-library/_write/main.c similarity index 100% rename from regression/cbmc-library/_write-01/main.c rename to regression/cbmc-library/_write/main.c diff --git a/regression/cbmc-library/_write-01/test.desc b/regression/cbmc-library/_write/test.desc similarity index 100% rename from regression/cbmc-library/_write-01/test.desc rename to regression/cbmc-library/_write/test.desc diff --git a/regression/cbmc-library/abort-01/main.c b/regression/cbmc-library/abort/main.c similarity index 100% rename from regression/cbmc-library/abort-01/main.c rename to regression/cbmc-library/abort/main.c diff --git a/regression/cbmc-library/abort-01/test.desc b/regression/cbmc-library/abort/test.desc similarity index 100% rename from regression/cbmc-library/abort-01/test.desc rename to regression/cbmc-library/abort/test.desc diff --git a/regression/cbmc-library/abs-01/main.c b/regression/cbmc-library/abs/main.c similarity index 90% rename from regression/cbmc-library/abs-01/main.c rename to regression/cbmc-library/abs/main.c index f15f84e3c5d..ace50236b58 100644 --- a/regression/cbmc-library/abs-01/main.c +++ b/regression/cbmc-library/abs/main.c @@ -3,8 +3,8 @@ #include #ifdef _WIN32 -#include -#define isnan _isnan +# include +# define isnan _isnan #endif int main() diff --git a/regression/cbmc-library/abs-01/test.desc b/regression/cbmc-library/abs/test.desc similarity index 100% rename from regression/cbmc-library/abs-01/test.desc rename to regression/cbmc-library/abs/test.desc diff --git a/regression/cbmc-library/alloca-01/main.c b/regression/cbmc-library/alloca/main_01.c similarity index 100% rename from regression/cbmc-library/alloca-01/main.c rename to regression/cbmc-library/alloca/main_01.c diff --git a/regression/cbmc-library/alloca-02/main.c b/regression/cbmc-library/alloca/main_02.c similarity index 100% rename from regression/cbmc-library/alloca-02/main.c rename to regression/cbmc-library/alloca/main_02.c diff --git a/regression/cbmc-library/alloca-03/main.c b/regression/cbmc-library/alloca/main_03.c similarity index 100% rename from regression/cbmc-library/alloca-03/main.c rename to regression/cbmc-library/alloca/main_03.c diff --git a/regression/cbmc-library/alloca_declaration/missing_parameters.c b/regression/cbmc-library/alloca/missing_parameters.c similarity index 100% rename from regression/cbmc-library/alloca_declaration/missing_parameters.c rename to regression/cbmc-library/alloca/missing_parameters.c diff --git a/regression/cbmc-library/alloca_declaration/missing_parameters.desc b/regression/cbmc-library/alloca/missing_parameters.desc similarity index 100% rename from regression/cbmc-library/alloca_declaration/missing_parameters.desc rename to regression/cbmc-library/alloca/missing_parameters.desc diff --git a/regression/cbmc-library/alloca-01/test.desc b/regression/cbmc-library/alloca/test_01.desc similarity index 93% rename from regression/cbmc-library/alloca-01/test.desc rename to regression/cbmc-library/alloca/test_01.desc index 66fa40a9537..9a37225c0da 100644 --- a/regression/cbmc-library/alloca-01/test.desc +++ b/regression/cbmc-library/alloca/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --pointer-check ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/alloca-02/test.desc b/regression/cbmc-library/alloca/test_02.desc similarity index 94% rename from regression/cbmc-library/alloca-02/test.desc rename to regression/cbmc-library/alloca/test_02.desc index 273ea7118de..8ddb64e09cc 100644 --- a/regression/cbmc-library/alloca-02/test.desc +++ b/regression/cbmc-library/alloca/test_02.desc @@ -1,5 +1,5 @@ CORE -main.c +main_02.c --pointer-check dereference failure: dead object in \*from_foo: FAILURE$ ^\*\* 2 of 7 failed diff --git a/regression/cbmc-library/alloca-03/test.desc b/regression/cbmc-library/alloca/test_03.desc similarity index 95% rename from regression/cbmc-library/alloca-03/test.desc rename to regression/cbmc-library/alloca/test_03.desc index 0ce80143c07..bf97fd0085f 100644 --- a/regression/cbmc-library/alloca-03/test.desc +++ b/regression/cbmc-library/alloca/test_03.desc @@ -1,5 +1,5 @@ CORE -main.c +main_03.c --pointer-check ^\[main.pointer_dereference.\d+\] line 31 dereference failure: dead object in \*global: FAILURE$ ^\*\* 1 of \d+ failed diff --git a/regression/cbmc-library/alloca_declaration/too_many_parameters.c b/regression/cbmc-library/alloca/too_many_parameters.c similarity index 100% rename from regression/cbmc-library/alloca_declaration/too_many_parameters.c rename to regression/cbmc-library/alloca/too_many_parameters.c diff --git a/regression/cbmc-library/alloca_declaration/too_many_parameters.desc b/regression/cbmc-library/alloca/too_many_parameters.desc similarity index 100% rename from regression/cbmc-library/alloca_declaration/too_many_parameters.desc rename to regression/cbmc-library/alloca/too_many_parameters.desc diff --git a/regression/cbmc-library/alloca_declaration/undeclared.c b/regression/cbmc-library/alloca/undeclared.c similarity index 100% rename from regression/cbmc-library/alloca_declaration/undeclared.c rename to regression/cbmc-library/alloca/undeclared.c diff --git a/regression/cbmc-library/alloca_declaration/undeclared.desc b/regression/cbmc-library/alloca/undeclared.desc similarity index 100% rename from regression/cbmc-library/alloca_declaration/undeclared.desc rename to regression/cbmc-library/alloca/undeclared.desc diff --git a/regression/cbmc-library/alloca_declaration/valid_declaration.c b/regression/cbmc-library/alloca/valid_declaration.c similarity index 100% rename from regression/cbmc-library/alloca_declaration/valid_declaration.c rename to regression/cbmc-library/alloca/valid_declaration.c diff --git a/regression/cbmc-library/alloca_declaration/valid_declaration.desc b/regression/cbmc-library/alloca/valid_declaration.desc similarity index 100% rename from regression/cbmc-library/alloca_declaration/valid_declaration.desc rename to regression/cbmc-library/alloca/valid_declaration.desc diff --git a/regression/cbmc-library/alloca_declaration/wrong_parameter_type.c b/regression/cbmc-library/alloca/wrong_parameter_type.c similarity index 100% rename from regression/cbmc-library/alloca_declaration/wrong_parameter_type.c rename to regression/cbmc-library/alloca/wrong_parameter_type.c diff --git a/regression/cbmc-library/alloca_declaration/wrong_parameter_type.desc b/regression/cbmc-library/alloca/wrong_parameter_type.desc similarity index 100% rename from regression/cbmc-library/alloca_declaration/wrong_parameter_type.desc rename to regression/cbmc-library/alloca/wrong_parameter_type.desc diff --git a/regression/cbmc-library/alloca_declaration/wrong_return_type.c b/regression/cbmc-library/alloca/wrong_return_type.c similarity index 100% rename from regression/cbmc-library/alloca_declaration/wrong_return_type.c rename to regression/cbmc-library/alloca/wrong_return_type.c diff --git a/regression/cbmc-library/alloca_declaration/wrong_return_type.desc b/regression/cbmc-library/alloca/wrong_return_type.desc similarity index 100% rename from regression/cbmc-library/alloca_declaration/wrong_return_type.desc rename to regression/cbmc-library/alloca/wrong_return_type.desc diff --git a/regression/cbmc-library/asctime-01/main.c b/regression/cbmc-library/asctime/main.c similarity index 100% rename from regression/cbmc-library/asctime-01/main.c rename to regression/cbmc-library/asctime/main.c diff --git a/regression/cbmc-library/asctime-01/test.desc b/regression/cbmc-library/asctime/test.desc similarity index 100% rename from regression/cbmc-library/asctime-01/test.desc rename to regression/cbmc-library/asctime/test.desc diff --git a/regression/cbmc-library/asprintf-01/main.c b/regression/cbmc-library/asprintf/main.c similarity index 100% rename from regression/cbmc-library/asprintf-01/main.c rename to regression/cbmc-library/asprintf/main.c diff --git a/regression/cbmc-library/asprintf-01/test.desc b/regression/cbmc-library/asprintf/test.desc similarity index 100% rename from regression/cbmc-library/asprintf-01/test.desc rename to regression/cbmc-library/asprintf/test.desc diff --git a/regression/cbmc-library/atoi-01/main.c b/regression/cbmc-library/atoi/main.c similarity index 100% rename from regression/cbmc-library/atoi-01/main.c rename to regression/cbmc-library/atoi/main.c diff --git a/regression/cbmc-library/atoi-01/test.desc b/regression/cbmc-library/atoi/test.desc similarity index 100% rename from regression/cbmc-library/atoi-01/test.desc rename to regression/cbmc-library/atoi/test.desc diff --git a/regression/cbmc-library/atol-01/main.c b/regression/cbmc-library/atol/main.c similarity index 100% rename from regression/cbmc-library/atol-01/main.c rename to regression/cbmc-library/atol/main.c diff --git a/regression/cbmc-library/atol-01/test.desc b/regression/cbmc-library/atol/test.desc similarity index 100% rename from regression/cbmc-library/atol-01/test.desc rename to regression/cbmc-library/atol/test.desc diff --git a/regression/cbmc-library/bzero-01/main.c b/regression/cbmc-library/bzero/main.c similarity index 100% rename from regression/cbmc-library/bzero-01/main.c rename to regression/cbmc-library/bzero/main.c diff --git a/regression/cbmc-library/bzero-01/test.desc b/regression/cbmc-library/bzero/test.desc similarity index 100% rename from regression/cbmc-library/bzero-01/test.desc rename to regression/cbmc-library/bzero/test.desc diff --git a/regression/cbmc-library/call_once-01/main.c b/regression/cbmc-library/call_once/main.c similarity index 100% rename from regression/cbmc-library/call_once-01/main.c rename to regression/cbmc-library/call_once/main.c diff --git a/regression/cbmc-library/call_once-01/test.desc b/regression/cbmc-library/call_once/test.desc similarity index 100% rename from regression/cbmc-library/call_once-01/test.desc rename to regression/cbmc-library/call_once/test.desc diff --git a/regression/cbmc-library/calloc-01/main.c b/regression/cbmc-library/calloc/main_01.c similarity index 100% rename from regression/cbmc-library/calloc-01/main.c rename to regression/cbmc-library/calloc/main_01.c diff --git a/regression/cbmc-library/calloc-02/main.c b/regression/cbmc-library/calloc/main_02.c similarity index 100% rename from regression/cbmc-library/calloc-02/main.c rename to regression/cbmc-library/calloc/main_02.c diff --git a/regression/cbmc-library/calloc-01/program-only.desc b/regression/cbmc-library/calloc/program-only_01.desc similarity index 96% rename from regression/cbmc-library/calloc-01/program-only.desc rename to regression/cbmc-library/calloc/program-only_01.desc index c798884d9dd..9c30c5c40d8 100644 --- a/regression/cbmc-library/calloc-01/program-only.desc +++ b/regression/cbmc-library/calloc/program-only_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --program-only dynamic_object#1 == \{ 0, 0 \} ^EXIT=0$ diff --git a/regression/cbmc-library/calloc-01/test.desc b/regression/cbmc-library/calloc/test_01.desc similarity index 90% rename from regression/cbmc-library/calloc-01/test.desc rename to regression/cbmc-library/calloc/test_01.desc index 915afae768a..899dfdff19b 100644 --- a/regression/cbmc-library/calloc-01/test.desc +++ b/regression/cbmc-library/calloc/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --no-malloc-may-fail ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/calloc-02/test.desc b/regression/cbmc-library/calloc/test_02.desc similarity index 93% rename from regression/cbmc-library/calloc-02/test.desc rename to regression/cbmc-library/calloc/test_02.desc index e9d6ddbb1d1..0ccf12b296c 100644 --- a/regression/cbmc-library/calloc-02/test.desc +++ b/regression/cbmc-library/calloc/test_02.desc @@ -1,5 +1,5 @@ CORE -main.c +main_02.c --unsigned-overflow-check --pointer-check --arrays-uf-always ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/ceil-01/main.c b/regression/cbmc-library/ceil/main.c similarity index 100% rename from regression/cbmc-library/ceil-01/main.c rename to regression/cbmc-library/ceil/main.c diff --git a/regression/cbmc-library/ceil-01/test.desc b/regression/cbmc-library/ceil/test.desc similarity index 100% rename from regression/cbmc-library/ceil-01/test.desc rename to regression/cbmc-library/ceil/test.desc diff --git a/regression/cbmc-library/ceilf-01/main.c b/regression/cbmc-library/ceilf/main.c similarity index 100% rename from regression/cbmc-library/ceilf-01/main.c rename to regression/cbmc-library/ceilf/main.c diff --git a/regression/cbmc-library/ceilf-01/test.desc b/regression/cbmc-library/ceilf/test.desc similarity index 100% rename from regression/cbmc-library/ceilf-01/test.desc rename to regression/cbmc-library/ceilf/test.desc diff --git a/regression/cbmc-library/ceill-01/main.c b/regression/cbmc-library/ceill/main.c similarity index 100% rename from regression/cbmc-library/ceill-01/main.c rename to regression/cbmc-library/ceill/main.c diff --git a/regression/cbmc-library/ceill-01/test.desc b/regression/cbmc-library/ceill/test.desc similarity index 100% rename from regression/cbmc-library/ceill-01/test.desc rename to regression/cbmc-library/ceill/test.desc diff --git a/regression/cbmc-library/clock_gettime-01/main.c b/regression/cbmc-library/clock_gettime/main.c similarity index 100% rename from regression/cbmc-library/clock_gettime-01/main.c rename to regression/cbmc-library/clock_gettime/main.c diff --git a/regression/cbmc-library/clock_gettime-01/test.desc b/regression/cbmc-library/clock_gettime/test.desc similarity index 100% rename from regression/cbmc-library/clock_gettime-01/test.desc rename to regression/cbmc-library/clock_gettime/test.desc diff --git a/regression/cbmc-library/close-01/main.c b/regression/cbmc-library/close/main.c similarity index 100% rename from regression/cbmc-library/close-01/main.c rename to regression/cbmc-library/close/main.c diff --git a/regression/cbmc-library/close-01/test.desc b/regression/cbmc-library/close/test.desc similarity index 100% rename from regression/cbmc-library/close-01/test.desc rename to regression/cbmc-library/close/test.desc diff --git a/regression/cbmc-library/closelog-01/main.c b/regression/cbmc-library/closelog/main.c similarity index 100% rename from regression/cbmc-library/closelog-01/main.c rename to regression/cbmc-library/closelog/main.c diff --git a/regression/cbmc-library/closelog-01/test.desc b/regression/cbmc-library/closelog/test.desc similarity index 100% rename from regression/cbmc-library/closelog-01/test.desc rename to regression/cbmc-library/closelog/test.desc diff --git a/regression/cbmc-library/cnd_broadcast-01/main.c b/regression/cbmc-library/cnd_broadcast/main.c similarity index 100% rename from regression/cbmc-library/cnd_broadcast-01/main.c rename to regression/cbmc-library/cnd_broadcast/main.c diff --git a/regression/cbmc-library/cnd_broadcast-01/test.desc b/regression/cbmc-library/cnd_broadcast/test.desc similarity index 100% rename from regression/cbmc-library/cnd_broadcast-01/test.desc rename to regression/cbmc-library/cnd_broadcast/test.desc diff --git a/regression/cbmc-library/cnd_destroy-01/main.c b/regression/cbmc-library/cnd_destroy/main.c similarity index 100% rename from regression/cbmc-library/cnd_destroy-01/main.c rename to regression/cbmc-library/cnd_destroy/main.c diff --git a/regression/cbmc-library/cnd_destroy-01/test.desc b/regression/cbmc-library/cnd_destroy/test.desc similarity index 100% rename from regression/cbmc-library/cnd_destroy-01/test.desc rename to regression/cbmc-library/cnd_destroy/test.desc diff --git a/regression/cbmc-library/cnd_init-01/main.c b/regression/cbmc-library/cnd_init/main.c similarity index 100% rename from regression/cbmc-library/cnd_init-01/main.c rename to regression/cbmc-library/cnd_init/main.c diff --git a/regression/cbmc-library/cnd_init-01/test.desc b/regression/cbmc-library/cnd_init/test.desc similarity index 100% rename from regression/cbmc-library/cnd_init-01/test.desc rename to regression/cbmc-library/cnd_init/test.desc diff --git a/regression/cbmc-library/cnd_signal-01/main.c b/regression/cbmc-library/cnd_signal/main.c similarity index 100% rename from regression/cbmc-library/cnd_signal-01/main.c rename to regression/cbmc-library/cnd_signal/main.c diff --git a/regression/cbmc-library/cnd_signal-01/test.desc b/regression/cbmc-library/cnd_signal/test.desc similarity index 100% rename from regression/cbmc-library/cnd_signal-01/test.desc rename to regression/cbmc-library/cnd_signal/test.desc diff --git a/regression/cbmc-library/cnd_timedwait-01/main.c b/regression/cbmc-library/cnd_timedwait/main.c similarity index 100% rename from regression/cbmc-library/cnd_timedwait-01/main.c rename to regression/cbmc-library/cnd_timedwait/main.c diff --git a/regression/cbmc-library/cnd_timedwait-01/test.desc b/regression/cbmc-library/cnd_timedwait/test.desc similarity index 100% rename from regression/cbmc-library/cnd_timedwait-01/test.desc rename to regression/cbmc-library/cnd_timedwait/test.desc diff --git a/regression/cbmc-library/cnd_wait-01/main.c b/regression/cbmc-library/cnd_wait/main.c similarity index 100% rename from regression/cbmc-library/cnd_wait-01/main.c rename to regression/cbmc-library/cnd_wait/main.c diff --git a/regression/cbmc-library/cnd_wait-01/test.desc b/regression/cbmc-library/cnd_wait/test.desc similarity index 100% rename from regression/cbmc-library/cnd_wait-01/test.desc rename to regression/cbmc-library/cnd_wait/test.desc diff --git a/regression/cbmc-library/copysign-01/main.c b/regression/cbmc-library/copysign/main.c similarity index 100% rename from regression/cbmc-library/copysign-01/main.c rename to regression/cbmc-library/copysign/main.c diff --git a/regression/cbmc-library/copysign-01/test.desc b/regression/cbmc-library/copysign/test.desc similarity index 100% rename from regression/cbmc-library/copysign-01/test.desc rename to regression/cbmc-library/copysign/test.desc diff --git a/regression/cbmc-library/copysignf-01/main.c b/regression/cbmc-library/copysignf/main.c similarity index 100% rename from regression/cbmc-library/copysignf-01/main.c rename to regression/cbmc-library/copysignf/main.c diff --git a/regression/cbmc-library/copysignf-01/test.desc b/regression/cbmc-library/copysignf/test.desc similarity index 100% rename from regression/cbmc-library/copysignf-01/test.desc rename to regression/cbmc-library/copysignf/test.desc diff --git a/regression/cbmc-library/copysignl-01/main.c b/regression/cbmc-library/copysignl/main.c similarity index 100% rename from regression/cbmc-library/copysignl-01/main.c rename to regression/cbmc-library/copysignl/main.c diff --git a/regression/cbmc-library/copysignl-01/test.desc b/regression/cbmc-library/copysignl/test.desc similarity index 100% rename from regression/cbmc-library/copysignl-01/test.desc rename to regression/cbmc-library/copysignl/test.desc diff --git a/regression/cbmc-library/cos-01/main.c b/regression/cbmc-library/cos/main.c similarity index 100% rename from regression/cbmc-library/cos-01/main.c rename to regression/cbmc-library/cos/main.c diff --git a/regression/cbmc-library/cos-01/test.desc b/regression/cbmc-library/cos/test.desc similarity index 100% rename from regression/cbmc-library/cos-01/test.desc rename to regression/cbmc-library/cos/test.desc diff --git a/regression/cbmc-library/cosf-01/main.c b/regression/cbmc-library/cosf/main.c similarity index 100% rename from regression/cbmc-library/cosf-01/main.c rename to regression/cbmc-library/cosf/main.c diff --git a/regression/cbmc-library/cosf-01/test.desc b/regression/cbmc-library/cosf/test.desc similarity index 100% rename from regression/cbmc-library/cosf-01/test.desc rename to regression/cbmc-library/cosf/test.desc diff --git a/regression/cbmc-library/cosl-01/main.c b/regression/cbmc-library/cosl/main.c similarity index 100% rename from regression/cbmc-library/cosl-01/main.c rename to regression/cbmc-library/cosl/main.c diff --git a/regression/cbmc-library/cosl-01/test.desc b/regression/cbmc-library/cosl/test.desc similarity index 100% rename from regression/cbmc-library/cosl-01/test.desc rename to regression/cbmc-library/cosl/test.desc diff --git a/regression/cbmc-library/creat-01/main.c b/regression/cbmc-library/creat/main.c similarity index 100% rename from regression/cbmc-library/creat-01/main.c rename to regression/cbmc-library/creat/main.c diff --git a/regression/cbmc-library/creat-01/test.desc b/regression/cbmc-library/creat/test.desc similarity index 100% rename from regression/cbmc-library/creat-01/test.desc rename to regression/cbmc-library/creat/test.desc diff --git a/regression/cbmc-library/ctime-01/main.c b/regression/cbmc-library/ctime/main.c similarity index 100% rename from regression/cbmc-library/ctime-01/main.c rename to regression/cbmc-library/ctime/main.c diff --git a/regression/cbmc-library/ctime-01/test.desc b/regression/cbmc-library/ctime/test.desc similarity index 100% rename from regression/cbmc-library/ctime-01/test.desc rename to regression/cbmc-library/ctime/test.desc diff --git a/regression/cbmc-library/dprintf-01/main.c b/regression/cbmc-library/dprintf/main.c similarity index 100% rename from regression/cbmc-library/dprintf-01/main.c rename to regression/cbmc-library/dprintf/main.c diff --git a/regression/cbmc-library/dprintf-01/test.desc b/regression/cbmc-library/dprintf/test.desc similarity index 100% rename from regression/cbmc-library/dprintf-01/test.desc rename to regression/cbmc-library/dprintf/test.desc diff --git a/regression/cbmc-library/err-01/main.c b/regression/cbmc-library/err/main.c similarity index 100% rename from regression/cbmc-library/err-01/main.c rename to regression/cbmc-library/err/main.c diff --git a/regression/cbmc-library/err-01/test.desc b/regression/cbmc-library/err/test.desc similarity index 100% rename from regression/cbmc-library/err-01/test.desc rename to regression/cbmc-library/err/test.desc diff --git a/regression/cbmc-library/errx-01/main.c b/regression/cbmc-library/errx/main.c similarity index 100% rename from regression/cbmc-library/errx-01/main.c rename to regression/cbmc-library/errx/main.c diff --git a/regression/cbmc-library/errx-01/test.desc b/regression/cbmc-library/errx/test.desc similarity index 100% rename from regression/cbmc-library/errx-01/test.desc rename to regression/cbmc-library/errx/test.desc diff --git a/regression/cbmc-library/exit-01/main.c b/regression/cbmc-library/exit/main.c similarity index 100% rename from regression/cbmc-library/exit-01/main.c rename to regression/cbmc-library/exit/main.c diff --git a/regression/cbmc-library/exit-01/test.desc b/regression/cbmc-library/exit/test.desc similarity index 100% rename from regression/cbmc-library/exit-01/test.desc rename to regression/cbmc-library/exit/test.desc diff --git a/regression/cbmc-library/exp-01/main.c b/regression/cbmc-library/exp/main.c similarity index 100% rename from regression/cbmc-library/exp-01/main.c rename to regression/cbmc-library/exp/main.c diff --git a/regression/cbmc-library/exp-01/test.desc b/regression/cbmc-library/exp/test.desc similarity index 100% rename from regression/cbmc-library/exp-01/test.desc rename to regression/cbmc-library/exp/test.desc diff --git a/regression/cbmc-library/exp2-01/main.c b/regression/cbmc-library/exp2/main.c similarity index 100% rename from regression/cbmc-library/exp2-01/main.c rename to regression/cbmc-library/exp2/main.c diff --git a/regression/cbmc-library/exp2-01/test.desc b/regression/cbmc-library/exp2/test.desc similarity index 100% rename from regression/cbmc-library/exp2-01/test.desc rename to regression/cbmc-library/exp2/test.desc diff --git a/regression/cbmc-library/exp2f-01/main.c b/regression/cbmc-library/exp2f/main.c similarity index 100% rename from regression/cbmc-library/exp2f-01/main.c rename to regression/cbmc-library/exp2f/main.c diff --git a/regression/cbmc-library/exp2f-01/test.desc b/regression/cbmc-library/exp2f/test.desc similarity index 100% rename from regression/cbmc-library/exp2f-01/test.desc rename to regression/cbmc-library/exp2f/test.desc diff --git a/regression/cbmc-library/exp2l-01/main.c b/regression/cbmc-library/exp2l/main.c similarity index 100% rename from regression/cbmc-library/exp2l-01/main.c rename to regression/cbmc-library/exp2l/main.c diff --git a/regression/cbmc-library/exp2l-01/test.desc b/regression/cbmc-library/exp2l/test.desc similarity index 100% rename from regression/cbmc-library/exp2l-01/test.desc rename to regression/cbmc-library/exp2l/test.desc diff --git a/regression/cbmc-library/expf-01/main.c b/regression/cbmc-library/expf/main.c similarity index 100% rename from regression/cbmc-library/expf-01/main.c rename to regression/cbmc-library/expf/main.c diff --git a/regression/cbmc-library/expf-01/test.desc b/regression/cbmc-library/expf/test.desc similarity index 100% rename from regression/cbmc-library/expf-01/test.desc rename to regression/cbmc-library/expf/test.desc diff --git a/regression/cbmc-library/expl-01/main.c b/regression/cbmc-library/expl/main.c similarity index 100% rename from regression/cbmc-library/expl-01/main.c rename to regression/cbmc-library/expl/main.c diff --git a/regression/cbmc-library/expl-01/test.desc b/regression/cbmc-library/expl/test.desc similarity index 100% rename from regression/cbmc-library/expl-01/test.desc rename to regression/cbmc-library/expl/test.desc diff --git a/regression/cbmc-library/fabs-01/main.c b/regression/cbmc-library/fabs/main.c similarity index 100% rename from regression/cbmc-library/fabs-01/main.c rename to regression/cbmc-library/fabs/main.c diff --git a/regression/cbmc-library/fabs-01/test.desc b/regression/cbmc-library/fabs/test.desc similarity index 100% rename from regression/cbmc-library/fabs-01/test.desc rename to regression/cbmc-library/fabs/test.desc diff --git a/regression/cbmc-library/fabsf-01/main.c b/regression/cbmc-library/fabsf/main.c similarity index 100% rename from regression/cbmc-library/fabsf-01/main.c rename to regression/cbmc-library/fabsf/main.c diff --git a/regression/cbmc-library/fabsf-01/test.desc b/regression/cbmc-library/fabsf/test.desc similarity index 100% rename from regression/cbmc-library/fabsf-01/test.desc rename to regression/cbmc-library/fabsf/test.desc diff --git a/regression/cbmc-library/fabsl-01/main.c b/regression/cbmc-library/fabsl/main.c similarity index 100% rename from regression/cbmc-library/fabsl-01/main.c rename to regression/cbmc-library/fabsl/main.c diff --git a/regression/cbmc-library/fabsl-01/test.desc b/regression/cbmc-library/fabsl/test.desc similarity index 100% rename from regression/cbmc-library/fabsl-01/test.desc rename to regression/cbmc-library/fabsl/test.desc diff --git a/regression/cbmc-library/fclose-01/main.c b/regression/cbmc-library/fclose/main.c similarity index 100% rename from regression/cbmc-library/fclose-01/main.c rename to regression/cbmc-library/fclose/main.c diff --git a/regression/cbmc-library/fclose-01/test.desc b/regression/cbmc-library/fclose/test.desc similarity index 100% rename from regression/cbmc-library/fclose-01/test.desc rename to regression/cbmc-library/fclose/test.desc diff --git a/regression/cbmc-library/fcntl-01/main.c b/regression/cbmc-library/fcntl/main.c similarity index 100% rename from regression/cbmc-library/fcntl-01/main.c rename to regression/cbmc-library/fcntl/main.c diff --git a/regression/cbmc-library/fcntl-01/test.desc b/regression/cbmc-library/fcntl/test.desc similarity index 100% rename from regression/cbmc-library/fcntl-01/test.desc rename to regression/cbmc-library/fcntl/test.desc diff --git a/regression/cbmc-library/fdim-01/main.c b/regression/cbmc-library/fdim/main.c similarity index 100% rename from regression/cbmc-library/fdim-01/main.c rename to regression/cbmc-library/fdim/main.c diff --git a/regression/cbmc-library/fdim-01/test.desc b/regression/cbmc-library/fdim/test.desc similarity index 100% rename from regression/cbmc-library/fdim-01/test.desc rename to regression/cbmc-library/fdim/test.desc diff --git a/regression/cbmc-library/fdimf-01/main.c b/regression/cbmc-library/fdimf/main.c similarity index 100% rename from regression/cbmc-library/fdimf-01/main.c rename to regression/cbmc-library/fdimf/main.c diff --git a/regression/cbmc-library/fdimf-01/test.desc b/regression/cbmc-library/fdimf/test.desc similarity index 100% rename from regression/cbmc-library/fdimf-01/test.desc rename to regression/cbmc-library/fdimf/test.desc diff --git a/regression/cbmc-library/fdiml-01/main.c b/regression/cbmc-library/fdiml/main.c similarity index 100% rename from regression/cbmc-library/fdiml-01/main.c rename to regression/cbmc-library/fdiml/main.c diff --git a/regression/cbmc-library/fdiml-01/test.desc b/regression/cbmc-library/fdiml/test.desc similarity index 100% rename from regression/cbmc-library/fdiml-01/test.desc rename to regression/cbmc-library/fdiml/test.desc diff --git a/regression/cbmc-library/fdopen-01/main.c b/regression/cbmc-library/fdopen/main.c similarity index 100% rename from regression/cbmc-library/fdopen-01/main.c rename to regression/cbmc-library/fdopen/main.c diff --git a/regression/cbmc-library/fdopen-01/test.desc b/regression/cbmc-library/fdopen/test.desc similarity index 100% rename from regression/cbmc-library/fdopen-01/test.desc rename to regression/cbmc-library/fdopen/test.desc diff --git a/regression/cbmc-library/fegetround-01/main.c b/regression/cbmc-library/fegetround/main.c similarity index 100% rename from regression/cbmc-library/fegetround-01/main.c rename to regression/cbmc-library/fegetround/main.c diff --git a/regression/cbmc-library/fegetround-01/test.desc b/regression/cbmc-library/fegetround/test.desc similarity index 100% rename from regression/cbmc-library/fegetround-01/test.desc rename to regression/cbmc-library/fegetround/test.desc diff --git a/regression/cbmc-library/feof-01/main.c b/regression/cbmc-library/feof/main.c similarity index 100% rename from regression/cbmc-library/feof-01/main.c rename to regression/cbmc-library/feof/main.c diff --git a/regression/cbmc-library/feof-01/test.desc b/regression/cbmc-library/feof/test.desc similarity index 100% rename from regression/cbmc-library/feof-01/test.desc rename to regression/cbmc-library/feof/test.desc diff --git a/regression/cbmc-library/feraiseexcept-01/main.c b/regression/cbmc-library/feraiseexcept/main.c similarity index 100% rename from regression/cbmc-library/feraiseexcept-01/main.c rename to regression/cbmc-library/feraiseexcept/main.c diff --git a/regression/cbmc-library/feraiseexcept-01/test.desc b/regression/cbmc-library/feraiseexcept/test.desc similarity index 100% rename from regression/cbmc-library/feraiseexcept-01/test.desc rename to regression/cbmc-library/feraiseexcept/test.desc diff --git a/regression/cbmc-library/ferror-01/main.c b/regression/cbmc-library/ferror/main.c similarity index 100% rename from regression/cbmc-library/ferror-01/main.c rename to regression/cbmc-library/ferror/main.c diff --git a/regression/cbmc-library/ferror-01/test.desc b/regression/cbmc-library/ferror/test.desc similarity index 100% rename from regression/cbmc-library/ferror-01/test.desc rename to regression/cbmc-library/ferror/test.desc diff --git a/regression/cbmc-library/fesetround-01/main.c b/regression/cbmc-library/fesetround/main_01.c similarity index 88% rename from regression/cbmc-library/fesetround-01/main.c rename to regression/cbmc-library/fesetround/main_01.c index 2bb8170638f..63d3bdbaca6 100644 --- a/regression/cbmc-library/fesetround-01/main.c +++ b/regression/cbmc-library/fesetround/main_01.c @@ -1,13 +1,13 @@ #ifdef __GNUC__ -#include -#include -#include +# include +# include +# include float nondet_value(); // Should work without this as it defaults to off. // It is explicitly ignored by GCC -#pragma STDC FENV_ACCESS OFF +# pragma STDC FENV_ACCESS OFF void roundingTest(float f1, float f2) { @@ -18,14 +18,14 @@ void roundingTest(float f1, float f2) float roundToNearestSum = f1 + f2; assert(roundToNearestSum == 0x1.000002p+0f); -#ifdef FE_DOWNWARD +# ifdef FE_DOWNWARD // Change the rounding mode fesetround(FE_DOWNWARD); // Should now round down to 0x1p+0; float roundDownSum = f1 + f2; assert(roundDownSum == 0x1.0p+0f); -#endif +# endif return; } diff --git a/regression/cbmc-library/fesetround-02/main.c b/regression/cbmc-library/fesetround/main_02.c similarity index 74% rename from regression/cbmc-library/fesetround-02/main.c rename to regression/cbmc-library/fesetround/main_02.c index f6f314e6112..4b233f15ca0 100644 --- a/regression/cbmc-library/fesetround-02/main.c +++ b/regression/cbmc-library/fesetround/main_02.c @@ -9,30 +9,30 @@ int main() #else -#include -#include +# include +# include int main() { -#ifdef FE_DOWNWARD +# ifdef FE_DOWNWARD fesetround(FE_DOWNWARD); assert(fegetround() == FE_DOWNWARD); -#endif +# endif -#ifdef FE_TONEAREST +# ifdef FE_TONEAREST fesetround(FE_TONEAREST); assert(fegetround() == FE_TONEAREST); -#endif +# endif -#ifdef FE_TOWARDZERO +# ifdef FE_TOWARDZERO fesetround(FE_TOWARDZERO); assert(fegetround() == FE_TOWARDZERO); -#endif +# endif -#ifdef FE_UPWARD +# ifdef FE_UPWARD fesetround(FE_UPWARD); assert(fegetround() == FE_UPWARD); -#endif +# endif } #endif diff --git a/regression/cbmc-library/fesetround-03/main.c b/regression/cbmc-library/fesetround/main_03.c similarity index 86% rename from regression/cbmc-library/fesetround-03/main.c rename to regression/cbmc-library/fesetround/main_03.c index f40097be3c6..0c6be63aa97 100644 --- a/regression/cbmc-library/fesetround-03/main.c +++ b/regression/cbmc-library/fesetround/main_03.c @@ -3,9 +3,9 @@ #ifdef __clang__ -#include -#include -#include +# include +# include +# include int main() { diff --git a/regression/cbmc-library/fesetround-04/main.c b/regression/cbmc-library/fesetround/main_04.c similarity index 100% rename from regression/cbmc-library/fesetround-04/main.c rename to regression/cbmc-library/fesetround/main_04.c diff --git a/regression/cbmc-library/fesetround-05/main.c b/regression/cbmc-library/fesetround/main_05.c similarity index 100% rename from regression/cbmc-library/fesetround-05/main.c rename to regression/cbmc-library/fesetround/main_05.c diff --git a/regression/cbmc-library/fesetround-06/main.c b/regression/cbmc-library/fesetround/main_06.c similarity index 100% rename from regression/cbmc-library/fesetround-06/main.c rename to regression/cbmc-library/fesetround/main_06.c diff --git a/regression/cbmc-library/fesetround-no-simp1-fix1/main.c b/regression/cbmc-library/fesetround/no-simp1-fix1.c similarity index 100% rename from regression/cbmc-library/fesetround-no-simp1-fix1/main.c rename to regression/cbmc-library/fesetround/no-simp1-fix1.c diff --git a/regression/cbmc-library/signbit-01/test.desc b/regression/cbmc-library/fesetround/no-simp1-fix1.desc similarity index 85% rename from regression/cbmc-library/signbit-01/test.desc rename to regression/cbmc-library/fesetround/no-simp1-fix1.desc index 4d2a93e6e26..039d0d3039c 100644 --- a/regression/cbmc-library/signbit-01/test.desc +++ b/regression/cbmc-library/fesetround/no-simp1-fix1.desc @@ -1,5 +1,5 @@ CORE -main.c +no-simp1-fix1.c --floatbv --no-simplify ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/fesetround-no-simp1-fix2/main.c b/regression/cbmc-library/fesetround/no-simp1-fix2.c similarity index 100% rename from regression/cbmc-library/fesetround-no-simp1-fix2/main.c rename to regression/cbmc-library/fesetround/no-simp1-fix2.c diff --git a/regression/cbmc-library/fesetround-no-simp1/test.desc b/regression/cbmc-library/fesetround/no-simp1-fix2.desc similarity index 88% rename from regression/cbmc-library/fesetround-no-simp1/test.desc rename to regression/cbmc-library/fesetround/no-simp1-fix2.desc index 20e0e91022a..750f0eebdf8 100644 --- a/regression/cbmc-library/fesetround-no-simp1/test.desc +++ b/regression/cbmc-library/fesetround/no-simp1-fix2.desc @@ -1,5 +1,5 @@ CORE -main.c +no-simp1-fix2.c --no-div-by-zero-check --floatbv --no-simplify ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/fesetround-no-simp1/main.c b/regression/cbmc-library/fesetround/no-simp1.c similarity index 100% rename from regression/cbmc-library/fesetround-no-simp1/main.c rename to regression/cbmc-library/fesetround/no-simp1.c diff --git a/regression/cbmc-library/fesetround-no-simp1-fix2/test.desc b/regression/cbmc-library/fesetround/no-simp1.desc similarity index 91% rename from regression/cbmc-library/fesetround-no-simp1-fix2/test.desc rename to regression/cbmc-library/fesetround/no-simp1.desc index 20e0e91022a..c9edeac8a88 100644 --- a/regression/cbmc-library/fesetround-no-simp1-fix2/test.desc +++ b/regression/cbmc-library/fesetround/no-simp1.desc @@ -1,5 +1,5 @@ CORE -main.c +no-simp1.c --no-div-by-zero-check --floatbv --no-simplify ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/isnan-01/test.desc b/regression/cbmc-library/fesetround/test_01.desc similarity index 89% rename from regression/cbmc-library/isnan-01/test.desc rename to regression/cbmc-library/fesetround/test_01.desc index b7d95a28215..13c8ca1afd4 100644 --- a/regression/cbmc-library/isnan-01/test.desc +++ b/regression/cbmc-library/fesetround/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --floatbv ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/fesetround-05/test.desc b/regression/cbmc-library/fesetround/test_02.desc similarity index 89% rename from regression/cbmc-library/fesetround-05/test.desc rename to regression/cbmc-library/fesetround/test_02.desc index b7d95a28215..6f11f6c551e 100644 --- a/regression/cbmc-library/fesetround-05/test.desc +++ b/regression/cbmc-library/fesetround/test_02.desc @@ -1,5 +1,5 @@ CORE -main.c +main_02.c --floatbv ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-02/memcpy3.desc b/regression/cbmc-library/fesetround/test_03.desc similarity index 88% rename from regression/cbmc-library/memcpy-02/memcpy3.desc rename to regression/cbmc-library/fesetround/test_03.desc index 97dac09582d..9e6e37bf58f 100644 --- a/regression/cbmc-library/memcpy-02/memcpy3.desc +++ b/regression/cbmc-library/fesetround/test_03.desc @@ -1,5 +1,5 @@ CORE -memcpy3.c +main_03.c ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/fesetround-04/test.desc b/regression/cbmc-library/fesetround/test_04.desc similarity index 89% rename from regression/cbmc-library/fesetround-04/test.desc rename to regression/cbmc-library/fesetround/test_04.desc index b7d95a28215..9c05506673a 100644 --- a/regression/cbmc-library/fesetround-04/test.desc +++ b/regression/cbmc-library/fesetround/test_04.desc @@ -1,5 +1,5 @@ CORE -main.c +main_04.c --floatbv ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/sin-01/test.desc b/regression/cbmc-library/fesetround/test_05.desc similarity index 89% rename from regression/cbmc-library/sin-01/test.desc rename to regression/cbmc-library/fesetround/test_05.desc index b7d95a28215..dfe433630e4 100644 --- a/regression/cbmc-library/sin-01/test.desc +++ b/regression/cbmc-library/fesetround/test_05.desc @@ -1,5 +1,5 @@ CORE -main.c +main_05.c --floatbv ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/trunc-01/test.desc b/regression/cbmc-library/fesetround/test_06.desc similarity index 88% rename from regression/cbmc-library/trunc-01/test.desc rename to regression/cbmc-library/fesetround/test_06.desc index 9efefbc7362..fa6d37c5cff 100644 --- a/regression/cbmc-library/trunc-01/test.desc +++ b/regression/cbmc-library/fesetround/test_06.desc @@ -1,5 +1,5 @@ CORE -main.c +main_06.c ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/fesetround-with-simp1/main.c b/regression/cbmc-library/fesetround/with-simp1.c similarity index 100% rename from regression/cbmc-library/fesetround-with-simp1/main.c rename to regression/cbmc-library/fesetround/with-simp1.c diff --git a/regression/cbmc-library/isinf-01/test.desc b/regression/cbmc-library/fesetround/with-simp1.desc similarity index 89% rename from regression/cbmc-library/isinf-01/test.desc rename to regression/cbmc-library/fesetround/with-simp1.desc index 544304c45ce..40e3b91977a 100644 --- a/regression/cbmc-library/isinf-01/test.desc +++ b/regression/cbmc-library/fesetround/with-simp1.desc @@ -1,5 +1,5 @@ CORE -main.c +with-simp1.c --no-div-by-zero-check --floatbv ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/fflush-01/main.c b/regression/cbmc-library/fflush/main.c similarity index 100% rename from regression/cbmc-library/fflush-01/main.c rename to regression/cbmc-library/fflush/main.c diff --git a/regression/cbmc-library/fflush-01/test.desc b/regression/cbmc-library/fflush/test.desc similarity index 100% rename from regression/cbmc-library/fflush-01/test.desc rename to regression/cbmc-library/fflush/test.desc diff --git a/regression/cbmc-library/fgetc-01/main.c b/regression/cbmc-library/fgetc/main.c similarity index 100% rename from regression/cbmc-library/fgetc-01/main.c rename to regression/cbmc-library/fgetc/main.c diff --git a/regression/cbmc-library/fgetc-01/test.desc b/regression/cbmc-library/fgetc/test.desc similarity index 100% rename from regression/cbmc-library/fgetc-01/test.desc rename to regression/cbmc-library/fgetc/test.desc diff --git a/regression/cbmc-library/fgets-01/__fgets_chk.desc b/regression/cbmc-library/fgets/__fgets_chk.desc similarity index 100% rename from regression/cbmc-library/fgets-01/__fgets_chk.desc rename to regression/cbmc-library/fgets/__fgets_chk.desc diff --git a/regression/cbmc-library/fgets-01/main.c b/regression/cbmc-library/fgets/main.c similarity index 100% rename from regression/cbmc-library/fgets-01/main.c rename to regression/cbmc-library/fgets/main.c diff --git a/regression/cbmc-library/fgets-01/test.desc b/regression/cbmc-library/fgets/test.desc similarity index 100% rename from regression/cbmc-library/fgets-01/test.desc rename to regression/cbmc-library/fgets/test.desc diff --git a/regression/cbmc-library/fileno-01/main.c b/regression/cbmc-library/fileno/main.c similarity index 100% rename from regression/cbmc-library/fileno-01/main.c rename to regression/cbmc-library/fileno/main.c diff --git a/regression/cbmc-library/fileno-01/test.desc b/regression/cbmc-library/fileno/test.desc similarity index 100% rename from regression/cbmc-library/fileno-01/test.desc rename to regression/cbmc-library/fileno/test.desc diff --git a/regression/cbmc-library/floor-01/main.c b/regression/cbmc-library/floor/main.c similarity index 100% rename from regression/cbmc-library/floor-01/main.c rename to regression/cbmc-library/floor/main.c diff --git a/regression/cbmc-library/equality_through_struct5/test.desc b/regression/cbmc-library/floor/test.desc similarity index 100% rename from regression/cbmc-library/equality_through_struct5/test.desc rename to regression/cbmc-library/floor/test.desc diff --git a/regression/cbmc-library/floorf-01/main.c b/regression/cbmc-library/floorf/main.c similarity index 100% rename from regression/cbmc-library/floorf-01/main.c rename to regression/cbmc-library/floorf/main.c diff --git a/regression/cbmc-library/fesetround-03/test.desc b/regression/cbmc-library/floorf/test.desc similarity index 100% rename from regression/cbmc-library/fesetround-03/test.desc rename to regression/cbmc-library/floorf/test.desc diff --git a/regression/cbmc-library/floorl-01/main.c b/regression/cbmc-library/floorl/main.c similarity index 100% rename from regression/cbmc-library/floorl-01/main.c rename to regression/cbmc-library/floorl/main.c diff --git a/regression/cbmc-library/fesetround-06/test.desc b/regression/cbmc-library/floorl/test.desc similarity index 100% rename from regression/cbmc-library/fesetround-06/test.desc rename to regression/cbmc-library/floorl/test.desc diff --git a/regression/cbmc-library/fma-01/main.c b/regression/cbmc-library/fma/main.c similarity index 100% rename from regression/cbmc-library/fma-01/main.c rename to regression/cbmc-library/fma/main.c diff --git a/regression/cbmc-library/fma-01/test.desc b/regression/cbmc-library/fma/test.desc similarity index 100% rename from regression/cbmc-library/fma-01/test.desc rename to regression/cbmc-library/fma/test.desc diff --git a/regression/cbmc-library/fmaf-01/main.c b/regression/cbmc-library/fmaf/main.c similarity index 100% rename from regression/cbmc-library/fmaf-01/main.c rename to regression/cbmc-library/fmaf/main.c diff --git a/regression/cbmc-library/fmaf-01/test.desc b/regression/cbmc-library/fmaf/test.desc similarity index 100% rename from regression/cbmc-library/fmaf-01/test.desc rename to regression/cbmc-library/fmaf/test.desc diff --git a/regression/cbmc-library/fmal-01/main.c b/regression/cbmc-library/fmal/main.c similarity index 100% rename from regression/cbmc-library/fmal-01/main.c rename to regression/cbmc-library/fmal/main.c diff --git a/regression/cbmc-library/fmal-01/test.desc b/regression/cbmc-library/fmal/test.desc similarity index 100% rename from regression/cbmc-library/fmal-01/test.desc rename to regression/cbmc-library/fmal/test.desc diff --git a/regression/cbmc-library/fmax-01/main.c b/regression/cbmc-library/fmax/main.c similarity index 100% rename from regression/cbmc-library/fmax-01/main.c rename to regression/cbmc-library/fmax/main.c diff --git a/regression/cbmc-library/fmax-01/test.desc b/regression/cbmc-library/fmax/test.desc similarity index 100% rename from regression/cbmc-library/fmax-01/test.desc rename to regression/cbmc-library/fmax/test.desc diff --git a/regression/cbmc-library/fmaxf-01/main.c b/regression/cbmc-library/fmaxf/main.c similarity index 100% rename from regression/cbmc-library/fmaxf-01/main.c rename to regression/cbmc-library/fmaxf/main.c diff --git a/regression/cbmc-library/fmaxf-01/test.desc b/regression/cbmc-library/fmaxf/test.desc similarity index 100% rename from regression/cbmc-library/fmaxf-01/test.desc rename to regression/cbmc-library/fmaxf/test.desc diff --git a/regression/cbmc-library/fmaxl-01/main.c b/regression/cbmc-library/fmaxl/main.c similarity index 100% rename from regression/cbmc-library/fmaxl-01/main.c rename to regression/cbmc-library/fmaxl/main.c diff --git a/regression/cbmc-library/fmaxl-01/test.desc b/regression/cbmc-library/fmaxl/test.desc similarity index 100% rename from regression/cbmc-library/fmaxl-01/test.desc rename to regression/cbmc-library/fmaxl/test.desc diff --git a/regression/cbmc-library/fmin-01/main.c b/regression/cbmc-library/fmin/main.c similarity index 100% rename from regression/cbmc-library/fmin-01/main.c rename to regression/cbmc-library/fmin/main.c diff --git a/regression/cbmc-library/fmin-01/test.desc b/regression/cbmc-library/fmin/test.desc similarity index 100% rename from regression/cbmc-library/fmin-01/test.desc rename to regression/cbmc-library/fmin/test.desc diff --git a/regression/cbmc-library/fminf-01/main.c b/regression/cbmc-library/fminf/main.c similarity index 100% rename from regression/cbmc-library/fminf-01/main.c rename to regression/cbmc-library/fminf/main.c diff --git a/regression/cbmc-library/fminf-01/test.desc b/regression/cbmc-library/fminf/test.desc similarity index 100% rename from regression/cbmc-library/fminf-01/test.desc rename to regression/cbmc-library/fminf/test.desc diff --git a/regression/cbmc-library/fminl-01/main.c b/regression/cbmc-library/fminl/main.c similarity index 100% rename from regression/cbmc-library/fminl-01/main.c rename to regression/cbmc-library/fminl/main.c diff --git a/regression/cbmc-library/fminl-01/test.desc b/regression/cbmc-library/fminl/test.desc similarity index 100% rename from regression/cbmc-library/fminl-01/test.desc rename to regression/cbmc-library/fminl/test.desc diff --git a/regression/cbmc-library/fmod-01/main.c b/regression/cbmc-library/fmod/main.c similarity index 100% rename from regression/cbmc-library/fmod-01/main.c rename to regression/cbmc-library/fmod/main.c diff --git a/regression/cbmc-library/fmod-01/test.desc b/regression/cbmc-library/fmod/test.desc similarity index 100% rename from regression/cbmc-library/fmod-01/test.desc rename to regression/cbmc-library/fmod/test.desc diff --git a/regression/cbmc-library/fmodf-01/main.c b/regression/cbmc-library/fmodf/main.c similarity index 100% rename from regression/cbmc-library/fmodf-01/main.c rename to regression/cbmc-library/fmodf/main.c diff --git a/regression/cbmc-library/fmodf-01/test.desc b/regression/cbmc-library/fmodf/test.desc similarity index 100% rename from regression/cbmc-library/fmodf-01/test.desc rename to regression/cbmc-library/fmodf/test.desc diff --git a/regression/cbmc-library/fmodl-01/main.c b/regression/cbmc-library/fmodl/main.c similarity index 100% rename from regression/cbmc-library/fmodl-01/main.c rename to regression/cbmc-library/fmodl/main.c diff --git a/regression/cbmc-library/fmodl-01/test.desc b/regression/cbmc-library/fmodl/test.desc similarity index 100% rename from regression/cbmc-library/fmodl-01/test.desc rename to regression/cbmc-library/fmodl/test.desc diff --git a/regression/cbmc-library/fopen-01/main.c b/regression/cbmc-library/fopen/main.c similarity index 100% rename from regression/cbmc-library/fopen-01/main.c rename to regression/cbmc-library/fopen/main.c diff --git a/regression/cbmc-library/fopen-01/test.desc b/regression/cbmc-library/fopen/test.desc similarity index 100% rename from regression/cbmc-library/fopen-01/test.desc rename to regression/cbmc-library/fopen/test.desc diff --git a/regression/cbmc-library/fprintf-01/__fprintf_chk.desc b/regression/cbmc-library/fprintf/__fprintf_chk.desc similarity index 100% rename from regression/cbmc-library/fprintf-01/__fprintf_chk.desc rename to regression/cbmc-library/fprintf/__fprintf_chk.desc diff --git a/regression/cbmc-library/fprintf-01/main.c b/regression/cbmc-library/fprintf/main.c similarity index 100% rename from regression/cbmc-library/fprintf-01/main.c rename to regression/cbmc-library/fprintf/main.c diff --git a/regression/cbmc-library/fprintf-01/test.desc b/regression/cbmc-library/fprintf/test.desc similarity index 100% rename from regression/cbmc-library/fprintf-01/test.desc rename to regression/cbmc-library/fprintf/test.desc diff --git a/regression/cbmc-library/fpurge-01/main.c b/regression/cbmc-library/fpurge/main.c similarity index 100% rename from regression/cbmc-library/fpurge-01/main.c rename to regression/cbmc-library/fpurge/main.c diff --git a/regression/cbmc-library/fpurge-01/test.desc b/regression/cbmc-library/fpurge/test.desc similarity index 100% rename from regression/cbmc-library/fpurge-01/test.desc rename to regression/cbmc-library/fpurge/test.desc diff --git a/regression/cbmc-library/fputs-01/main.c b/regression/cbmc-library/fputs/main.c similarity index 100% rename from regression/cbmc-library/fputs-01/main.c rename to regression/cbmc-library/fputs/main.c diff --git a/regression/cbmc-library/fputs-01/test.desc b/regression/cbmc-library/fputs/test.desc similarity index 100% rename from regression/cbmc-library/fputs-01/test.desc rename to regression/cbmc-library/fputs/test.desc diff --git a/regression/cbmc-library/fread-01/__fread_chk.desc b/regression/cbmc-library/fread/__fread_chk.desc similarity index 100% rename from regression/cbmc-library/fread-01/__fread_chk.desc rename to regression/cbmc-library/fread/__fread_chk.desc diff --git a/regression/cbmc-library/fread-01/main.c b/regression/cbmc-library/fread/main.c similarity index 100% rename from regression/cbmc-library/fread-01/main.c rename to regression/cbmc-library/fread/main.c diff --git a/regression/cbmc-library/fread-01/test.desc b/regression/cbmc-library/fread/test.desc similarity index 100% rename from regression/cbmc-library/fread-01/test.desc rename to regression/cbmc-library/fread/test.desc diff --git a/regression/cbmc-library/free-01/main.c b/regression/cbmc-library/free/main.c similarity index 100% rename from regression/cbmc-library/free-01/main.c rename to regression/cbmc-library/free/main.c diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free/test.desc similarity index 100% rename from regression/cbmc-library/free-01/test.desc rename to regression/cbmc-library/free/test.desc diff --git a/regression/cbmc-library/freopen-01/main.c b/regression/cbmc-library/freopen/main.c similarity index 100% rename from regression/cbmc-library/freopen-01/main.c rename to regression/cbmc-library/freopen/main.c diff --git a/regression/cbmc-library/freopen-01/test.desc b/regression/cbmc-library/freopen/test.desc similarity index 100% rename from regression/cbmc-library/freopen-01/test.desc rename to regression/cbmc-library/freopen/test.desc diff --git a/regression/cbmc-library/fscanf-01/main.c b/regression/cbmc-library/fscanf/main.c similarity index 100% rename from regression/cbmc-library/fscanf-01/main.c rename to regression/cbmc-library/fscanf/main.c diff --git a/regression/cbmc-library/fscanf-01/test.desc b/regression/cbmc-library/fscanf/test.desc similarity index 100% rename from regression/cbmc-library/fscanf-01/test.desc rename to regression/cbmc-library/fscanf/test.desc diff --git a/regression/cbmc-library/fseek-01/main.c b/regression/cbmc-library/fseek/main.c similarity index 100% rename from regression/cbmc-library/fseek-01/main.c rename to regression/cbmc-library/fseek/main.c diff --git a/regression/cbmc-library/fseek-01/test.desc b/regression/cbmc-library/fseek/test.desc similarity index 100% rename from regression/cbmc-library/fseek-01/test.desc rename to regression/cbmc-library/fseek/test.desc diff --git a/regression/cbmc-library/ftell-01/main.c b/regression/cbmc-library/ftell/main.c similarity index 100% rename from regression/cbmc-library/ftell-01/main.c rename to regression/cbmc-library/ftell/main.c diff --git a/regression/cbmc-library/ftell-01/test.desc b/regression/cbmc-library/ftell/test.desc similarity index 100% rename from regression/cbmc-library/ftell-01/test.desc rename to regression/cbmc-library/ftell/test.desc diff --git a/regression/cbmc-library/fwrite-01/main.c b/regression/cbmc-library/fwrite/main.c similarity index 100% rename from regression/cbmc-library/fwrite-01/main.c rename to regression/cbmc-library/fwrite/main.c diff --git a/regression/cbmc-library/fwrite-01/test.desc b/regression/cbmc-library/fwrite/test.desc similarity index 100% rename from regression/cbmc-library/fwrite-01/test.desc rename to regression/cbmc-library/fwrite/test.desc diff --git a/regression/cbmc-library/getc-01/main.c b/regression/cbmc-library/getc/main.c similarity index 100% rename from regression/cbmc-library/getc-01/main.c rename to regression/cbmc-library/getc/main.c diff --git a/regression/cbmc-library/getc-01/test.desc b/regression/cbmc-library/getc/test.desc similarity index 100% rename from regression/cbmc-library/getc-01/test.desc rename to regression/cbmc-library/getc/test.desc diff --git a/regression/cbmc-library/getchar-01/main.c b/regression/cbmc-library/getchar/main.c similarity index 100% rename from regression/cbmc-library/getchar-01/main.c rename to regression/cbmc-library/getchar/main.c diff --git a/regression/cbmc-library/getchar-01/test.desc b/regression/cbmc-library/getchar/test.desc similarity index 100% rename from regression/cbmc-library/getchar-01/test.desc rename to regression/cbmc-library/getchar/test.desc diff --git a/regression/cbmc-library/getenv-01/main.c b/regression/cbmc-library/getenv/main.c similarity index 100% rename from regression/cbmc-library/getenv-01/main.c rename to regression/cbmc-library/getenv/main.c diff --git a/regression/cbmc-library/getenv-01/test.desc b/regression/cbmc-library/getenv/test.desc similarity index 100% rename from regression/cbmc-library/getenv-01/test.desc rename to regression/cbmc-library/getenv/test.desc diff --git a/regression/cbmc-library/gethostbyaddr-01/main.c b/regression/cbmc-library/gethostbyaddr/main.c similarity index 100% rename from regression/cbmc-library/gethostbyaddr-01/main.c rename to regression/cbmc-library/gethostbyaddr/main.c diff --git a/regression/cbmc-library/gethostbyaddr-01/test.desc b/regression/cbmc-library/gethostbyaddr/test.desc similarity index 100% rename from regression/cbmc-library/gethostbyaddr-01/test.desc rename to regression/cbmc-library/gethostbyaddr/test.desc diff --git a/regression/cbmc-library/gethostbyname-01/main.c b/regression/cbmc-library/gethostbyname/main.c similarity index 100% rename from regression/cbmc-library/gethostbyname-01/main.c rename to regression/cbmc-library/gethostbyname/main.c diff --git a/regression/cbmc-library/gethostbyname-01/test.desc b/regression/cbmc-library/gethostbyname/test.desc similarity index 100% rename from regression/cbmc-library/gethostbyname-01/test.desc rename to regression/cbmc-library/gethostbyname/test.desc diff --git a/regression/cbmc-library/gethostent-01/main.c b/regression/cbmc-library/gethostent/main.c similarity index 100% rename from regression/cbmc-library/gethostent-01/main.c rename to regression/cbmc-library/gethostent/main.c diff --git a/regression/cbmc-library/gethostent-01/test.desc b/regression/cbmc-library/gethostent/test.desc similarity index 100% rename from regression/cbmc-library/gethostent-01/test.desc rename to regression/cbmc-library/gethostent/test.desc diff --git a/regression/cbmc-library/getopt-01/main.c b/regression/cbmc-library/getopt/main.c similarity index 100% rename from regression/cbmc-library/getopt-01/main.c rename to regression/cbmc-library/getopt/main.c diff --git a/regression/cbmc-library/getopt-01/test.desc b/regression/cbmc-library/getopt/test.desc similarity index 100% rename from regression/cbmc-library/getopt-01/test.desc rename to regression/cbmc-library/getopt/test.desc diff --git a/regression/cbmc-library/getopt_long-01/main.c b/regression/cbmc-library/getopt_long/main.c similarity index 100% rename from regression/cbmc-library/getopt_long-01/main.c rename to regression/cbmc-library/getopt_long/main.c diff --git a/regression/cbmc-library/getopt_long-01/test.desc b/regression/cbmc-library/getopt_long/test.desc similarity index 100% rename from regression/cbmc-library/getopt_long-01/test.desc rename to regression/cbmc-library/getopt_long/test.desc diff --git a/regression/cbmc-library/getpwnam-01/main.c b/regression/cbmc-library/getpwnam/main.c similarity index 100% rename from regression/cbmc-library/getpwnam-01/main.c rename to regression/cbmc-library/getpwnam/main.c diff --git a/regression/cbmc-library/getpwnam-01/test.desc b/regression/cbmc-library/getpwnam/test.desc similarity index 100% rename from regression/cbmc-library/getpwnam-01/test.desc rename to regression/cbmc-library/getpwnam/test.desc diff --git a/regression/cbmc-library/getpwuid-01/main.c b/regression/cbmc-library/getpwuid/main.c similarity index 100% rename from regression/cbmc-library/getpwuid-01/main.c rename to regression/cbmc-library/getpwuid/main.c diff --git a/regression/cbmc-library/getpwuid-01/test.desc b/regression/cbmc-library/getpwuid/test.desc similarity index 100% rename from regression/cbmc-library/getpwuid-01/test.desc rename to regression/cbmc-library/getpwuid/test.desc diff --git a/regression/cbmc-library/getrandom-01/main.c b/regression/cbmc-library/getrandom/main.c similarity index 94% rename from regression/cbmc-library/getrandom-01/main.c rename to regression/cbmc-library/getrandom/main.c index 9325690b789..836612d47f3 100644 --- a/regression/cbmc-library/getrandom-01/main.c +++ b/regression/cbmc-library/getrandom/main.c @@ -1,4 +1,4 @@ -# include +#include #if defined(__GLIBC__) && \ (__GLIBC__ > 2 || (__GLIBC__ == 2 && __GLIBC_MINOR__ >= 25)) diff --git a/regression/cbmc-library/getrandom-01/test.desc b/regression/cbmc-library/getrandom/test.desc similarity index 100% rename from regression/cbmc-library/getrandom-01/test.desc rename to regression/cbmc-library/getrandom/test.desc diff --git a/regression/cbmc-library/getw-01/main.c b/regression/cbmc-library/getw/main.c similarity index 100% rename from regression/cbmc-library/getw-01/main.c rename to regression/cbmc-library/getw/main.c diff --git a/regression/cbmc-library/getw-01/test.desc b/regression/cbmc-library/getw/test.desc similarity index 100% rename from regression/cbmc-library/getw-01/test.desc rename to regression/cbmc-library/getw/test.desc diff --git a/regression/cbmc-library/gmtime-01/main.c b/regression/cbmc-library/gmtime/main.c similarity index 100% rename from regression/cbmc-library/gmtime-01/main.c rename to regression/cbmc-library/gmtime/main.c diff --git a/regression/cbmc-library/gmtime-01/test.desc b/regression/cbmc-library/gmtime/test.desc similarity index 100% rename from regression/cbmc-library/gmtime-01/test.desc rename to regression/cbmc-library/gmtime/test.desc diff --git a/regression/cbmc-library/gmtime_r-01/main.c b/regression/cbmc-library/gmtime_r/main.c similarity index 100% rename from regression/cbmc-library/gmtime_r-01/main.c rename to regression/cbmc-library/gmtime_r/main.c diff --git a/regression/cbmc-library/gmtime_r-01/test.desc b/regression/cbmc-library/gmtime_r/test.desc similarity index 100% rename from regression/cbmc-library/gmtime_r-01/test.desc rename to regression/cbmc-library/gmtime_r/test.desc diff --git a/regression/cbmc-library/htonl-01/main.c b/regression/cbmc-library/htonl-01/main.c deleted file mode 100644 index 4e582d599c7..00000000000 --- a/regression/cbmc-library/htonl-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - htonl(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/inet_endian1/main.c b/regression/cbmc-library/htonl/main.c similarity index 78% rename from regression/cbmc-library/inet_endian1/main.c rename to regression/cbmc-library/htonl/main.c index 4178ecff4a8..ffe2008c64f 100644 --- a/regression/cbmc-library/inet_endian1/main.c +++ b/regression/cbmc-library/htonl/main.c @@ -1,6 +1,7 @@ #ifndef _WIN32 -#include -#include +# include + +# include int main() { diff --git a/regression/cbmc-library/floor-01/test.desc b/regression/cbmc-library/htonl/test.desc similarity index 100% rename from regression/cbmc-library/floor-01/test.desc rename to regression/cbmc-library/htonl/test.desc diff --git a/regression/cbmc-library/htons-01/main.c b/regression/cbmc-library/htons/main.c similarity index 100% rename from regression/cbmc-library/htons-01/main.c rename to regression/cbmc-library/htons/main.c diff --git a/regression/cbmc-library/htonl-01/test.desc b/regression/cbmc-library/htons/test.desc similarity index 100% rename from regression/cbmc-library/htonl-01/test.desc rename to regression/cbmc-library/htons/test.desc diff --git a/regression/cbmc-library/imaxabs-01/main.c b/regression/cbmc-library/imaxabs/main.c similarity index 100% rename from regression/cbmc-library/imaxabs-01/main.c rename to regression/cbmc-library/imaxabs/main.c diff --git a/regression/cbmc-library/imaxabs-01/test.desc b/regression/cbmc-library/imaxabs/test.desc similarity index 100% rename from regression/cbmc-library/imaxabs-01/test.desc rename to regression/cbmc-library/imaxabs/test.desc diff --git a/regression/cbmc-library/inet_addr-01/main.c b/regression/cbmc-library/inet_addr/main.c similarity index 100% rename from regression/cbmc-library/inet_addr-01/main.c rename to regression/cbmc-library/inet_addr/main.c diff --git a/regression/cbmc-library/htons-01/test.desc b/regression/cbmc-library/inet_addr/test.desc similarity index 100% rename from regression/cbmc-library/htons-01/test.desc rename to regression/cbmc-library/inet_addr/test.desc diff --git a/regression/cbmc-library/inet_aton-01/main.c b/regression/cbmc-library/inet_aton/main.c similarity index 100% rename from regression/cbmc-library/inet_aton-01/main.c rename to regression/cbmc-library/inet_aton/main.c diff --git a/regression/cbmc-library/inet_addr-01/test.desc b/regression/cbmc-library/inet_aton/test.desc similarity index 100% rename from regression/cbmc-library/inet_addr-01/test.desc rename to regression/cbmc-library/inet_aton/test.desc diff --git a/regression/cbmc-library/inet_network-01/main.c b/regression/cbmc-library/inet_network/main.c similarity index 100% rename from regression/cbmc-library/inet_network-01/main.c rename to regression/cbmc-library/inet_network/main.c diff --git a/regression/cbmc-library/inet_aton-01/test.desc b/regression/cbmc-library/inet_network/test.desc similarity index 100% rename from regression/cbmc-library/inet_aton-01/test.desc rename to regression/cbmc-library/inet_network/test.desc diff --git a/regression/cbmc-library/inet_ntoa-01/main.c b/regression/cbmc-library/inet_ntoa/main.c similarity index 100% rename from regression/cbmc-library/inet_ntoa-01/main.c rename to regression/cbmc-library/inet_ntoa/main.c diff --git a/regression/cbmc-library/inet_ntoa-01/test.desc b/regression/cbmc-library/inet_ntoa/test.desc similarity index 100% rename from regression/cbmc-library/inet_ntoa-01/test.desc rename to regression/cbmc-library/inet_ntoa/test.desc diff --git a/regression/cbmc-library/isalnum-01/main.c b/regression/cbmc-library/isalnum/main.c similarity index 100% rename from regression/cbmc-library/isalnum-01/main.c rename to regression/cbmc-library/isalnum/main.c diff --git a/regression/cbmc-library/inet_network-01/test.desc b/regression/cbmc-library/isalnum/test.desc similarity index 100% rename from regression/cbmc-library/inet_network-01/test.desc rename to regression/cbmc-library/isalnum/test.desc diff --git a/regression/cbmc-library/isalpha-01/main.c b/regression/cbmc-library/isalpha/main.c similarity index 100% rename from regression/cbmc-library/isalpha-01/main.c rename to regression/cbmc-library/isalpha/main.c diff --git a/regression/cbmc-library/isalnum-01/test.desc b/regression/cbmc-library/isalpha/test.desc similarity index 100% rename from regression/cbmc-library/isalnum-01/test.desc rename to regression/cbmc-library/isalpha/test.desc diff --git a/regression/cbmc-library/isblank-01/main.c b/regression/cbmc-library/isblank/main.c similarity index 100% rename from regression/cbmc-library/isblank-01/main.c rename to regression/cbmc-library/isblank/main.c diff --git a/regression/cbmc-library/isalpha-01/test.desc b/regression/cbmc-library/isblank/test.desc similarity index 100% rename from regression/cbmc-library/isalpha-01/test.desc rename to regression/cbmc-library/isblank/test.desc diff --git a/regression/cbmc-library/iscntrl-01/main.c b/regression/cbmc-library/iscntrl/main.c similarity index 100% rename from regression/cbmc-library/iscntrl-01/main.c rename to regression/cbmc-library/iscntrl/main.c diff --git a/regression/cbmc-library/isblank-01/test.desc b/regression/cbmc-library/iscntrl/test.desc similarity index 100% rename from regression/cbmc-library/isblank-01/test.desc rename to regression/cbmc-library/iscntrl/test.desc diff --git a/regression/cbmc-library/isdigit-01/main.c b/regression/cbmc-library/isdigit/main.c similarity index 100% rename from regression/cbmc-library/isdigit-01/main.c rename to regression/cbmc-library/isdigit/main.c diff --git a/regression/cbmc-library/iscntrl-01/test.desc b/regression/cbmc-library/isdigit/test.desc similarity index 100% rename from regression/cbmc-library/iscntrl-01/test.desc rename to regression/cbmc-library/isdigit/test.desc diff --git a/regression/cbmc-library/isfinite-01/main.c b/regression/cbmc-library/isfinite/main.c similarity index 100% rename from regression/cbmc-library/isfinite-01/main.c rename to regression/cbmc-library/isfinite/main.c diff --git a/regression/cbmc-library/isdigit-01/test.desc b/regression/cbmc-library/isfinite/test.desc similarity index 100% rename from regression/cbmc-library/isdigit-01/test.desc rename to regression/cbmc-library/isfinite/test.desc diff --git a/regression/cbmc-library/isgraph-01/main.c b/regression/cbmc-library/isgraph/main.c similarity index 100% rename from regression/cbmc-library/isgraph-01/main.c rename to regression/cbmc-library/isgraph/main.c diff --git a/regression/cbmc-library/isfinite-01/test.desc b/regression/cbmc-library/isgraph/test.desc similarity index 100% rename from regression/cbmc-library/isfinite-01/test.desc rename to regression/cbmc-library/isgraph/test.desc diff --git a/regression/cbmc-library/isinf-01/main.c b/regression/cbmc-library/isinf/main.c similarity index 100% rename from regression/cbmc-library/isinf-01/main.c rename to regression/cbmc-library/isinf/main.c diff --git a/regression/cbmc-library/fesetround-with-simp1/test.desc b/regression/cbmc-library/isinf/test.desc similarity index 100% rename from regression/cbmc-library/fesetround-with-simp1/test.desc rename to regression/cbmc-library/isinf/test.desc diff --git a/regression/cbmc-library/isinff-01/main.c b/regression/cbmc-library/isinff/main.c similarity index 100% rename from regression/cbmc-library/isinff-01/main.c rename to regression/cbmc-library/isinff/main.c diff --git a/regression/cbmc-library/isgraph-01/test.desc b/regression/cbmc-library/isinff/test.desc similarity index 100% rename from regression/cbmc-library/isgraph-01/test.desc rename to regression/cbmc-library/isinff/test.desc diff --git a/regression/cbmc-library/isinfl-01/main.c b/regression/cbmc-library/isinfl/main.c similarity index 100% rename from regression/cbmc-library/isinfl-01/main.c rename to regression/cbmc-library/isinfl/main.c diff --git a/regression/cbmc-library/isinff-01/test.desc b/regression/cbmc-library/isinfl/test.desc similarity index 100% rename from regression/cbmc-library/isinff-01/test.desc rename to regression/cbmc-library/isinfl/test.desc diff --git a/regression/cbmc-library/islower-01/main.c b/regression/cbmc-library/islower/main.c similarity index 100% rename from regression/cbmc-library/islower-01/main.c rename to regression/cbmc-library/islower/main.c diff --git a/regression/cbmc-library/isinfl-01/test.desc b/regression/cbmc-library/islower/test.desc similarity index 100% rename from regression/cbmc-library/isinfl-01/test.desc rename to regression/cbmc-library/islower/test.desc diff --git a/regression/cbmc-library/isnan-01/main.c b/regression/cbmc-library/isnan/main.c similarity index 100% rename from regression/cbmc-library/isnan-01/main.c rename to regression/cbmc-library/isnan/main.c diff --git a/regression/cbmc-library/fesetround-01/test.desc b/regression/cbmc-library/isnan/test.desc similarity index 100% rename from regression/cbmc-library/fesetround-01/test.desc rename to regression/cbmc-library/isnan/test.desc diff --git a/regression/cbmc-library/isnanf-01/main.c b/regression/cbmc-library/isnanf/main.c similarity index 100% rename from regression/cbmc-library/isnanf-01/main.c rename to regression/cbmc-library/isnanf/main.c diff --git a/regression/cbmc-library/islower-01/test.desc b/regression/cbmc-library/isnanf/test.desc similarity index 100% rename from regression/cbmc-library/islower-01/test.desc rename to regression/cbmc-library/isnanf/test.desc diff --git a/regression/cbmc-library/isnanl-01/main.c b/regression/cbmc-library/isnanl/main.c similarity index 100% rename from regression/cbmc-library/isnanl-01/main.c rename to regression/cbmc-library/isnanl/main.c diff --git a/regression/cbmc-library/isnanf-01/test.desc b/regression/cbmc-library/isnanl/test.desc similarity index 100% rename from regression/cbmc-library/isnanf-01/test.desc rename to regression/cbmc-library/isnanl/test.desc diff --git a/regression/cbmc-library/isnormal-01/main.c b/regression/cbmc-library/isnormal/main.c similarity index 100% rename from regression/cbmc-library/isnormal-01/main.c rename to regression/cbmc-library/isnormal/main.c diff --git a/regression/cbmc-library/isnanl-01/test.desc b/regression/cbmc-library/isnormal/test.desc similarity index 100% rename from regression/cbmc-library/isnanl-01/test.desc rename to regression/cbmc-library/isnormal/test.desc diff --git a/regression/cbmc-library/isprint-01/main.c b/regression/cbmc-library/isprint/main.c similarity index 100% rename from regression/cbmc-library/isprint-01/main.c rename to regression/cbmc-library/isprint/main.c diff --git a/regression/cbmc-library/isnormal-01/test.desc b/regression/cbmc-library/isprint/test.desc similarity index 100% rename from regression/cbmc-library/isnormal-01/test.desc rename to regression/cbmc-library/isprint/test.desc diff --git a/regression/cbmc-library/ispunct-01/main.c b/regression/cbmc-library/ispunct/main.c similarity index 100% rename from regression/cbmc-library/ispunct-01/main.c rename to regression/cbmc-library/ispunct/main.c diff --git a/regression/cbmc-library/isprint-01/test.desc b/regression/cbmc-library/ispunct/test.desc similarity index 100% rename from regression/cbmc-library/isprint-01/test.desc rename to regression/cbmc-library/ispunct/test.desc diff --git a/regression/cbmc-library/isspace-01/main.c b/regression/cbmc-library/isspace/main.c similarity index 100% rename from regression/cbmc-library/isspace-01/main.c rename to regression/cbmc-library/isspace/main.c diff --git a/regression/cbmc-library/ispunct-01/test.desc b/regression/cbmc-library/isspace/test.desc similarity index 100% rename from regression/cbmc-library/ispunct-01/test.desc rename to regression/cbmc-library/isspace/test.desc diff --git a/regression/cbmc-library/isupper-01/main.c b/regression/cbmc-library/isupper/main.c similarity index 100% rename from regression/cbmc-library/isupper-01/main.c rename to regression/cbmc-library/isupper/main.c diff --git a/regression/cbmc-library/isspace-01/test.desc b/regression/cbmc-library/isupper/test.desc similarity index 100% rename from regression/cbmc-library/isspace-01/test.desc rename to regression/cbmc-library/isupper/test.desc diff --git a/regression/cbmc-library/isxdigit-01/main.c b/regression/cbmc-library/isxdigit/main.c similarity index 100% rename from regression/cbmc-library/isxdigit-01/main.c rename to regression/cbmc-library/isxdigit/main.c diff --git a/regression/cbmc-library/isupper-01/test.desc b/regression/cbmc-library/isxdigit/test.desc similarity index 100% rename from regression/cbmc-library/isupper-01/test.desc rename to regression/cbmc-library/isxdigit/test.desc diff --git a/regression/cbmc-library/kill-01/main.c b/regression/cbmc-library/kill/main.c similarity index 100% rename from regression/cbmc-library/kill-01/main.c rename to regression/cbmc-library/kill/main.c diff --git a/regression/cbmc-library/isxdigit-01/test.desc b/regression/cbmc-library/kill/test.desc similarity index 100% rename from regression/cbmc-library/isxdigit-01/test.desc rename to regression/cbmc-library/kill/test.desc diff --git a/regression/cbmc-library/labs-01/main.c b/regression/cbmc-library/labs/main.c similarity index 100% rename from regression/cbmc-library/labs-01/main.c rename to regression/cbmc-library/labs/main.c diff --git a/regression/cbmc-library/kill-01/test.desc b/regression/cbmc-library/labs/test.desc similarity index 100% rename from regression/cbmc-library/kill-01/test.desc rename to regression/cbmc-library/labs/test.desc diff --git a/regression/cbmc-library/llabs-01/main.c b/regression/cbmc-library/llabs/main.c similarity index 99% rename from regression/cbmc-library/llabs-01/main.c rename to regression/cbmc-library/llabs/main.c index 84822acaefe..3a84918af84 100644 --- a/regression/cbmc-library/llabs-01/main.c +++ b/regression/cbmc-library/llabs/main.c @@ -1,7 +1,6 @@ #include -#include - #include +#include int main() { diff --git a/regression/cbmc-library/llabs-01/test.desc b/regression/cbmc-library/llabs/test.desc similarity index 100% rename from regression/cbmc-library/llabs-01/test.desc rename to regression/cbmc-library/llabs/test.desc diff --git a/regression/cbmc-library/llrint-01/main.c b/regression/cbmc-library/llrint/main.c similarity index 100% rename from regression/cbmc-library/llrint-01/main.c rename to regression/cbmc-library/llrint/main.c diff --git a/regression/cbmc-library/labs-01/test.desc b/regression/cbmc-library/llrint/test.desc similarity index 100% rename from regression/cbmc-library/labs-01/test.desc rename to regression/cbmc-library/llrint/test.desc diff --git a/regression/cbmc-library/llrintf-01/main.c b/regression/cbmc-library/llrintf/main.c similarity index 100% rename from regression/cbmc-library/llrintf-01/main.c rename to regression/cbmc-library/llrintf/main.c diff --git a/regression/cbmc-library/llrint-01/test.desc b/regression/cbmc-library/llrintf/test.desc similarity index 100% rename from regression/cbmc-library/llrint-01/test.desc rename to regression/cbmc-library/llrintf/test.desc diff --git a/regression/cbmc-library/llrintl-01/main.c b/regression/cbmc-library/llrintl/main.c similarity index 100% rename from regression/cbmc-library/llrintl-01/main.c rename to regression/cbmc-library/llrintl/main.c diff --git a/regression/cbmc-library/llrintf-01/test.desc b/regression/cbmc-library/llrintl/test.desc similarity index 100% rename from regression/cbmc-library/llrintf-01/test.desc rename to regression/cbmc-library/llrintl/test.desc diff --git a/regression/cbmc-library/llround-01/main.c b/regression/cbmc-library/llround/main.c similarity index 100% rename from regression/cbmc-library/llround-01/main.c rename to regression/cbmc-library/llround/main.c diff --git a/regression/cbmc-library/llrintl-01/test.desc b/regression/cbmc-library/llround/test.desc similarity index 100% rename from regression/cbmc-library/llrintl-01/test.desc rename to regression/cbmc-library/llround/test.desc diff --git a/regression/cbmc-library/llroundf-01/main.c b/regression/cbmc-library/llroundf/main.c similarity index 100% rename from regression/cbmc-library/llroundf-01/main.c rename to regression/cbmc-library/llroundf/main.c diff --git a/regression/cbmc-library/llround-01/test.desc b/regression/cbmc-library/llroundf/test.desc similarity index 100% rename from regression/cbmc-library/llround-01/test.desc rename to regression/cbmc-library/llroundf/test.desc diff --git a/regression/cbmc-library/llroundl-01/main.c b/regression/cbmc-library/llroundl/main.c similarity index 100% rename from regression/cbmc-library/llroundl-01/main.c rename to regression/cbmc-library/llroundl/main.c diff --git a/regression/cbmc-library/llroundf-01/test.desc b/regression/cbmc-library/llroundl/test.desc similarity index 100% rename from regression/cbmc-library/llroundf-01/test.desc rename to regression/cbmc-library/llroundl/test.desc diff --git a/regression/cbmc-library/localeconv-01/main.c b/regression/cbmc-library/localeconv/main.c similarity index 100% rename from regression/cbmc-library/localeconv-01/main.c rename to regression/cbmc-library/localeconv/main.c diff --git a/regression/cbmc-library/llroundl-01/test.desc b/regression/cbmc-library/localeconv/test.desc similarity index 100% rename from regression/cbmc-library/llroundl-01/test.desc rename to regression/cbmc-library/localeconv/test.desc diff --git a/regression/cbmc-library/localtime-01/main.c b/regression/cbmc-library/localtime/main.c similarity index 100% rename from regression/cbmc-library/localtime-01/main.c rename to regression/cbmc-library/localtime/main.c diff --git a/regression/cbmc-library/localeconv-01/test.desc b/regression/cbmc-library/localtime/test.desc similarity index 100% rename from regression/cbmc-library/localeconv-01/test.desc rename to regression/cbmc-library/localtime/test.desc diff --git a/regression/cbmc-library/localtime_r-01/main.c b/regression/cbmc-library/localtime_r/main.c similarity index 100% rename from regression/cbmc-library/localtime_r-01/main.c rename to regression/cbmc-library/localtime_r/main.c diff --git a/regression/cbmc-library/localtime-01/test.desc b/regression/cbmc-library/localtime_r/test.desc similarity index 100% rename from regression/cbmc-library/localtime-01/test.desc rename to regression/cbmc-library/localtime_r/test.desc diff --git a/regression/cbmc-library/log-01/main.c b/regression/cbmc-library/log/main.c similarity index 100% rename from regression/cbmc-library/log-01/main.c rename to regression/cbmc-library/log/main.c diff --git a/regression/cbmc-library/log-01/test.desc b/regression/cbmc-library/log/test.desc similarity index 100% rename from regression/cbmc-library/log-01/test.desc rename to regression/cbmc-library/log/test.desc diff --git a/regression/cbmc-library/log10-01/main.c b/regression/cbmc-library/log10/main.c similarity index 100% rename from regression/cbmc-library/log10-01/main.c rename to regression/cbmc-library/log10/main.c diff --git a/regression/cbmc-library/log10-01/test.desc b/regression/cbmc-library/log10/test.desc similarity index 100% rename from regression/cbmc-library/log10-01/test.desc rename to regression/cbmc-library/log10/test.desc diff --git a/regression/cbmc-library/log10f-01/main.c b/regression/cbmc-library/log10f/main.c similarity index 100% rename from regression/cbmc-library/log10f-01/main.c rename to regression/cbmc-library/log10f/main.c diff --git a/regression/cbmc-library/log10f-01/test.desc b/regression/cbmc-library/log10f/test.desc similarity index 100% rename from regression/cbmc-library/log10f-01/test.desc rename to regression/cbmc-library/log10f/test.desc diff --git a/regression/cbmc-library/log10l-01/main.c b/regression/cbmc-library/log10l/main.c similarity index 100% rename from regression/cbmc-library/log10l-01/main.c rename to regression/cbmc-library/log10l/main.c diff --git a/regression/cbmc-library/log10l-01/test.desc b/regression/cbmc-library/log10l/test.desc similarity index 100% rename from regression/cbmc-library/log10l-01/test.desc rename to regression/cbmc-library/log10l/test.desc diff --git a/regression/cbmc-library/log2-01/main.c b/regression/cbmc-library/log2/main.c similarity index 100% rename from regression/cbmc-library/log2-01/main.c rename to regression/cbmc-library/log2/main.c diff --git a/regression/cbmc-library/log2-01/test.desc b/regression/cbmc-library/log2/test.desc similarity index 100% rename from regression/cbmc-library/log2-01/test.desc rename to regression/cbmc-library/log2/test.desc diff --git a/regression/cbmc-library/log2f-01/main.c b/regression/cbmc-library/log2f/main.c similarity index 100% rename from regression/cbmc-library/log2f-01/main.c rename to regression/cbmc-library/log2f/main.c diff --git a/regression/cbmc-library/log2f-01/test.desc b/regression/cbmc-library/log2f/test.desc similarity index 100% rename from regression/cbmc-library/log2f-01/test.desc rename to regression/cbmc-library/log2f/test.desc diff --git a/regression/cbmc-library/log2l-01/main.c b/regression/cbmc-library/log2l/main.c similarity index 100% rename from regression/cbmc-library/log2l-01/main.c rename to regression/cbmc-library/log2l/main.c diff --git a/regression/cbmc-library/log2l-01/test.desc b/regression/cbmc-library/log2l/test.desc similarity index 100% rename from regression/cbmc-library/log2l-01/test.desc rename to regression/cbmc-library/log2l/test.desc diff --git a/regression/cbmc-library/logf-01/main.c b/regression/cbmc-library/logf/main.c similarity index 100% rename from regression/cbmc-library/logf-01/main.c rename to regression/cbmc-library/logf/main.c diff --git a/regression/cbmc-library/logf-01/test.desc b/regression/cbmc-library/logf/test.desc similarity index 100% rename from regression/cbmc-library/logf-01/test.desc rename to regression/cbmc-library/logf/test.desc diff --git a/regression/cbmc-library/logl-01/main.c b/regression/cbmc-library/logl/main.c similarity index 100% rename from regression/cbmc-library/logl-01/main.c rename to regression/cbmc-library/logl/main.c diff --git a/regression/cbmc-library/logl-01/test.desc b/regression/cbmc-library/logl/test.desc similarity index 100% rename from regression/cbmc-library/logl-01/test.desc rename to regression/cbmc-library/logl/test.desc diff --git a/regression/cbmc-library/longjmp-01/main.c b/regression/cbmc-library/longjmp/main.c similarity index 100% rename from regression/cbmc-library/longjmp-01/main.c rename to regression/cbmc-library/longjmp/main.c diff --git a/regression/cbmc-library/longjmp-01/test.desc b/regression/cbmc-library/longjmp/test.desc similarity index 100% rename from regression/cbmc-library/longjmp-01/test.desc rename to regression/cbmc-library/longjmp/test.desc diff --git a/regression/cbmc-library/lrint-01/main.c b/regression/cbmc-library/lrint/main.c similarity index 100% rename from regression/cbmc-library/lrint-01/main.c rename to regression/cbmc-library/lrint/main.c diff --git a/regression/cbmc-library/localtime_r-01/test.desc b/regression/cbmc-library/lrint/test.desc similarity index 100% rename from regression/cbmc-library/localtime_r-01/test.desc rename to regression/cbmc-library/lrint/test.desc diff --git a/regression/cbmc-library/lrintf-01/main.c b/regression/cbmc-library/lrintf/main.c similarity index 100% rename from regression/cbmc-library/lrintf-01/main.c rename to regression/cbmc-library/lrintf/main.c diff --git a/regression/cbmc-library/lrint-01/test.desc b/regression/cbmc-library/lrintf/test.desc similarity index 100% rename from regression/cbmc-library/lrint-01/test.desc rename to regression/cbmc-library/lrintf/test.desc diff --git a/regression/cbmc-library/lrintl-01/main.c b/regression/cbmc-library/lrintl/main.c similarity index 100% rename from regression/cbmc-library/lrintl-01/main.c rename to regression/cbmc-library/lrintl/main.c diff --git a/regression/cbmc-library/lrintf-01/test.desc b/regression/cbmc-library/lrintl/test.desc similarity index 100% rename from regression/cbmc-library/lrintf-01/test.desc rename to regression/cbmc-library/lrintl/test.desc diff --git a/regression/cbmc-library/lround-01/main.c b/regression/cbmc-library/lround/main.c similarity index 100% rename from regression/cbmc-library/lround-01/main.c rename to regression/cbmc-library/lround/main.c diff --git a/regression/cbmc-library/lrintl-01/test.desc b/regression/cbmc-library/lround/test.desc similarity index 100% rename from regression/cbmc-library/lrintl-01/test.desc rename to regression/cbmc-library/lround/test.desc diff --git a/regression/cbmc-library/lroundf-01/main.c b/regression/cbmc-library/lroundf/main.c similarity index 100% rename from regression/cbmc-library/lroundf-01/main.c rename to regression/cbmc-library/lroundf/main.c diff --git a/regression/cbmc-library/lround-01/test.desc b/regression/cbmc-library/lroundf/test.desc similarity index 100% rename from regression/cbmc-library/lround-01/test.desc rename to regression/cbmc-library/lroundf/test.desc diff --git a/regression/cbmc-library/lroundl-01/main.c b/regression/cbmc-library/lroundl/main.c similarity index 100% rename from regression/cbmc-library/lroundl-01/main.c rename to regression/cbmc-library/lroundl/main.c diff --git a/regression/cbmc-library/lroundf-01/test.desc b/regression/cbmc-library/lroundl/test.desc similarity index 100% rename from regression/cbmc-library/lroundf-01/test.desc rename to regression/cbmc-library/lroundl/test.desc diff --git a/regression/cbmc-library/malloc-01/main.c b/regression/cbmc-library/malloc-01/main.c deleted file mode 100644 index fe564dce9b2..00000000000 --- a/regression/cbmc-library/malloc-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - malloc(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/Malloc20/main.c b/regression/cbmc-library/malloc/main.c similarity index 100% rename from regression/cbmc-library/Malloc20/main.c rename to regression/cbmc-library/malloc/main.c diff --git a/regression/cbmc-library/Malloc20/test.desc b/regression/cbmc-library/malloc/test.desc similarity index 100% rename from regression/cbmc-library/Malloc20/test.desc rename to regression/cbmc-library/malloc/test.desc diff --git a/regression/cbmc-library/memcmp-01/main.c b/regression/cbmc-library/memcmp/main.c similarity index 100% rename from regression/cbmc-library/memcmp-01/main.c rename to regression/cbmc-library/memcmp/main.c diff --git a/regression/cbmc-library/lroundl-01/test.desc b/regression/cbmc-library/memcmp/test.desc similarity index 100% rename from regression/cbmc-library/lroundl-01/test.desc rename to regression/cbmc-library/memcmp/test.desc diff --git a/regression/cbmc-library/memcpy-01/constant-propagation.desc b/regression/cbmc-library/memcpy/constant-propagation_01.desc similarity index 93% rename from regression/cbmc-library/memcpy-01/constant-propagation.desc rename to regression/cbmc-library/memcpy/constant-propagation_01.desc index 9762ce62b88..8eecb8a3aec 100644 --- a/regression/cbmc-library/memcpy-01/constant-propagation.desc +++ b/regression/cbmc-library/memcpy/constant-propagation_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --no-standard-checks --verbosity 8 ^Generated 1\d* VCC\(s\), 0 remaining after simplification$ ^EXIT=0$ diff --git a/regression/cbmc-library/memcpy-01/main.c b/regression/cbmc-library/memcpy/main_01.c similarity index 100% rename from regression/cbmc-library/memcpy-01/main.c rename to regression/cbmc-library/memcpy/main_01.c diff --git a/regression/cbmc-library/memcpy-03/main.c b/regression/cbmc-library/memcpy/main_03.c similarity index 100% rename from regression/cbmc-library/memcpy-03/main.c rename to regression/cbmc-library/memcpy/main_03.c diff --git a/regression/cbmc-library/memcpy-04/main.c b/regression/cbmc-library/memcpy/main_04.c similarity index 100% rename from regression/cbmc-library/memcpy-04/main.c rename to regression/cbmc-library/memcpy/main_04.c diff --git a/regression/cbmc-library/memcpy-05/main.c b/regression/cbmc-library/memcpy/main_05.c similarity index 100% rename from regression/cbmc-library/memcpy-05/main.c rename to regression/cbmc-library/memcpy/main_05.c diff --git a/regression/cbmc-library/memcpy-06/main.c b/regression/cbmc-library/memcpy/main_06.c similarity index 100% rename from regression/cbmc-library/memcpy-06/main.c rename to regression/cbmc-library/memcpy/main_06.c diff --git a/regression/cbmc-library/memcpy-07/main.c b/regression/cbmc-library/memcpy/main_07.c similarity index 100% rename from regression/cbmc-library/memcpy-07/main.c rename to regression/cbmc-library/memcpy/main_07.c diff --git a/regression/cbmc-library/memcpy-08/main.c b/regression/cbmc-library/memcpy/main_08.c similarity index 100% rename from regression/cbmc-library/memcpy-08/main.c rename to regression/cbmc-library/memcpy/main_08.c diff --git a/regression/cbmc-library/memcpy-09/main.c b/regression/cbmc-library/memcpy/main_09.c similarity index 100% rename from regression/cbmc-library/memcpy-09/main.c rename to regression/cbmc-library/memcpy/main_09.c diff --git a/regression/cbmc-library/memcpy-02/memcpy1.c b/regression/cbmc-library/memcpy/memcpy1_02.c similarity index 100% rename from regression/cbmc-library/memcpy-02/memcpy1.c rename to regression/cbmc-library/memcpy/memcpy1_02.c diff --git a/regression/cbmc-library/memcpy-02/memcpy1.desc b/regression/cbmc-library/memcpy/memcpy1_02.desc similarity index 94% rename from regression/cbmc-library/memcpy-02/memcpy1.desc rename to regression/cbmc-library/memcpy/memcpy1_02.desc index f84056324a3..95635d2572a 100644 --- a/regression/cbmc-library/memcpy-02/memcpy1.desc +++ b/regression/cbmc-library/memcpy/memcpy1_02.desc @@ -1,5 +1,5 @@ CORE -memcpy1.c +memcpy1_02.c --bounds-check --pointer-check ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-02/memcpy2.c b/regression/cbmc-library/memcpy/memcpy2_02.c similarity index 100% rename from regression/cbmc-library/memcpy-02/memcpy2.c rename to regression/cbmc-library/memcpy/memcpy2_02.c diff --git a/regression/cbmc-library/memcpy-02/memcpy2.desc b/regression/cbmc-library/memcpy/memcpy2_02.desc similarity index 85% rename from regression/cbmc-library/memcpy-02/memcpy2.desc rename to regression/cbmc-library/memcpy/memcpy2_02.desc index 2aa28439c19..83e325c7451 100644 --- a/regression/cbmc-library/memcpy-02/memcpy2.desc +++ b/regression/cbmc-library/memcpy/memcpy2_02.desc @@ -1,5 +1,5 @@ CORE -memcpy2.c +memcpy2_02.c ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-02/memcpy3.c b/regression/cbmc-library/memcpy/memcpy3_02.c similarity index 100% rename from regression/cbmc-library/memcpy-02/memcpy3.c rename to regression/cbmc-library/memcpy/memcpy3_02.c diff --git a/regression/cbmc-library/memcpy/memcpy3_02.desc b/regression/cbmc-library/memcpy/memcpy3_02.desc new file mode 100644 index 00000000000..da51da0931a --- /dev/null +++ b/regression/cbmc-library/memcpy/memcpy3_02.desc @@ -0,0 +1,8 @@ +CORE +memcpy3_02.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/memcpy-02/memcpy4.c b/regression/cbmc-library/memcpy/memcpy4_02.c similarity index 100% rename from regression/cbmc-library/memcpy-02/memcpy4.c rename to regression/cbmc-library/memcpy/memcpy4_02.c diff --git a/regression/cbmc-library/memcpy-02/memcpy4.desc b/regression/cbmc-library/memcpy/memcpy4_02.desc similarity index 96% rename from regression/cbmc-library/memcpy-02/memcpy4.desc rename to regression/cbmc-library/memcpy/memcpy4_02.desc index dce453fe152..a7375ed6ae6 100644 --- a/regression/cbmc-library/memcpy-02/memcpy4.desc +++ b/regression/cbmc-library/memcpy/memcpy4_02.desc @@ -1,5 +1,5 @@ CORE -memcpy4.c +memcpy4_02.c --pointer-check ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-01/test.desc b/regression/cbmc-library/memcpy/test_01.desc similarity index 96% rename from regression/cbmc-library/memcpy-01/test.desc rename to regression/cbmc-library/memcpy/test_01.desc index b8aa4e562b8..408242d4a5a 100644 --- a/regression/cbmc-library/memcpy-01/test.desc +++ b/regression/cbmc-library/memcpy/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --bounds-check --pointer-check ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-03/test.desc b/regression/cbmc-library/memcpy/test_03.desc similarity index 94% rename from regression/cbmc-library/memcpy-03/test.desc rename to regression/cbmc-library/memcpy/test_03.desc index 7dbda2b83e4..b283bd35a87 100644 --- a/regression/cbmc-library/memcpy-03/test.desc +++ b/regression/cbmc-library/memcpy/test_03.desc @@ -1,5 +1,5 @@ CORE -main.c +main_03.c ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-04/test.desc b/regression/cbmc-library/memcpy/test_04.desc similarity index 95% rename from regression/cbmc-library/memcpy-04/test.desc rename to regression/cbmc-library/memcpy/test_04.desc index 677883aefd0..8b483d9d037 100644 --- a/regression/cbmc-library/memcpy-04/test.desc +++ b/regression/cbmc-library/memcpy/test_04.desc @@ -1,5 +1,5 @@ CORE -main.c +main_04.c --no-malloc-may-fail ^\[publish.assertion.1\] line 18 should pass: SUCCESS$ ^\[publish.assertion.2\] line 19 should fail: FAILURE$ diff --git a/regression/cbmc-library/memcpy-05/test.desc b/regression/cbmc-library/memcpy/test_05.desc similarity index 90% rename from regression/cbmc-library/memcpy-05/test.desc rename to regression/cbmc-library/memcpy/test_05.desc index b078554745c..84bde78a5d8 100644 --- a/regression/cbmc-library/memcpy-05/test.desc +++ b/regression/cbmc-library/memcpy/test_05.desc @@ -1,5 +1,5 @@ CORE -main.c +main_05.c --no-malloc-may-fail ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc-library/memcpy-06/test.desc b/regression/cbmc-library/memcpy/test_06.desc similarity index 96% rename from regression/cbmc-library/memcpy-06/test.desc rename to regression/cbmc-library/memcpy/test_06.desc index 666ab2ea623..59a7a4bfdc2 100644 --- a/regression/cbmc-library/memcpy-06/test.desc +++ b/regression/cbmc-library/memcpy/test_06.desc @@ -1,5 +1,5 @@ CORE gcc-only -main.c +main_06.c function 'memcpy' is not declared parameter "memcpy::dst" type mismatch diff --git a/regression/cbmc-library/memcpy-07/test.desc b/regression/cbmc-library/memcpy/test_07.desc similarity index 96% rename from regression/cbmc-library/memcpy-07/test.desc rename to regression/cbmc-library/memcpy/test_07.desc index 6defaba620a..c02cb00ded0 100644 --- a/regression/cbmc-library/memcpy-07/test.desc +++ b/regression/cbmc-library/memcpy/test_07.desc @@ -1,5 +1,5 @@ CORE -main.c +main_07.c ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memcpy-08/test.desc b/regression/cbmc-library/memcpy/test_08.desc similarity index 95% rename from regression/cbmc-library/memcpy-08/test.desc rename to regression/cbmc-library/memcpy/test_08.desc index 4d09581661a..519db5ff977 100644 --- a/regression/cbmc-library/memcpy-08/test.desc +++ b/regression/cbmc-library/memcpy/test_08.desc @@ -1,5 +1,5 @@ CORE -main.c +main_08.c --no-malloc-may-fail ^\[main.assertion.1\] line 20 should pass: SUCCESS$ ^\[main.assertion.2\] line 21 should fail: FAILURE$ diff --git a/regression/cbmc-library/memcpy-09/test.desc b/regression/cbmc-library/memcpy/test_09.desc similarity index 96% rename from regression/cbmc-library/memcpy-09/test.desc rename to regression/cbmc-library/memcpy/test_09.desc index 217091c1fa3..b84b04efac1 100644 --- a/regression/cbmc-library/memcpy-09/test.desc +++ b/regression/cbmc-library/memcpy/test_09.desc @@ -1,5 +1,5 @@ CORE gcc-only -main.c +main_09.c ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc-library/memmove-01/constant.c b/regression/cbmc-library/memmove/constant.c similarity index 100% rename from regression/cbmc-library/memmove-01/constant.c rename to regression/cbmc-library/memmove/constant.c diff --git a/regression/cbmc-library/memmove-01/constant.desc b/regression/cbmc-library/memmove/constant.desc similarity index 100% rename from regression/cbmc-library/memmove-01/constant.desc rename to regression/cbmc-library/memmove/constant.desc diff --git a/regression/cbmc-library/memmove-01/main.c b/regression/cbmc-library/memmove/main.c similarity index 100% rename from regression/cbmc-library/memmove-01/main.c rename to regression/cbmc-library/memmove/main.c diff --git a/regression/cbmc-library/memmove-01/test.desc b/regression/cbmc-library/memmove/test.desc similarity index 100% rename from regression/cbmc-library/memmove-01/test.desc rename to regression/cbmc-library/memmove/test.desc diff --git a/regression/cbmc-library/memset-01/main.c b/regression/cbmc-library/memset-01/main.c deleted file mode 100644 index 699b3884332..00000000000 --- a/regression/cbmc-library/memset-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - memset(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/equality_through_struct_containing_arrays3/main.c b/regression/cbmc-library/memset/equality_through_struct_containing_arrays3.c similarity index 100% rename from regression/cbmc-library/equality_through_struct_containing_arrays3/main.c rename to regression/cbmc-library/memset/equality_through_struct_containing_arrays3.c diff --git a/regression/cbmc-library/memset/equality_through_struct_containing_arrays3.desc b/regression/cbmc-library/memset/equality_through_struct_containing_arrays3.desc new file mode 100644 index 00000000000..2f8f3ae1d3a --- /dev/null +++ b/regression/cbmc-library/memset/equality_through_struct_containing_arrays3.desc @@ -0,0 +1,8 @@ +CORE +equality_through_struct_containing_arrays3.c +--no-malloc-may-fail +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/equality_through_struct5/main.c b/regression/cbmc-library/memset/main.c similarity index 100% rename from regression/cbmc-library/equality_through_struct5/main.c rename to regression/cbmc-library/memset/main.c diff --git a/regression/cbmc-library/floorf-01/test.desc b/regression/cbmc-library/memset/test.desc similarity index 100% rename from regression/cbmc-library/floorf-01/test.desc rename to regression/cbmc-library/memset/test.desc diff --git a/regression/cbmc-library/mktime-01/main.c b/regression/cbmc-library/mktime/main.c similarity index 100% rename from regression/cbmc-library/mktime-01/main.c rename to regression/cbmc-library/mktime/main.c diff --git a/regression/cbmc-library/malloc-01/test.desc b/regression/cbmc-library/mktime/test.desc similarity index 100% rename from regression/cbmc-library/malloc-01/test.desc rename to regression/cbmc-library/mktime/test.desc diff --git a/regression/cbmc-library/mmap-01/main.c b/regression/cbmc-library/mmap/main.c similarity index 100% rename from regression/cbmc-library/mmap-01/main.c rename to regression/cbmc-library/mmap/main.c diff --git a/regression/cbmc-library/mmap-01/test.desc b/regression/cbmc-library/mmap/test.desc similarity index 100% rename from regression/cbmc-library/mmap-01/test.desc rename to regression/cbmc-library/mmap/test.desc diff --git a/regression/cbmc-library/modf-01/main.c b/regression/cbmc-library/modf/main.c similarity index 100% rename from regression/cbmc-library/modf-01/main.c rename to regression/cbmc-library/modf/main.c diff --git a/regression/cbmc-library/memcmp-01/test.desc b/regression/cbmc-library/modf/test.desc similarity index 100% rename from regression/cbmc-library/memcmp-01/test.desc rename to regression/cbmc-library/modf/test.desc diff --git a/regression/cbmc-library/modff-01/main.c b/regression/cbmc-library/modff/main.c similarity index 100% rename from regression/cbmc-library/modff-01/main.c rename to regression/cbmc-library/modff/main.c diff --git a/regression/cbmc-library/memset-01/test.desc b/regression/cbmc-library/modff/test.desc similarity index 100% rename from regression/cbmc-library/memset-01/test.desc rename to regression/cbmc-library/modff/test.desc diff --git a/regression/cbmc-library/modfl-01/main.c b/regression/cbmc-library/modfl/main.c similarity index 100% rename from regression/cbmc-library/modfl-01/main.c rename to regression/cbmc-library/modfl/main.c diff --git a/regression/cbmc-library/mktime-01/test.desc b/regression/cbmc-library/modfl/test.desc similarity index 100% rename from regression/cbmc-library/mktime-01/test.desc rename to regression/cbmc-library/modfl/test.desc diff --git a/regression/cbmc-library/mtx_destroy-01/main.c b/regression/cbmc-library/mtx_destroy/main.c similarity index 100% rename from regression/cbmc-library/mtx_destroy-01/main.c rename to regression/cbmc-library/mtx_destroy/main.c diff --git a/regression/cbmc-library/modf-01/test.desc b/regression/cbmc-library/mtx_destroy/test.desc similarity index 100% rename from regression/cbmc-library/modf-01/test.desc rename to regression/cbmc-library/mtx_destroy/test.desc diff --git a/regression/cbmc-library/mtx_init-01/main.c b/regression/cbmc-library/mtx_init/main.c similarity index 100% rename from regression/cbmc-library/mtx_init-01/main.c rename to regression/cbmc-library/mtx_init/main.c diff --git a/regression/cbmc-library/modff-01/test.desc b/regression/cbmc-library/mtx_init/test.desc similarity index 100% rename from regression/cbmc-library/modff-01/test.desc rename to regression/cbmc-library/mtx_init/test.desc diff --git a/regression/cbmc-library/mtx_lock-01/main.c b/regression/cbmc-library/mtx_lock/main.c similarity index 100% rename from regression/cbmc-library/mtx_lock-01/main.c rename to regression/cbmc-library/mtx_lock/main.c diff --git a/regression/cbmc-library/modfl-01/test.desc b/regression/cbmc-library/mtx_lock/test.desc similarity index 100% rename from regression/cbmc-library/modfl-01/test.desc rename to regression/cbmc-library/mtx_lock/test.desc diff --git a/regression/cbmc-library/mtx_timedlock-01/main.c b/regression/cbmc-library/mtx_timedlock/main.c similarity index 100% rename from regression/cbmc-library/mtx_timedlock-01/main.c rename to regression/cbmc-library/mtx_timedlock/main.c diff --git a/regression/cbmc-library/mtx_destroy-01/test.desc b/regression/cbmc-library/mtx_timedlock/test.desc similarity index 100% rename from regression/cbmc-library/mtx_destroy-01/test.desc rename to regression/cbmc-library/mtx_timedlock/test.desc diff --git a/regression/cbmc-library/mtx_trylock-01/main.c b/regression/cbmc-library/mtx_trylock/main.c similarity index 100% rename from regression/cbmc-library/mtx_trylock-01/main.c rename to regression/cbmc-library/mtx_trylock/main.c diff --git a/regression/cbmc-library/mtx_init-01/test.desc b/regression/cbmc-library/mtx_trylock/test.desc similarity index 100% rename from regression/cbmc-library/mtx_init-01/test.desc rename to regression/cbmc-library/mtx_trylock/test.desc diff --git a/regression/cbmc-library/mtx_unlock-01/main.c b/regression/cbmc-library/mtx_unlock/main.c similarity index 100% rename from regression/cbmc-library/mtx_unlock-01/main.c rename to regression/cbmc-library/mtx_unlock/main.c diff --git a/regression/cbmc-library/mtx_lock-01/test.desc b/regression/cbmc-library/mtx_unlock/test.desc similarity index 100% rename from regression/cbmc-library/mtx_lock-01/test.desc rename to regression/cbmc-library/mtx_unlock/test.desc diff --git a/regression/cbmc-library/nan-01/main.c b/regression/cbmc-library/nan/main.c similarity index 100% rename from regression/cbmc-library/nan-01/main.c rename to regression/cbmc-library/nan/main.c diff --git a/regression/cbmc-library/mtx_timedlock-01/test.desc b/regression/cbmc-library/nan/test.desc similarity index 100% rename from regression/cbmc-library/mtx_timedlock-01/test.desc rename to regression/cbmc-library/nan/test.desc diff --git a/regression/cbmc-library/nanf-01/main.c b/regression/cbmc-library/nanf/main.c similarity index 100% rename from regression/cbmc-library/nanf-01/main.c rename to regression/cbmc-library/nanf/main.c diff --git a/regression/cbmc-library/mtx_trylock-01/test.desc b/regression/cbmc-library/nanf/test.desc similarity index 100% rename from regression/cbmc-library/mtx_trylock-01/test.desc rename to regression/cbmc-library/nanf/test.desc diff --git a/regression/cbmc-library/nanl-01/main.c b/regression/cbmc-library/nanl/main.c similarity index 100% rename from regression/cbmc-library/nanl-01/main.c rename to regression/cbmc-library/nanl/main.c diff --git a/regression/cbmc-library/mtx_unlock-01/test.desc b/regression/cbmc-library/nanl/test.desc similarity index 100% rename from regression/cbmc-library/mtx_unlock-01/test.desc rename to regression/cbmc-library/nanl/test.desc diff --git a/regression/cbmc-library/nearbyint-01/main.c b/regression/cbmc-library/nearbyint/main.c similarity index 100% rename from regression/cbmc-library/nearbyint-01/main.c rename to regression/cbmc-library/nearbyint/main.c diff --git a/regression/cbmc-library/nan-01/test.desc b/regression/cbmc-library/nearbyint/test.desc similarity index 100% rename from regression/cbmc-library/nan-01/test.desc rename to regression/cbmc-library/nearbyint/test.desc diff --git a/regression/cbmc-library/nearbyintf-01/main.c b/regression/cbmc-library/nearbyintf/main.c similarity index 100% rename from regression/cbmc-library/nearbyintf-01/main.c rename to regression/cbmc-library/nearbyintf/main.c diff --git a/regression/cbmc-library/nanf-01/test.desc b/regression/cbmc-library/nearbyintf/test.desc similarity index 100% rename from regression/cbmc-library/nanf-01/test.desc rename to regression/cbmc-library/nearbyintf/test.desc diff --git a/regression/cbmc-library/nearbyintl-01/main.c b/regression/cbmc-library/nearbyintl/main.c similarity index 100% rename from regression/cbmc-library/nearbyintl-01/main.c rename to regression/cbmc-library/nearbyintl/main.c diff --git a/regression/cbmc-library/nanl-01/test.desc b/regression/cbmc-library/nearbyintl/test.desc similarity index 100% rename from regression/cbmc-library/nanl-01/test.desc rename to regression/cbmc-library/nearbyintl/test.desc diff --git a/regression/cbmc-library/nextUp-01/main.c b/regression/cbmc-library/nextUp/main.c similarity index 100% rename from regression/cbmc-library/nextUp-01/main.c rename to regression/cbmc-library/nextUp/main.c diff --git a/regression/cbmc-library/nearbyint-01/test.desc b/regression/cbmc-library/nextUp/test.desc similarity index 100% rename from regression/cbmc-library/nearbyint-01/test.desc rename to regression/cbmc-library/nextUp/test.desc diff --git a/regression/cbmc-library/nextUpf-01/main.c b/regression/cbmc-library/nextUpf/main.c similarity index 100% rename from regression/cbmc-library/nextUpf-01/main.c rename to regression/cbmc-library/nextUpf/main.c diff --git a/regression/cbmc-library/nearbyintf-01/test.desc b/regression/cbmc-library/nextUpf/test.desc similarity index 100% rename from regression/cbmc-library/nearbyintf-01/test.desc rename to regression/cbmc-library/nextUpf/test.desc diff --git a/regression/cbmc-library/nextUpl-01/main.c b/regression/cbmc-library/nextUpl/main.c similarity index 100% rename from regression/cbmc-library/nextUpl-01/main.c rename to regression/cbmc-library/nextUpl/main.c diff --git a/regression/cbmc-library/nearbyintl-01/test.desc b/regression/cbmc-library/nextUpl/test.desc similarity index 100% rename from regression/cbmc-library/nearbyintl-01/test.desc rename to regression/cbmc-library/nextUpl/test.desc diff --git a/regression/cbmc-library/ntohl-01/main.c b/regression/cbmc-library/ntohl/main.c similarity index 100% rename from regression/cbmc-library/ntohl-01/main.c rename to regression/cbmc-library/ntohl/main.c diff --git a/regression/cbmc-library/nextUp-01/test.desc b/regression/cbmc-library/ntohl/test.desc similarity index 100% rename from regression/cbmc-library/nextUp-01/test.desc rename to regression/cbmc-library/ntohl/test.desc diff --git a/regression/cbmc-library/ntohs-01/main.c b/regression/cbmc-library/ntohs/main.c similarity index 100% rename from regression/cbmc-library/ntohs-01/main.c rename to regression/cbmc-library/ntohs/main.c diff --git a/regression/cbmc-library/nextUpf-01/test.desc b/regression/cbmc-library/ntohs/test.desc similarity index 100% rename from regression/cbmc-library/nextUpf-01/test.desc rename to regression/cbmc-library/ntohs/test.desc diff --git a/regression/cbmc-library/open-01/main.c b/regression/cbmc-library/open/main.c similarity index 100% rename from regression/cbmc-library/open-01/main.c rename to regression/cbmc-library/open/main.c diff --git a/regression/cbmc-library/open-01/test.desc b/regression/cbmc-library/open/test.desc similarity index 100% rename from regression/cbmc-library/open-01/test.desc rename to regression/cbmc-library/open/test.desc diff --git a/regression/cbmc-library/openat-01/main.c b/regression/cbmc-library/openat/main.c similarity index 100% rename from regression/cbmc-library/openat-01/main.c rename to regression/cbmc-library/openat/main.c diff --git a/regression/cbmc-library/openat-01/test.desc b/regression/cbmc-library/openat/test.desc similarity index 100% rename from regression/cbmc-library/openat-01/test.desc rename to regression/cbmc-library/openat/test.desc diff --git a/regression/cbmc-library/openlog-01/main.c b/regression/cbmc-library/openlog/main.c similarity index 100% rename from regression/cbmc-library/openlog-01/main.c rename to regression/cbmc-library/openlog/main.c diff --git a/regression/cbmc-library/nextUpl-01/test.desc b/regression/cbmc-library/openlog/test.desc similarity index 100% rename from regression/cbmc-library/nextUpl-01/test.desc rename to regression/cbmc-library/openlog/test.desc diff --git a/regression/cbmc-library/perror-01/main.c b/regression/cbmc-library/perror/main.c similarity index 100% rename from regression/cbmc-library/perror-01/main.c rename to regression/cbmc-library/perror/main.c diff --git a/regression/cbmc-library/ntohl-01/test.desc b/regression/cbmc-library/perror/test.desc similarity index 100% rename from regression/cbmc-library/ntohl-01/test.desc rename to regression/cbmc-library/perror/test.desc diff --git a/regression/cbmc-library/pipe-01/main.c b/regression/cbmc-library/pipe/main.c similarity index 90% rename from regression/cbmc-library/pipe-01/main.c rename to regression/cbmc-library/pipe/main.c index 4da3acedc17..5c2bd6a2bea 100644 --- a/regression/cbmc-library/pipe-01/main.c +++ b/regression/cbmc-library/pipe/main.c @@ -1,8 +1,8 @@ #ifdef _WIN32 -#include -#include +# include +# include #else -#include +# include #endif #include diff --git a/regression/cbmc-library/pipe-01/test.desc b/regression/cbmc-library/pipe/test.desc similarity index 100% rename from regression/cbmc-library/pipe-01/test.desc rename to regression/cbmc-library/pipe/test.desc diff --git a/regression/cbmc-library/posix_memalign-01/main.c b/regression/cbmc-library/posix_memalign/main_01.c similarity index 100% rename from regression/cbmc-library/posix_memalign-01/main.c rename to regression/cbmc-library/posix_memalign/main_01.c diff --git a/regression/cbmc-library/posix_memalign-02/main.c b/regression/cbmc-library/posix_memalign/main_02.c similarity index 100% rename from regression/cbmc-library/posix_memalign-02/main.c rename to regression/cbmc-library/posix_memalign/main_02.c diff --git a/regression/cbmc-library/posix_memalign-01/test.desc b/regression/cbmc-library/posix_memalign/test_01.desc similarity index 93% rename from regression/cbmc-library/posix_memalign-01/test.desc rename to regression/cbmc-library/posix_memalign/test_01.desc index efd17d8bc17..cb40cbcdb5d 100644 --- a/regression/cbmc-library/posix_memalign-01/test.desc +++ b/regression/cbmc-library/posix_memalign/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --pointer-check --bounds-check --malloc-may-fail --malloc-fail-null VERIFICATION SUCCESSFUL ^EXIT=0$ diff --git a/regression/cbmc-library/posix_memalign-02/test.desc b/regression/cbmc-library/posix_memalign/test_02.desc similarity index 96% rename from regression/cbmc-library/posix_memalign-02/test.desc rename to regression/cbmc-library/posix_memalign/test_02.desc index 648263292fe..557cebabd95 100644 --- a/regression/cbmc-library/posix_memalign-02/test.desc +++ b/regression/cbmc-library/posix_memalign/test_02.desc @@ -1,5 +1,5 @@ CORE -main.c +main_02.c --pointer-check --bounds-check --malloc-may-fail --malloc-fail-null ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/pow-01/main.c b/regression/cbmc-library/pow/main.c similarity index 100% rename from regression/cbmc-library/pow-01/main.c rename to regression/cbmc-library/pow/main.c diff --git a/regression/cbmc-library/pow-01/test.desc b/regression/cbmc-library/pow/test.desc similarity index 100% rename from regression/cbmc-library/pow-01/test.desc rename to regression/cbmc-library/pow/test.desc diff --git a/regression/cbmc-library/powf-01/main.c b/regression/cbmc-library/powf/main.c similarity index 100% rename from regression/cbmc-library/powf-01/main.c rename to regression/cbmc-library/powf/main.c diff --git a/regression/cbmc-library/powf-01/test.desc b/regression/cbmc-library/powf/test.desc similarity index 100% rename from regression/cbmc-library/powf-01/test.desc rename to regression/cbmc-library/powf/test.desc diff --git a/regression/cbmc-library/powl-01/main.c b/regression/cbmc-library/powl/main.c similarity index 100% rename from regression/cbmc-library/powl-01/main.c rename to regression/cbmc-library/powl/main.c diff --git a/regression/cbmc-library/powl-01/test.desc b/regression/cbmc-library/powl/test.desc similarity index 100% rename from regression/cbmc-library/powl-01/test.desc rename to regression/cbmc-library/powl/test.desc diff --git a/regression/cbmc-library/printf-01/__printf_chk.desc b/regression/cbmc-library/printf/__printf_chk.desc similarity index 100% rename from regression/cbmc-library/printf-01/__printf_chk.desc rename to regression/cbmc-library/printf/__printf_chk.desc diff --git a/regression/cbmc-library/printf-01/main.c b/regression/cbmc-library/printf/main.c similarity index 100% rename from regression/cbmc-library/printf-01/main.c rename to regression/cbmc-library/printf/main.c diff --git a/regression/cbmc-library/printf-01/test.desc b/regression/cbmc-library/printf/test.desc similarity index 100% rename from regression/cbmc-library/printf-01/test.desc rename to regression/cbmc-library/printf/test.desc diff --git a/regression/cbmc-library/pthread_barrier_destroy-01/main.c b/regression/cbmc-library/pthread_barrier_destroy/main.c similarity index 100% rename from regression/cbmc-library/pthread_barrier_destroy-01/main.c rename to regression/cbmc-library/pthread_barrier_destroy/main.c diff --git a/regression/cbmc-library/pthread_barrier_destroy-01/test.desc b/regression/cbmc-library/pthread_barrier_destroy/test.desc similarity index 100% rename from regression/cbmc-library/pthread_barrier_destroy-01/test.desc rename to regression/cbmc-library/pthread_barrier_destroy/test.desc diff --git a/regression/cbmc-library/pthread_barrier_init-01/main.c b/regression/cbmc-library/pthread_barrier_init/main.c similarity index 100% rename from regression/cbmc-library/pthread_barrier_init-01/main.c rename to regression/cbmc-library/pthread_barrier_init/main.c diff --git a/regression/cbmc-library/pthread_barrier_init-01/test.desc b/regression/cbmc-library/pthread_barrier_init/test.desc similarity index 100% rename from regression/cbmc-library/pthread_barrier_init-01/test.desc rename to regression/cbmc-library/pthread_barrier_init/test.desc diff --git a/regression/cbmc-library/pthread_barrier_wait-01/main.c b/regression/cbmc-library/pthread_barrier_wait/main.c similarity index 100% rename from regression/cbmc-library/pthread_barrier_wait-01/main.c rename to regression/cbmc-library/pthread_barrier_wait/main.c diff --git a/regression/cbmc-library/pthread_barrier_wait-01/test.desc b/regression/cbmc-library/pthread_barrier_wait/test.desc similarity index 100% rename from regression/cbmc-library/pthread_barrier_wait-01/test.desc rename to regression/cbmc-library/pthread_barrier_wait/test.desc diff --git a/regression/cbmc-library/pthread_cancel-01/main.c b/regression/cbmc-library/pthread_cancel/main.c similarity index 100% rename from regression/cbmc-library/pthread_cancel-01/main.c rename to regression/cbmc-library/pthread_cancel/main.c diff --git a/regression/cbmc-library/pthread_cancel-01/test.desc b/regression/cbmc-library/pthread_cancel/test.desc similarity index 100% rename from regression/cbmc-library/pthread_cancel-01/test.desc rename to regression/cbmc-library/pthread_cancel/test.desc diff --git a/regression/cbmc-library/pthread_cond_broadcast-01/main.c b/regression/cbmc-library/pthread_cond_broadcast/main.c similarity index 100% rename from regression/cbmc-library/pthread_cond_broadcast-01/main.c rename to regression/cbmc-library/pthread_cond_broadcast/main.c diff --git a/regression/cbmc-library/pthread_cond_broadcast-01/test.desc b/regression/cbmc-library/pthread_cond_broadcast/test.desc similarity index 100% rename from regression/cbmc-library/pthread_cond_broadcast-01/test.desc rename to regression/cbmc-library/pthread_cond_broadcast/test.desc diff --git a/regression/cbmc-library/pthread_cond_init-01/main.c b/regression/cbmc-library/pthread_cond_init/main.c similarity index 100% rename from regression/cbmc-library/pthread_cond_init-01/main.c rename to regression/cbmc-library/pthread_cond_init/main.c diff --git a/regression/cbmc-library/pthread_cond_init-01/test.desc b/regression/cbmc-library/pthread_cond_init/test.desc similarity index 100% rename from regression/cbmc-library/pthread_cond_init-01/test.desc rename to regression/cbmc-library/pthread_cond_init/test.desc diff --git a/regression/cbmc-library/pthread_cond_signal-01/main.c b/regression/cbmc-library/pthread_cond_signal/main.c similarity index 100% rename from regression/cbmc-library/pthread_cond_signal-01/main.c rename to regression/cbmc-library/pthread_cond_signal/main.c diff --git a/regression/cbmc-library/pthread_cond_signal-01/test.desc b/regression/cbmc-library/pthread_cond_signal/test.desc similarity index 100% rename from regression/cbmc-library/pthread_cond_signal-01/test.desc rename to regression/cbmc-library/pthread_cond_signal/test.desc diff --git a/regression/cbmc-library/pthread_cond_wait-01/main.c b/regression/cbmc-library/pthread_cond_wait/main.c similarity index 100% rename from regression/cbmc-library/pthread_cond_wait-01/main.c rename to regression/cbmc-library/pthread_cond_wait/main.c diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait/test.desc similarity index 100% rename from regression/cbmc-library/pthread_cond_wait-01/test.desc rename to regression/cbmc-library/pthread_cond_wait/test.desc diff --git a/regression/cbmc-library/pthread_create-01/main.c b/regression/cbmc-library/pthread_create/main.c similarity index 100% rename from regression/cbmc-library/pthread_create-01/main.c rename to regression/cbmc-library/pthread_create/main.c diff --git a/regression/cbmc-library/pthread_create-01/test.desc b/regression/cbmc-library/pthread_create/test.desc similarity index 100% rename from regression/cbmc-library/pthread_create-01/test.desc rename to regression/cbmc-library/pthread_create/test.desc diff --git a/regression/cbmc-library/pthread_exit-01/main.c b/regression/cbmc-library/pthread_exit/main.c similarity index 100% rename from regression/cbmc-library/pthread_exit-01/main.c rename to regression/cbmc-library/pthread_exit/main.c diff --git a/regression/cbmc-library/pthread_exit-01/test.desc b/regression/cbmc-library/pthread_exit/test.desc similarity index 100% rename from regression/cbmc-library/pthread_exit-01/test.desc rename to regression/cbmc-library/pthread_exit/test.desc diff --git a/regression/cbmc-library/pthread_getspecific-01/main.c b/regression/cbmc-library/pthread_getspecific/main.c similarity index 100% rename from regression/cbmc-library/pthread_getspecific-01/main.c rename to regression/cbmc-library/pthread_getspecific/main.c diff --git a/regression/cbmc-library/ntohs-01/test.desc b/regression/cbmc-library/pthread_getspecific/test.desc similarity index 100% rename from regression/cbmc-library/ntohs-01/test.desc rename to regression/cbmc-library/pthread_getspecific/test.desc diff --git a/regression/cbmc-library/pthread_join-01/main.c b/regression/cbmc-library/pthread_join/main.c similarity index 100% rename from regression/cbmc-library/pthread_join-01/main.c rename to regression/cbmc-library/pthread_join/main.c diff --git a/regression/cbmc-library/pthread_join-01/test.desc b/regression/cbmc-library/pthread_join/test.desc similarity index 100% rename from regression/cbmc-library/pthread_join-01/test.desc rename to regression/cbmc-library/pthread_join/test.desc diff --git a/regression/cbmc-library/pthread_key_create-01/main.c b/regression/cbmc-library/pthread_key_create/main.c similarity index 100% rename from regression/cbmc-library/pthread_key_create-01/main.c rename to regression/cbmc-library/pthread_key_create/main.c diff --git a/regression/cbmc-library/openlog-01/test.desc b/regression/cbmc-library/pthread_key_create/test.desc similarity index 100% rename from regression/cbmc-library/openlog-01/test.desc rename to regression/cbmc-library/pthread_key_create/test.desc diff --git a/regression/cbmc-library/pthread_key_delete-01/main.c b/regression/cbmc-library/pthread_key_delete/main.c similarity index 100% rename from regression/cbmc-library/pthread_key_delete-01/main.c rename to regression/cbmc-library/pthread_key_delete/main.c diff --git a/regression/cbmc-library/perror-01/test.desc b/regression/cbmc-library/pthread_key_delete/test.desc similarity index 100% rename from regression/cbmc-library/perror-01/test.desc rename to regression/cbmc-library/pthread_key_delete/test.desc diff --git a/regression/cbmc-library/pthread_mutex_destroy-01/main.c b/regression/cbmc-library/pthread_mutex_destroy/main.c similarity index 100% rename from regression/cbmc-library/pthread_mutex_destroy-01/main.c rename to regression/cbmc-library/pthread_mutex_destroy/main.c diff --git a/regression/cbmc-library/pthread_mutex_destroy-01/test.desc b/regression/cbmc-library/pthread_mutex_destroy/test.desc similarity index 100% rename from regression/cbmc-library/pthread_mutex_destroy-01/test.desc rename to regression/cbmc-library/pthread_mutex_destroy/test.desc diff --git a/regression/cbmc-library/pthread_mutex_init-01/main.c b/regression/cbmc-library/pthread_mutex_init/main.c similarity index 100% rename from regression/cbmc-library/pthread_mutex_init-01/main.c rename to regression/cbmc-library/pthread_mutex_init/main.c diff --git a/regression/cbmc-library/pthread_mutex_init-01/test.desc b/regression/cbmc-library/pthread_mutex_init/test.desc similarity index 100% rename from regression/cbmc-library/pthread_mutex_init-01/test.desc rename to regression/cbmc-library/pthread_mutex_init/test.desc diff --git a/regression/cbmc-library/pthread_mutex_lock-01/main.c b/regression/cbmc-library/pthread_mutex_lock/main.c similarity index 100% rename from regression/cbmc-library/pthread_mutex_lock-01/main.c rename to regression/cbmc-library/pthread_mutex_lock/main.c diff --git a/regression/cbmc-library/pthread_mutex_lock-01/test.desc b/regression/cbmc-library/pthread_mutex_lock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_mutex_lock-01/test.desc rename to regression/cbmc-library/pthread_mutex_lock/test.desc diff --git a/regression/cbmc-library/pthread_mutex_trylock-01/main.c b/regression/cbmc-library/pthread_mutex_trylock/main.c similarity index 100% rename from regression/cbmc-library/pthread_mutex_trylock-01/main.c rename to regression/cbmc-library/pthread_mutex_trylock/main.c diff --git a/regression/cbmc-library/pthread_mutex_trylock-01/test.desc b/regression/cbmc-library/pthread_mutex_trylock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_mutex_trylock-01/test.desc rename to regression/cbmc-library/pthread_mutex_trylock/test.desc diff --git a/regression/cbmc-library/pthread_mutex_unlock-01/main.c b/regression/cbmc-library/pthread_mutex_unlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_mutex_unlock-01/main.c rename to regression/cbmc-library/pthread_mutex_unlock/main.c diff --git a/regression/cbmc-library/pthread_mutex_unlock-01/test.desc b/regression/cbmc-library/pthread_mutex_unlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_mutex_unlock-01/test.desc rename to regression/cbmc-library/pthread_mutex_unlock/test.desc diff --git a/regression/cbmc-library/pthread_mutexattr_settype-01/main.c b/regression/cbmc-library/pthread_mutexattr_settype/main.c similarity index 100% rename from regression/cbmc-library/pthread_mutexattr_settype-01/main.c rename to regression/cbmc-library/pthread_mutexattr_settype/main.c diff --git a/regression/cbmc-library/pthread_mutexattr_settype-01/test.desc b/regression/cbmc-library/pthread_mutexattr_settype/test.desc similarity index 100% rename from regression/cbmc-library/pthread_mutexattr_settype-01/test.desc rename to regression/cbmc-library/pthread_mutexattr_settype/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_destroy-01/main.c b/regression/cbmc-library/pthread_rwlock_destroy/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_destroy-01/main.c rename to regression/cbmc-library/pthread_rwlock_destroy/main.c diff --git a/regression/cbmc-library/pthread_rwlock_destroy-01/test.desc b/regression/cbmc-library/pthread_rwlock_destroy/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_destroy-01/test.desc rename to regression/cbmc-library/pthread_rwlock_destroy/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_init-01/main.c b/regression/cbmc-library/pthread_rwlock_init/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_init-01/main.c rename to regression/cbmc-library/pthread_rwlock_init/main.c diff --git a/regression/cbmc-library/pthread_rwlock_init-01/test.desc b/regression/cbmc-library/pthread_rwlock_init/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_init-01/test.desc rename to regression/cbmc-library/pthread_rwlock_init/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_rdlock-01/main.c b/regression/cbmc-library/pthread_rwlock_rdlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_rdlock-01/main.c rename to regression/cbmc-library/pthread_rwlock_rdlock/main.c diff --git a/regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_rdlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc rename to regression/cbmc-library/pthread_rwlock_rdlock/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_tryrdlock-01/main.c b/regression/cbmc-library/pthread_rwlock_tryrdlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_tryrdlock-01/main.c rename to regression/cbmc-library/pthread_rwlock_tryrdlock/main.c diff --git a/regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_tryrdlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc rename to regression/cbmc-library/pthread_rwlock_tryrdlock/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_trywrlock-01/main.c b/regression/cbmc-library/pthread_rwlock_trywrlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_trywrlock-01/main.c rename to regression/cbmc-library/pthread_rwlock_trywrlock/main.c diff --git a/regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_trywrlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc rename to regression/cbmc-library/pthread_rwlock_trywrlock/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_unlock-01/main.c b/regression/cbmc-library/pthread_rwlock_unlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_unlock-01/main.c rename to regression/cbmc-library/pthread_rwlock_unlock/main.c diff --git a/regression/cbmc-library/pthread_rwlock_unlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_unlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_unlock-01/test.desc rename to regression/cbmc-library/pthread_rwlock_unlock/test.desc diff --git a/regression/cbmc-library/pthread_rwlock_wrlock-01/main.c b/regression/cbmc-library/pthread_rwlock_wrlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_rwlock_wrlock-01/main.c rename to regression/cbmc-library/pthread_rwlock_wrlock/main.c diff --git a/regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_wrlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc rename to regression/cbmc-library/pthread_rwlock_wrlock/test.desc diff --git a/regression/cbmc-library/pthread_setspecific-01/main.c b/regression/cbmc-library/pthread_setspecific/main.c similarity index 100% rename from regression/cbmc-library/pthread_setspecific-01/main.c rename to regression/cbmc-library/pthread_setspecific/main.c diff --git a/regression/cbmc-library/pthread_getspecific-01/test.desc b/regression/cbmc-library/pthread_setspecific/test.desc similarity index 100% rename from regression/cbmc-library/pthread_getspecific-01/test.desc rename to regression/cbmc-library/pthread_setspecific/test.desc diff --git a/regression/cbmc-library/pthread_spin_lock-01/main.c b/regression/cbmc-library/pthread_spin_lock/main.c similarity index 100% rename from regression/cbmc-library/pthread_spin_lock-01/main.c rename to regression/cbmc-library/pthread_spin_lock/main.c diff --git a/regression/cbmc-library/pthread_spin_lock-01/test.desc b/regression/cbmc-library/pthread_spin_lock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_spin_lock-01/test.desc rename to regression/cbmc-library/pthread_spin_lock/test.desc diff --git a/regression/cbmc-library/pthread_spin_trylock-01/main.c b/regression/cbmc-library/pthread_spin_trylock/main.c similarity index 100% rename from regression/cbmc-library/pthread_spin_trylock-01/main.c rename to regression/cbmc-library/pthread_spin_trylock/main.c diff --git a/regression/cbmc-library/pthread_spin_trylock-01/test.desc b/regression/cbmc-library/pthread_spin_trylock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_spin_trylock-01/test.desc rename to regression/cbmc-library/pthread_spin_trylock/test.desc diff --git a/regression/cbmc-library/pthread_spin_unlock-01/main.c b/regression/cbmc-library/pthread_spin_unlock/main.c similarity index 100% rename from regression/cbmc-library/pthread_spin_unlock-01/main.c rename to regression/cbmc-library/pthread_spin_unlock/main.c diff --git a/regression/cbmc-library/pthread_spin_unlock-01/test.desc b/regression/cbmc-library/pthread_spin_unlock/test.desc similarity index 100% rename from regression/cbmc-library/pthread_spin_unlock-01/test.desc rename to regression/cbmc-library/pthread_spin_unlock/test.desc diff --git a/regression/cbmc-library/putchar-01/main.c b/regression/cbmc-library/putchar/main.c similarity index 100% rename from regression/cbmc-library/putchar-01/main.c rename to regression/cbmc-library/putchar/main.c diff --git a/regression/cbmc-library/pthread_key_create-01/test.desc b/regression/cbmc-library/putchar/test.desc similarity index 100% rename from regression/cbmc-library/pthread_key_create-01/test.desc rename to regression/cbmc-library/putchar/test.desc diff --git a/regression/cbmc-library/puts-01/main.c b/regression/cbmc-library/puts/main.c similarity index 100% rename from regression/cbmc-library/puts-01/main.c rename to regression/cbmc-library/puts/main.c diff --git a/regression/cbmc-library/pthread_key_delete-01/test.desc b/regression/cbmc-library/puts/test.desc similarity index 100% rename from regression/cbmc-library/pthread_key_delete-01/test.desc rename to regression/cbmc-library/puts/test.desc diff --git a/regression/cbmc-library/rand-01/main.c b/regression/cbmc-library/rand/main.c similarity index 100% rename from regression/cbmc-library/rand-01/main.c rename to regression/cbmc-library/rand/main.c diff --git a/regression/cbmc-library/rand-01/test.desc b/regression/cbmc-library/rand/test.desc similarity index 100% rename from regression/cbmc-library/rand-01/test.desc rename to regression/cbmc-library/rand/test.desc diff --git a/regression/cbmc-library/rand_r-01/main.c b/regression/cbmc-library/rand_r/main.c similarity index 100% rename from regression/cbmc-library/rand_r-01/main.c rename to regression/cbmc-library/rand_r/main.c diff --git a/regression/cbmc-library/rand_r-01/test.desc b/regression/cbmc-library/rand_r/test.desc similarity index 100% rename from regression/cbmc-library/rand_r-01/test.desc rename to regression/cbmc-library/rand_r/test.desc diff --git a/regression/cbmc-library/random-01/main.c b/regression/cbmc-library/random/main.c similarity index 100% rename from regression/cbmc-library/random-01/main.c rename to regression/cbmc-library/random/main.c diff --git a/regression/cbmc-library/pthread_setspecific-01/test.desc b/regression/cbmc-library/random/test.desc similarity index 100% rename from regression/cbmc-library/pthread_setspecific-01/test.desc rename to regression/cbmc-library/random/test.desc diff --git a/regression/cbmc-library/read-01/main.c b/regression/cbmc-library/read/main.c similarity index 83% rename from regression/cbmc-library/read-01/main.c rename to regression/cbmc-library/read/main.c index a5cbdab443a..34ee48d381e 100644 --- a/regression/cbmc-library/read-01/main.c +++ b/regression/cbmc-library/read/main.c @@ -1,7 +1,7 @@ #ifdef _WIN32 -#include +# include #else -#include +# include #endif #include diff --git a/regression/cbmc-library/read-01/test.desc b/regression/cbmc-library/read/test.desc similarity index 100% rename from regression/cbmc-library/read-01/test.desc rename to regression/cbmc-library/read/test.desc diff --git a/regression/cbmc-library/realloc-02/test.desc b/regression/cbmc-library/realloc-02/test.desc deleted file mode 100644 index 915afae768a..00000000000 --- a/regression/cbmc-library/realloc-02/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---no-malloc-may-fail -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/realloc-01/main.c b/regression/cbmc-library/realloc/main_01.c similarity index 100% rename from regression/cbmc-library/realloc-01/main.c rename to regression/cbmc-library/realloc/main_01.c diff --git a/regression/cbmc-library/realloc-02/main.c b/regression/cbmc-library/realloc/main_02.c similarity index 100% rename from regression/cbmc-library/realloc-02/main.c rename to regression/cbmc-library/realloc/main_02.c diff --git a/regression/cbmc-library/realloc-03/main.c b/regression/cbmc-library/realloc/main_03.c similarity index 100% rename from regression/cbmc-library/realloc-03/main.c rename to regression/cbmc-library/realloc/main_03.c diff --git a/regression/cbmc-library/realloc-01/test.desc b/regression/cbmc-library/realloc/test_01.desc similarity index 90% rename from regression/cbmc-library/realloc-01/test.desc rename to regression/cbmc-library/realloc/test_01.desc index 915afae768a..899dfdff19b 100644 --- a/regression/cbmc-library/realloc-01/test.desc +++ b/regression/cbmc-library/realloc/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c --no-malloc-may-fail ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc b/regression/cbmc-library/realloc/test_02.desc similarity index 90% rename from regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc rename to regression/cbmc-library/realloc/test_02.desc index 915afae768a..d2d2b1b92f2 100644 --- a/regression/cbmc-library/equality_through_struct_containing_arrays3/test.desc +++ b/regression/cbmc-library/realloc/test_02.desc @@ -1,5 +1,5 @@ CORE -main.c +main_02.c --no-malloc-may-fail ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/realloc-03/test.desc b/regression/cbmc-library/realloc/test_03.desc similarity index 96% rename from regression/cbmc-library/realloc-03/test.desc rename to regression/cbmc-library/realloc/test_03.desc index 94f222a4b5f..05129eeb348 100644 --- a/regression/cbmc-library/realloc-03/test.desc +++ b/regression/cbmc-library/realloc/test_03.desc @@ -1,5 +1,5 @@ CORE -main.c +main_03.c ^EXIT=6$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/remainder-01/main.c b/regression/cbmc-library/remainder/main.c similarity index 100% rename from regression/cbmc-library/remainder-01/main.c rename to regression/cbmc-library/remainder/main.c diff --git a/regression/cbmc-library/putchar-01/test.desc b/regression/cbmc-library/remainder/test.desc similarity index 100% rename from regression/cbmc-library/putchar-01/test.desc rename to regression/cbmc-library/remainder/test.desc diff --git a/regression/cbmc-library/remainderf-01/main.c b/regression/cbmc-library/remainderf/main.c similarity index 100% rename from regression/cbmc-library/remainderf-01/main.c rename to regression/cbmc-library/remainderf/main.c diff --git a/regression/cbmc-library/puts-01/test.desc b/regression/cbmc-library/remainderf/test.desc similarity index 100% rename from regression/cbmc-library/puts-01/test.desc rename to regression/cbmc-library/remainderf/test.desc diff --git a/regression/cbmc-library/remainderl-01/main.c b/regression/cbmc-library/remainderl/main.c similarity index 100% rename from regression/cbmc-library/remainderl-01/main.c rename to regression/cbmc-library/remainderl/main.c diff --git a/regression/cbmc-library/random-01/test.desc b/regression/cbmc-library/remainderl/test.desc similarity index 100% rename from regression/cbmc-library/random-01/test.desc rename to regression/cbmc-library/remainderl/test.desc diff --git a/regression/cbmc-library/rewind-01/main.c b/regression/cbmc-library/rewind/main.c similarity index 100% rename from regression/cbmc-library/rewind-01/main.c rename to regression/cbmc-library/rewind/main.c diff --git a/regression/cbmc-library/remainder-01/test.desc b/regression/cbmc-library/rewind/test.desc similarity index 100% rename from regression/cbmc-library/remainder-01/test.desc rename to regression/cbmc-library/rewind/test.desc diff --git a/regression/cbmc-library/rint-01/main.c b/regression/cbmc-library/rint/main.c similarity index 100% rename from regression/cbmc-library/rint-01/main.c rename to regression/cbmc-library/rint/main.c diff --git a/regression/cbmc-library/remainderf-01/test.desc b/regression/cbmc-library/rint/test.desc similarity index 100% rename from regression/cbmc-library/remainderf-01/test.desc rename to regression/cbmc-library/rint/test.desc diff --git a/regression/cbmc-library/rintf-01/main.c b/regression/cbmc-library/rintf/main.c similarity index 100% rename from regression/cbmc-library/rintf-01/main.c rename to regression/cbmc-library/rintf/main.c diff --git a/regression/cbmc-library/remainderl-01/test.desc b/regression/cbmc-library/rintf/test.desc similarity index 100% rename from regression/cbmc-library/remainderl-01/test.desc rename to regression/cbmc-library/rintf/test.desc diff --git a/regression/cbmc-library/rintl-01/main.c b/regression/cbmc-library/rintl/main.c similarity index 100% rename from regression/cbmc-library/rintl-01/main.c rename to regression/cbmc-library/rintl/main.c diff --git a/regression/cbmc-library/rewind-01/test.desc b/regression/cbmc-library/rintl/test.desc similarity index 100% rename from regression/cbmc-library/rewind-01/test.desc rename to regression/cbmc-library/rintl/test.desc diff --git a/regression/cbmc-library/round-01/main.c b/regression/cbmc-library/round/main.c similarity index 100% rename from regression/cbmc-library/round-01/main.c rename to regression/cbmc-library/round/main.c diff --git a/regression/cbmc-library/floorl-01/test.desc b/regression/cbmc-library/round/test.desc similarity index 100% rename from regression/cbmc-library/floorl-01/test.desc rename to regression/cbmc-library/round/test.desc diff --git a/regression/cbmc-library/roundf-01/main.c b/regression/cbmc-library/roundf/main.c similarity index 100% rename from regression/cbmc-library/roundf-01/main.c rename to regression/cbmc-library/roundf/main.c diff --git a/regression/cbmc-library/inet_endian1/test.desc b/regression/cbmc-library/roundf/test.desc similarity index 100% rename from regression/cbmc-library/inet_endian1/test.desc rename to regression/cbmc-library/roundf/test.desc diff --git a/regression/cbmc-library/roundl-01/main.c b/regression/cbmc-library/roundl/main.c similarity index 100% rename from regression/cbmc-library/roundl-01/main.c rename to regression/cbmc-library/roundl/main.c diff --git a/regression/cbmc-library/round-01/test.desc b/regression/cbmc-library/roundl/test.desc similarity index 100% rename from regression/cbmc-library/round-01/test.desc rename to regression/cbmc-library/roundl/test.desc diff --git a/regression/cbmc-library/scanf-01/main.c b/regression/cbmc-library/scanf/main.c similarity index 100% rename from regression/cbmc-library/scanf-01/main.c rename to regression/cbmc-library/scanf/main.c diff --git a/regression/cbmc-library/scanf-01/test.desc b/regression/cbmc-library/scanf/test.desc similarity index 100% rename from regression/cbmc-library/scanf-01/test.desc rename to regression/cbmc-library/scanf/test.desc diff --git a/regression/cbmc-library/sem_destroy-01/main.c b/regression/cbmc-library/sem_destroy/main.c similarity index 100% rename from regression/cbmc-library/sem_destroy-01/main.c rename to regression/cbmc-library/sem_destroy/main.c diff --git a/regression/cbmc-library/rint-01/test.desc b/regression/cbmc-library/sem_destroy/test.desc similarity index 100% rename from regression/cbmc-library/rint-01/test.desc rename to regression/cbmc-library/sem_destroy/test.desc diff --git a/regression/cbmc-library/sem_getvalue-01/main.c b/regression/cbmc-library/sem_getvalue/main.c similarity index 100% rename from regression/cbmc-library/sem_getvalue-01/main.c rename to regression/cbmc-library/sem_getvalue/main.c diff --git a/regression/cbmc-library/rintf-01/test.desc b/regression/cbmc-library/sem_getvalue/test.desc similarity index 100% rename from regression/cbmc-library/rintf-01/test.desc rename to regression/cbmc-library/sem_getvalue/test.desc diff --git a/regression/cbmc-library/sem_init-01/main.c b/regression/cbmc-library/sem_init/main.c similarity index 100% rename from regression/cbmc-library/sem_init-01/main.c rename to regression/cbmc-library/sem_init/main.c diff --git a/regression/cbmc-library/rintl-01/test.desc b/regression/cbmc-library/sem_init/test.desc similarity index 100% rename from regression/cbmc-library/rintl-01/test.desc rename to regression/cbmc-library/sem_init/test.desc diff --git a/regression/cbmc-library/sem_post-01/main.c b/regression/cbmc-library/sem_post/main.c similarity index 100% rename from regression/cbmc-library/sem_post-01/main.c rename to regression/cbmc-library/sem_post/main.c diff --git a/regression/cbmc-library/sem_destroy-01/test.desc b/regression/cbmc-library/sem_post/test.desc similarity index 100% rename from regression/cbmc-library/sem_destroy-01/test.desc rename to regression/cbmc-library/sem_post/test.desc diff --git a/regression/cbmc-library/sem_post_multiple-01/main.c b/regression/cbmc-library/sem_post_multiple/main.c similarity index 100% rename from regression/cbmc-library/sem_post_multiple-01/main.c rename to regression/cbmc-library/sem_post_multiple/main.c diff --git a/regression/cbmc-library/sem_getvalue-01/test.desc b/regression/cbmc-library/sem_post_multiple/test.desc similarity index 100% rename from regression/cbmc-library/sem_getvalue-01/test.desc rename to regression/cbmc-library/sem_post_multiple/test.desc diff --git a/regression/cbmc-library/sem_timedwait-01/main.c b/regression/cbmc-library/sem_timedwait/main.c similarity index 100% rename from regression/cbmc-library/sem_timedwait-01/main.c rename to regression/cbmc-library/sem_timedwait/main.c diff --git a/regression/cbmc-library/sem_init-01/test.desc b/regression/cbmc-library/sem_timedwait/test.desc similarity index 100% rename from regression/cbmc-library/sem_init-01/test.desc rename to regression/cbmc-library/sem_timedwait/test.desc diff --git a/regression/cbmc-library/sem_trywait-01/main.c b/regression/cbmc-library/sem_trywait/main.c similarity index 100% rename from regression/cbmc-library/sem_trywait-01/main.c rename to regression/cbmc-library/sem_trywait/main.c diff --git a/regression/cbmc-library/sem_post-01/test.desc b/regression/cbmc-library/sem_trywait/test.desc similarity index 100% rename from regression/cbmc-library/sem_post-01/test.desc rename to regression/cbmc-library/sem_trywait/test.desc diff --git a/regression/cbmc-library/sem_wait-01/main.c b/regression/cbmc-library/sem_wait/main.c similarity index 100% rename from regression/cbmc-library/sem_wait-01/main.c rename to regression/cbmc-library/sem_wait/main.c diff --git a/regression/cbmc-library/sem_post_multiple-01/test.desc b/regression/cbmc-library/sem_wait/test.desc similarity index 100% rename from regression/cbmc-library/sem_post_multiple-01/test.desc rename to regression/cbmc-library/sem_wait/test.desc diff --git a/regression/cbmc-library/setjmp-01/main.c b/regression/cbmc-library/setjmp/main.c similarity index 100% rename from regression/cbmc-library/setjmp-01/main.c rename to regression/cbmc-library/setjmp/main.c diff --git a/regression/cbmc-library/setjmp-01/test.desc b/regression/cbmc-library/setjmp/test.desc similarity index 100% rename from regression/cbmc-library/setjmp-01/test.desc rename to regression/cbmc-library/setjmp/test.desc diff --git a/regression/cbmc-library/setlocale-01/main.c b/regression/cbmc-library/setlocale/main.c similarity index 100% rename from regression/cbmc-library/setlocale-01/main.c rename to regression/cbmc-library/setlocale/main.c diff --git a/regression/cbmc-library/sem_timedwait-01/test.desc b/regression/cbmc-library/setlocale/test.desc similarity index 100% rename from regression/cbmc-library/sem_timedwait-01/test.desc rename to regression/cbmc-library/setlocale/test.desc diff --git a/regression/cbmc-library/siglongjmp-01/main.c b/regression/cbmc-library/siglongjmp/main.c similarity index 100% rename from regression/cbmc-library/siglongjmp-01/main.c rename to regression/cbmc-library/siglongjmp/main.c diff --git a/regression/cbmc-library/siglongjmp-01/test.desc b/regression/cbmc-library/siglongjmp/test.desc similarity index 100% rename from regression/cbmc-library/siglongjmp-01/test.desc rename to regression/cbmc-library/siglongjmp/test.desc diff --git a/regression/cbmc-library/signbit-01/main.c b/regression/cbmc-library/signbit/main.c similarity index 100% rename from regression/cbmc-library/signbit-01/main.c rename to regression/cbmc-library/signbit/main.c diff --git a/regression/cbmc-library/fesetround-no-simp1-fix1/test.desc b/regression/cbmc-library/signbit/test.desc similarity index 100% rename from regression/cbmc-library/fesetround-no-simp1-fix1/test.desc rename to regression/cbmc-library/signbit/test.desc diff --git a/regression/cbmc-library/sigsetjmp-01/main.c b/regression/cbmc-library/sigsetjmp/main.c similarity index 100% rename from regression/cbmc-library/sigsetjmp-01/main.c rename to regression/cbmc-library/sigsetjmp/main.c diff --git a/regression/cbmc-library/sigsetjmp-01/test.desc b/regression/cbmc-library/sigsetjmp/test.desc similarity index 100% rename from regression/cbmc-library/sigsetjmp-01/test.desc rename to regression/cbmc-library/sigsetjmp/test.desc diff --git a/regression/cbmc-library/sin-01/main.c b/regression/cbmc-library/sin/main.c similarity index 100% rename from regression/cbmc-library/sin-01/main.c rename to regression/cbmc-library/sin/main.c diff --git a/regression/cbmc-library/fesetround-02/test.desc b/regression/cbmc-library/sin/test.desc similarity index 100% rename from regression/cbmc-library/fesetround-02/test.desc rename to regression/cbmc-library/sin/test.desc diff --git a/regression/cbmc-library/sinf-01/main.c b/regression/cbmc-library/sinf/main.c similarity index 100% rename from regression/cbmc-library/sinf-01/main.c rename to regression/cbmc-library/sinf/main.c diff --git a/regression/cbmc-library/sem_trywait-01/test.desc b/regression/cbmc-library/sinf/test.desc similarity index 100% rename from regression/cbmc-library/sem_trywait-01/test.desc rename to regression/cbmc-library/sinf/test.desc diff --git a/regression/cbmc-library/sinl-01/main.c b/regression/cbmc-library/sinl/main.c similarity index 100% rename from regression/cbmc-library/sinl-01/main.c rename to regression/cbmc-library/sinl/main.c diff --git a/regression/cbmc-library/sem_wait-01/test.desc b/regression/cbmc-library/sinl/test.desc similarity index 100% rename from regression/cbmc-library/sem_wait-01/test.desc rename to regression/cbmc-library/sinl/test.desc diff --git a/regression/cbmc-library/sleep-01/main.c b/regression/cbmc-library/sleep/main.c similarity index 100% rename from regression/cbmc-library/sleep-01/main.c rename to regression/cbmc-library/sleep/main.c diff --git a/regression/cbmc-library/sleep-01/test.desc b/regression/cbmc-library/sleep/test.desc similarity index 100% rename from regression/cbmc-library/sleep-01/test.desc rename to regression/cbmc-library/sleep/test.desc diff --git a/regression/cbmc-library/snprintf-01/main.c b/regression/cbmc-library/snprintf/main.c similarity index 100% rename from regression/cbmc-library/snprintf-01/main.c rename to regression/cbmc-library/snprintf/main.c diff --git a/regression/cbmc-library/snprintf-01/test.desc b/regression/cbmc-library/snprintf/test.desc similarity index 100% rename from regression/cbmc-library/snprintf-01/test.desc rename to regression/cbmc-library/snprintf/test.desc diff --git a/regression/cbmc-library/sqrt-01/main.c b/regression/cbmc-library/sqrt/main.c similarity index 100% rename from regression/cbmc-library/sqrt-01/main.c rename to regression/cbmc-library/sqrt/main.c diff --git a/regression/cbmc-library/setlocale-01/test.desc b/regression/cbmc-library/sqrt/test.desc similarity index 100% rename from regression/cbmc-library/setlocale-01/test.desc rename to regression/cbmc-library/sqrt/test.desc diff --git a/regression/cbmc-library/sqrtf-01/main.c b/regression/cbmc-library/sqrtf/main.c similarity index 100% rename from regression/cbmc-library/sqrtf-01/main.c rename to regression/cbmc-library/sqrtf/main.c diff --git a/regression/cbmc-library/sinf-01/test.desc b/regression/cbmc-library/sqrtf/test.desc similarity index 100% rename from regression/cbmc-library/sinf-01/test.desc rename to regression/cbmc-library/sqrtf/test.desc diff --git a/regression/cbmc-library/sqrtl-01/main.c b/regression/cbmc-library/sqrtl/main.c similarity index 100% rename from regression/cbmc-library/sqrtl-01/main.c rename to regression/cbmc-library/sqrtl/main.c diff --git a/regression/cbmc-library/sinl-01/test.desc b/regression/cbmc-library/sqrtl/test.desc similarity index 100% rename from regression/cbmc-library/sinl-01/test.desc rename to regression/cbmc-library/sqrtl/test.desc diff --git a/regression/cbmc-library/sscanf-01/main.c b/regression/cbmc-library/sscanf/main.c similarity index 100% rename from regression/cbmc-library/sscanf-01/main.c rename to regression/cbmc-library/sscanf/main.c diff --git a/regression/cbmc-library/sscanf-01/test.desc b/regression/cbmc-library/sscanf/test.desc similarity index 100% rename from regression/cbmc-library/sscanf-01/test.desc rename to regression/cbmc-library/sscanf/test.desc diff --git a/regression/cbmc-library/strcasecmp-01/main.c b/regression/cbmc-library/strcasecmp/main.c similarity index 100% rename from regression/cbmc-library/strcasecmp-01/main.c rename to regression/cbmc-library/strcasecmp/main.c diff --git a/regression/cbmc-library/sqrt-01/test.desc b/regression/cbmc-library/strcasecmp/test.desc similarity index 100% rename from regression/cbmc-library/sqrt-01/test.desc rename to regression/cbmc-library/strcasecmp/test.desc diff --git a/regression/cbmc-library/strcat-01/main.c b/regression/cbmc-library/strcat/main.c similarity index 100% rename from regression/cbmc-library/strcat-01/main.c rename to regression/cbmc-library/strcat/main.c diff --git a/regression/cbmc-library/strcat-01/test.desc b/regression/cbmc-library/strcat/test.desc similarity index 100% rename from regression/cbmc-library/strcat-01/test.desc rename to regression/cbmc-library/strcat/test.desc diff --git a/regression/cbmc-library/strchr-01/main.c b/regression/cbmc-library/strchr/main.c similarity index 100% rename from regression/cbmc-library/strchr-01/main.c rename to regression/cbmc-library/strchr/main.c diff --git a/regression/cbmc-library/strchr-01/test.desc b/regression/cbmc-library/strchr/test.desc similarity index 100% rename from regression/cbmc-library/strchr-01/test.desc rename to regression/cbmc-library/strchr/test.desc diff --git a/regression/cbmc-library/strcmp-01/main.c b/regression/cbmc-library/strcmp-01/main.c deleted file mode 100644 index 8350ad259f1..00000000000 --- a/regression/cbmc-library/strcmp-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - strcmp(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/String6/main.c b/regression/cbmc-library/strcmp/main.c similarity index 100% rename from regression/cbmc-library/String6/main.c rename to regression/cbmc-library/strcmp/main.c diff --git a/regression/cbmc-library/String6/strdup-calloc.desc b/regression/cbmc-library/strcmp/strdup-calloc.desc similarity index 100% rename from regression/cbmc-library/String6/strdup-calloc.desc rename to regression/cbmc-library/strcmp/strdup-calloc.desc diff --git a/regression/cbmc-library/String6/test.desc b/regression/cbmc-library/strcmp/test.desc similarity index 100% rename from regression/cbmc-library/String6/test.desc rename to regression/cbmc-library/strcmp/test.desc diff --git a/regression/cbmc-library/strcpy-01/main.c b/regression/cbmc-library/strcpy/main.c similarity index 100% rename from regression/cbmc-library/strcpy-01/main.c rename to regression/cbmc-library/strcpy/main.c diff --git a/regression/cbmc-library/strcpy-01/test.desc b/regression/cbmc-library/strcpy/test.desc similarity index 100% rename from regression/cbmc-library/strcpy-01/test.desc rename to regression/cbmc-library/strcpy/test.desc diff --git a/regression/cbmc-library/strdup-01/main.c b/regression/cbmc-library/strdup/main.c similarity index 100% rename from regression/cbmc-library/strdup-01/main.c rename to regression/cbmc-library/strdup/main.c diff --git a/regression/cbmc-library/sqrtf-01/test.desc b/regression/cbmc-library/strdup/test.desc similarity index 100% rename from regression/cbmc-library/sqrtf-01/test.desc rename to regression/cbmc-library/strdup/test.desc diff --git a/regression/cbmc-library/strerror-01/main.c b/regression/cbmc-library/strerror/main.c similarity index 100% rename from regression/cbmc-library/strerror-01/main.c rename to regression/cbmc-library/strerror/main.c diff --git a/regression/cbmc-library/sqrtl-01/test.desc b/regression/cbmc-library/strerror/test.desc similarity index 100% rename from regression/cbmc-library/sqrtl-01/test.desc rename to regression/cbmc-library/strerror/test.desc diff --git a/regression/cbmc-library/strftime-01/main.c b/regression/cbmc-library/strftime/main.c similarity index 100% rename from regression/cbmc-library/strftime-01/main.c rename to regression/cbmc-library/strftime/main.c diff --git a/regression/cbmc-library/strftime-01/test.desc b/regression/cbmc-library/strftime/test.desc similarity index 100% rename from regression/cbmc-library/strftime-01/test.desc rename to regression/cbmc-library/strftime/test.desc diff --git a/regression/cbmc-library/strlen-01/main.c b/regression/cbmc-library/strlen/main_01.c similarity index 100% rename from regression/cbmc-library/strlen-01/main.c rename to regression/cbmc-library/strlen/main_01.c diff --git a/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc b/regression/cbmc-library/strlen/test-c-with-string-abstraction_02.desc similarity index 96% rename from regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc rename to regression/cbmc-library/strlen/test-c-with-string-abstraction_02.desc index 02383fd37d9..e20dd6392aa 100644 --- a/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc +++ b/regression/cbmc-library/strlen/test-c-with-string-abstraction_02.desc @@ -1,5 +1,5 @@ CORE -test.c +test_02.c --string-abstraction --show-goto-functions ASSIGN strlen#return_value := \*strlen::s::s#str\.length - pointer_offset\(strlen::s\) ^EXIT=0$ diff --git a/regression/cbmc-library/strlen-02/test-c-without-string-abstraction.desc b/regression/cbmc-library/strlen/test-c-without-string-abstraction_02.desc similarity index 96% rename from regression/cbmc-library/strlen-02/test-c-without-string-abstraction.desc rename to regression/cbmc-library/strlen/test-c-without-string-abstraction_02.desc index d2b76c017fd..0db771224d1 100644 --- a/regression/cbmc-library/strlen-02/test-c-without-string-abstraction.desc +++ b/regression/cbmc-library/strlen/test-c-without-string-abstraction_02.desc @@ -1,5 +1,5 @@ CORE -test.c +test_02.c --show-goto-functions IF ¬\(cast\(\*\(strlen::s \+ cast\(strlen::1::len, signedbv\[.*\]\)\), signedbv\[32\]\) ≠ 0\) THEN GOTO 2 ^EXIT=0$ diff --git a/regression/cbmc-library/timegm-01/test.desc b/regression/cbmc-library/strlen/test_01.desc similarity index 91% rename from regression/cbmc-library/timegm-01/test.desc rename to regression/cbmc-library/strlen/test_01.desc index 9542d988e8d..2e1ae5a9f54 100644 --- a/regression/cbmc-library/timegm-01/test.desc +++ b/regression/cbmc-library/strlen/test_01.desc @@ -1,5 +1,5 @@ KNOWNBUG -main.c +main_01.c --pointer-check --bounds-check ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/strlen-02/test.c b/regression/cbmc-library/strlen/test_02.c similarity index 100% rename from regression/cbmc-library/strlen-02/test.c rename to regression/cbmc-library/strlen/test_02.c diff --git a/regression/cbmc-library/strncasecmp-01/main.c b/regression/cbmc-library/strncasecmp/main.c similarity index 100% rename from regression/cbmc-library/strncasecmp-01/main.c rename to regression/cbmc-library/strncasecmp/main.c diff --git a/regression/cbmc-library/strncasecmp-01/test.desc b/regression/cbmc-library/strncasecmp/test.desc similarity index 100% rename from regression/cbmc-library/strncasecmp-01/test.desc rename to regression/cbmc-library/strncasecmp/test.desc diff --git a/regression/cbmc-library/strncat-01/main.c b/regression/cbmc-library/strncat/main.c similarity index 100% rename from regression/cbmc-library/strncat-01/main.c rename to regression/cbmc-library/strncat/main.c diff --git a/regression/cbmc-library/strncat-01/test.desc b/regression/cbmc-library/strncat/test.desc similarity index 100% rename from regression/cbmc-library/strncat-01/test.desc rename to regression/cbmc-library/strncat/test.desc diff --git a/regression/cbmc-library/strncmp-01/main.c b/regression/cbmc-library/strncmp/main.c similarity index 83% rename from regression/cbmc-library/strncmp-01/main.c rename to regression/cbmc-library/strncmp/main.c index ee405e1dda6..b5451f0b321 100644 --- a/regression/cbmc-library/strncmp-01/main.c +++ b/regression/cbmc-library/strncmp/main.c @@ -1,9 +1,6 @@ #include #include -#include -#include - int main() { char a[] = "abc"; diff --git a/regression/cbmc-library/strncmp-01/test.desc b/regression/cbmc-library/strncmp/test.desc similarity index 100% rename from regression/cbmc-library/strncmp-01/test.desc rename to regression/cbmc-library/strncmp/test.desc diff --git a/regression/cbmc-library/strncpy-01/main.c b/regression/cbmc-library/strncpy/main.c similarity index 100% rename from regression/cbmc-library/strncpy-01/main.c rename to regression/cbmc-library/strncpy/main.c diff --git a/regression/cbmc-library/strcasecmp-01/test.desc b/regression/cbmc-library/strncpy/test.desc similarity index 100% rename from regression/cbmc-library/strcasecmp-01/test.desc rename to regression/cbmc-library/strncpy/test.desc diff --git a/regression/cbmc-library/strrchr-01/main.c b/regression/cbmc-library/strrchr/main.c similarity index 100% rename from regression/cbmc-library/strrchr-01/main.c rename to regression/cbmc-library/strrchr/main.c diff --git a/regression/cbmc-library/strcmp-01/test.desc b/regression/cbmc-library/strrchr/test.desc similarity index 100% rename from regression/cbmc-library/strcmp-01/test.desc rename to regression/cbmc-library/strrchr/test.desc diff --git a/regression/cbmc-library/strtol-01/main.c b/regression/cbmc-library/strtol/main_01.c similarity index 100% rename from regression/cbmc-library/strtol-01/main.c rename to regression/cbmc-library/strtol/main_01.c diff --git a/regression/cbmc-library/strtol-02/main.c b/regression/cbmc-library/strtol/main_02.c similarity index 100% rename from regression/cbmc-library/strtol-02/main.c rename to regression/cbmc-library/strtol/main_02.c diff --git a/regression/cbmc-library/truncf-01/test.desc b/regression/cbmc-library/strtol/test_01.desc similarity index 88% rename from regression/cbmc-library/truncf-01/test.desc rename to regression/cbmc-library/strtol/test_01.desc index 9efefbc7362..861203074c1 100644 --- a/regression/cbmc-library/truncf-01/test.desc +++ b/regression/cbmc-library/strtol/test_01.desc @@ -1,5 +1,5 @@ CORE -main.c +main_01.c ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/strtol-02/test.desc b/regression/cbmc-library/strtol/test_02.desc similarity index 95% rename from regression/cbmc-library/strtol-02/test.desc rename to regression/cbmc-library/strtol/test_02.desc index 92776cb5537..ad8192ea2d0 100644 --- a/regression/cbmc-library/strtol-02/test.desc +++ b/regression/cbmc-library/strtol/test_02.desc @@ -1,5 +1,5 @@ CORE -main.c +main_02.c --signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/sysconf-01/main.c b/regression/cbmc-library/sysconf/main.c similarity index 100% rename from regression/cbmc-library/sysconf-01/main.c rename to regression/cbmc-library/sysconf/main.c diff --git a/regression/cbmc-library/sysconf-01/test.desc b/regression/cbmc-library/sysconf/test.desc similarity index 100% rename from regression/cbmc-library/sysconf-01/test.desc rename to regression/cbmc-library/sysconf/test.desc diff --git a/regression/cbmc-library/syslog-01/__syslog_chk.desc b/regression/cbmc-library/syslog/__syslog_chk.desc similarity index 100% rename from regression/cbmc-library/syslog-01/__syslog_chk.desc rename to regression/cbmc-library/syslog/__syslog_chk.desc diff --git a/regression/cbmc-library/syslog-01/main.c b/regression/cbmc-library/syslog/main.c similarity index 100% rename from regression/cbmc-library/syslog-01/main.c rename to regression/cbmc-library/syslog/main.c diff --git a/regression/cbmc-library/syslog-01/test.desc b/regression/cbmc-library/syslog/test.desc similarity index 100% rename from regression/cbmc-library/syslog-01/test.desc rename to regression/cbmc-library/syslog/test.desc diff --git a/regression/cbmc-library/thrd_create-01/main.c b/regression/cbmc-library/thrd_create/main.c similarity index 100% rename from regression/cbmc-library/thrd_create-01/main.c rename to regression/cbmc-library/thrd_create/main.c diff --git a/regression/cbmc-library/strdup-01/test.desc b/regression/cbmc-library/thrd_create/test.desc similarity index 100% rename from regression/cbmc-library/strdup-01/test.desc rename to regression/cbmc-library/thrd_create/test.desc diff --git a/regression/cbmc-library/thrd_current-01/main.c b/regression/cbmc-library/thrd_current/main.c similarity index 100% rename from regression/cbmc-library/thrd_current-01/main.c rename to regression/cbmc-library/thrd_current/main.c diff --git a/regression/cbmc-library/strerror-01/test.desc b/regression/cbmc-library/thrd_current/test.desc similarity index 100% rename from regression/cbmc-library/strerror-01/test.desc rename to regression/cbmc-library/thrd_current/test.desc diff --git a/regression/cbmc-library/thrd_equal-01/main.c b/regression/cbmc-library/thrd_equal/main.c similarity index 100% rename from regression/cbmc-library/thrd_equal-01/main.c rename to regression/cbmc-library/thrd_equal/main.c diff --git a/regression/cbmc-library/strlen-01/test.desc b/regression/cbmc-library/thrd_equal/test.desc similarity index 100% rename from regression/cbmc-library/strlen-01/test.desc rename to regression/cbmc-library/thrd_equal/test.desc diff --git a/regression/cbmc-library/thrd_exit-01/main.c b/regression/cbmc-library/thrd_exit/main.c similarity index 100% rename from regression/cbmc-library/thrd_exit-01/main.c rename to regression/cbmc-library/thrd_exit/main.c diff --git a/regression/cbmc-library/strncpy-01/test.desc b/regression/cbmc-library/thrd_exit/test.desc similarity index 100% rename from regression/cbmc-library/strncpy-01/test.desc rename to regression/cbmc-library/thrd_exit/test.desc diff --git a/regression/cbmc-library/thrd_sleep-01/main.c b/regression/cbmc-library/thrd_sleep/main.c similarity index 100% rename from regression/cbmc-library/thrd_sleep-01/main.c rename to regression/cbmc-library/thrd_sleep/main.c diff --git a/regression/cbmc-library/strrchr-01/test.desc b/regression/cbmc-library/thrd_sleep/test.desc similarity index 100% rename from regression/cbmc-library/strrchr-01/test.desc rename to regression/cbmc-library/thrd_sleep/test.desc diff --git a/regression/cbmc-library/thrd_yield-01/main.c b/regression/cbmc-library/thrd_yield/main.c similarity index 100% rename from regression/cbmc-library/thrd_yield-01/main.c rename to regression/cbmc-library/thrd_yield/main.c diff --git a/regression/cbmc-library/thrd_create-01/test.desc b/regression/cbmc-library/thrd_yield/test.desc similarity index 100% rename from regression/cbmc-library/thrd_create-01/test.desc rename to regression/cbmc-library/thrd_yield/test.desc diff --git a/regression/cbmc-library/time-01/main.c b/regression/cbmc-library/time/main.c similarity index 100% rename from regression/cbmc-library/time-01/main.c rename to regression/cbmc-library/time/main.c diff --git a/regression/cbmc-library/time-01/test.desc b/regression/cbmc-library/time/test.desc similarity index 100% rename from regression/cbmc-library/time-01/test.desc rename to regression/cbmc-library/time/test.desc diff --git a/regression/cbmc-library/timegm-01/main.c b/regression/cbmc-library/timegm/main.c similarity index 100% rename from regression/cbmc-library/timegm-01/main.c rename to regression/cbmc-library/timegm/main.c diff --git a/regression/cbmc-library/thrd_current-01/test.desc b/regression/cbmc-library/timegm/test.desc similarity index 100% rename from regression/cbmc-library/thrd_current-01/test.desc rename to regression/cbmc-library/timegm/test.desc diff --git a/regression/cbmc-library/tolower-01/main.c b/regression/cbmc-library/tolower/main.c similarity index 100% rename from regression/cbmc-library/tolower-01/main.c rename to regression/cbmc-library/tolower/main.c diff --git a/regression/cbmc-library/tolower-01/test.desc b/regression/cbmc-library/tolower/test.desc similarity index 100% rename from regression/cbmc-library/tolower-01/test.desc rename to regression/cbmc-library/tolower/test.desc diff --git a/regression/cbmc-library/toupper-01/main.c b/regression/cbmc-library/toupper/main.c similarity index 100% rename from regression/cbmc-library/toupper-01/main.c rename to regression/cbmc-library/toupper/main.c diff --git a/regression/cbmc-library/toupper-01/test.desc b/regression/cbmc-library/toupper/test.desc similarity index 100% rename from regression/cbmc-library/toupper-01/test.desc rename to regression/cbmc-library/toupper/test.desc diff --git a/regression/cbmc-library/trunc-01/main.c b/regression/cbmc-library/trunc/main.c similarity index 100% rename from regression/cbmc-library/trunc-01/main.c rename to regression/cbmc-library/trunc/main.c diff --git a/regression/cbmc-library/roundf-01/test.desc b/regression/cbmc-library/trunc/test.desc similarity index 100% rename from regression/cbmc-library/roundf-01/test.desc rename to regression/cbmc-library/trunc/test.desc diff --git a/regression/cbmc-library/truncf-01/main.c b/regression/cbmc-library/truncf/main.c similarity index 100% rename from regression/cbmc-library/truncf-01/main.c rename to regression/cbmc-library/truncf/main.c diff --git a/regression/cbmc-library/roundl-01/test.desc b/regression/cbmc-library/truncf/test.desc similarity index 100% rename from regression/cbmc-library/roundl-01/test.desc rename to regression/cbmc-library/truncf/test.desc diff --git a/regression/cbmc-library/truncl-01/test.desc b/regression/cbmc-library/truncl-01/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/cbmc-library/truncl-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/truncl-01/main.c b/regression/cbmc-library/truncl/main.c similarity index 100% rename from regression/cbmc-library/truncl-01/main.c rename to regression/cbmc-library/truncl/main.c diff --git a/regression/cbmc-library/strtol-01/test.desc b/regression/cbmc-library/truncl/test.desc similarity index 100% rename from regression/cbmc-library/strtol-01/test.desc rename to regression/cbmc-library/truncl/test.desc diff --git a/regression/cbmc-library/unlink-01/test.desc b/regression/cbmc-library/unlink-01/test.desc deleted file mode 100644 index 9542d988e8d..00000000000 --- a/regression/cbmc-library/unlink-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/unlink-01/main.c b/regression/cbmc-library/unlink/main.c similarity index 100% rename from regression/cbmc-library/unlink-01/main.c rename to regression/cbmc-library/unlink/main.c diff --git a/regression/cbmc-library/thrd_equal-01/test.desc b/regression/cbmc-library/unlink/test.desc similarity index 100% rename from regression/cbmc-library/thrd_equal-01/test.desc rename to regression/cbmc-library/unlink/test.desc diff --git a/regression/cbmc-library/usleep-01/main.c b/regression/cbmc-library/usleep/main.c similarity index 100% rename from regression/cbmc-library/usleep-01/main.c rename to regression/cbmc-library/usleep/main.c diff --git a/regression/cbmc-library/usleep-01/test.desc b/regression/cbmc-library/usleep/test.desc similarity index 100% rename from regression/cbmc-library/usleep-01/test.desc rename to regression/cbmc-library/usleep/test.desc diff --git a/regression/cbmc-library/valloc-01/test.desc b/regression/cbmc-library/valloc-01/test.desc deleted file mode 100644 index 9542d988e8d..00000000000 --- a/regression/cbmc-library/valloc-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/valloc-01/main.c b/regression/cbmc-library/valloc/main.c similarity index 100% rename from regression/cbmc-library/valloc-01/main.c rename to regression/cbmc-library/valloc/main.c diff --git a/regression/cbmc-library/thrd_exit-01/test.desc b/regression/cbmc-library/valloc/test.desc similarity index 100% rename from regression/cbmc-library/thrd_exit-01/test.desc rename to regression/cbmc-library/valloc/test.desc diff --git a/regression/cbmc-library/vasprintf-01/main.c b/regression/cbmc-library/vasprintf/main.c similarity index 100% rename from regression/cbmc-library/vasprintf-01/main.c rename to regression/cbmc-library/vasprintf/main.c diff --git a/regression/cbmc-library/vasprintf-01/test.desc b/regression/cbmc-library/vasprintf/test.desc similarity index 100% rename from regression/cbmc-library/vasprintf-01/test.desc rename to regression/cbmc-library/vasprintf/test.desc diff --git a/regression/cbmc-library/vdprintf-01/main.c b/regression/cbmc-library/vdprintf/main.c similarity index 100% rename from regression/cbmc-library/vdprintf-01/main.c rename to regression/cbmc-library/vdprintf/main.c diff --git a/regression/cbmc-library/vdprintf-01/test.desc b/regression/cbmc-library/vdprintf/test.desc similarity index 100% rename from regression/cbmc-library/vdprintf-01/test.desc rename to regression/cbmc-library/vdprintf/test.desc diff --git a/regression/cbmc-library/vfprintf-01/__vfprintf_chk.desc b/regression/cbmc-library/vfprintf/__vfprintf_chk.desc similarity index 100% rename from regression/cbmc-library/vfprintf-01/__vfprintf_chk.desc rename to regression/cbmc-library/vfprintf/__vfprintf_chk.desc diff --git a/regression/cbmc-library/vfprintf-01/main.c b/regression/cbmc-library/vfprintf/main.c similarity index 100% rename from regression/cbmc-library/vfprintf-01/main.c rename to regression/cbmc-library/vfprintf/main.c diff --git a/regression/cbmc-library/vfprintf-01/test.desc b/regression/cbmc-library/vfprintf/test.desc similarity index 100% rename from regression/cbmc-library/vfprintf-01/test.desc rename to regression/cbmc-library/vfprintf/test.desc diff --git a/regression/cbmc-library/vfscanf-01/main.c b/regression/cbmc-library/vfscanf/main.c similarity index 100% rename from regression/cbmc-library/vfscanf-01/main.c rename to regression/cbmc-library/vfscanf/main.c diff --git a/regression/cbmc-library/vfscanf-01/test.desc b/regression/cbmc-library/vfscanf/test.desc similarity index 100% rename from regression/cbmc-library/vfscanf-01/test.desc rename to regression/cbmc-library/vfscanf/test.desc diff --git a/regression/cbmc-library/vscanf-01/main.c b/regression/cbmc-library/vscanf/main.c similarity index 100% rename from regression/cbmc-library/vscanf-01/main.c rename to regression/cbmc-library/vscanf/main.c diff --git a/regression/cbmc-library/vscanf-01/test.desc b/regression/cbmc-library/vscanf/test.desc similarity index 100% rename from regression/cbmc-library/vscanf-01/test.desc rename to regression/cbmc-library/vscanf/test.desc diff --git a/regression/cbmc-library/vsnprintf-01/main.c b/regression/cbmc-library/vsnprintf/main.c similarity index 100% rename from regression/cbmc-library/vsnprintf-01/main.c rename to regression/cbmc-library/vsnprintf/main.c diff --git a/regression/cbmc-library/vsnprintf-01/test.desc b/regression/cbmc-library/vsnprintf/test.desc similarity index 100% rename from regression/cbmc-library/vsnprintf-01/test.desc rename to regression/cbmc-library/vsnprintf/test.desc diff --git a/regression/cbmc-library/vsscanf-01/main.c b/regression/cbmc-library/vsscanf/main.c similarity index 100% rename from regression/cbmc-library/vsscanf-01/main.c rename to regression/cbmc-library/vsscanf/main.c diff --git a/regression/cbmc-library/vsscanf-01/test.desc b/regression/cbmc-library/vsscanf/test.desc similarity index 100% rename from regression/cbmc-library/vsscanf-01/test.desc rename to regression/cbmc-library/vsscanf/test.desc diff --git a/regression/cbmc-library/warn-01/test.desc b/regression/cbmc-library/warn-01/test.desc deleted file mode 100644 index 9542d988e8d..00000000000 --- a/regression/cbmc-library/warn-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/warn-01/main.c b/regression/cbmc-library/warn/main.c similarity index 100% rename from regression/cbmc-library/warn-01/main.c rename to regression/cbmc-library/warn/main.c diff --git a/regression/cbmc-library/thrd_sleep-01/test.desc b/regression/cbmc-library/warn/test.desc similarity index 100% rename from regression/cbmc-library/thrd_sleep-01/test.desc rename to regression/cbmc-library/warn/test.desc diff --git a/regression/cbmc-library/warnx-01/test.desc b/regression/cbmc-library/warnx-01/test.desc deleted file mode 100644 index 9542d988e8d..00000000000 --- a/regression/cbmc-library/warnx-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/warnx-01/main.c b/regression/cbmc-library/warnx/main.c similarity index 100% rename from regression/cbmc-library/warnx-01/main.c rename to regression/cbmc-library/warnx/main.c diff --git a/regression/cbmc-library/thrd_yield-01/test.desc b/regression/cbmc-library/warnx/test.desc similarity index 100% rename from regression/cbmc-library/thrd_yield-01/test.desc rename to regression/cbmc-library/warnx/test.desc diff --git a/regression/cbmc-library/write-01/main.c b/regression/cbmc-library/write/main.c similarity index 100% rename from regression/cbmc-library/write-01/main.c rename to regression/cbmc-library/write/main.c diff --git a/regression/cbmc-library/write-01/test.desc b/regression/cbmc-library/write/test.desc similarity index 100% rename from regression/cbmc-library/write-01/test.desc rename to regression/cbmc-library/write/test.desc diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh index 9d973341585..6883984ae26 100755 --- a/src/ansi-c/library_check.sh +++ b/src/ansi-c/library_check.sh @@ -70,14 +70,14 @@ perl -p -i -e 's/^fopen64\n//' __functions # fopen perl -p -i -e 's/^freopen64\n//' __functions # freopen perl -p -i -e 's/^mmap64\n//' __functions # mmap perl -p -i -e 's/^munmap\n//' __functions # mmap-01 -perl -p -i -e 's/^__fgets_chk\n//' __functions # fgets-01/__fgets_chk.desc -perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc -perl -p -i -e 's/^__fread_chk\n//' __functions # fread-01/__fread_chk.desc -perl -p -i -e 's/^__printf_chk\n//' __functions # printf-01/__printf_chk.desc -perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc -perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog-01/test.desc +perl -p -i -e 's/^__fgets_chk\n//' __functions # fgets/__fgets_chk.desc +perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf/__fprintf_chk.desc +perl -p -i -e 's/^__fread_chk\n//' __functions # fread/__fread_chk.desc +perl -p -i -e 's/^__printf_chk\n//' __functions # printf/__printf_chk.desc +perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog/__syslog_chk.desc +perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog/test.desc perl -p -i -e 's/^__time64\n//' __functions # time -perl -p -i -e 's/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.desc +perl -p -i -e 's/^__vfprintf_chk\n//' __functions # vfprintf/__vfprintf_chk.desc # Some functions are covered by tests in other folders: perl -p -i -e 's/^__spawned_thread\n//' __functions # any pthread_create tests @@ -101,7 +101,7 @@ perl -p -i -e 's/^_mm_setr_epi(16|32)\n//' __functions # cbmc/SIMD1 perl -p -i -e 's/^_mm_setr_pi16\n//' __functions # cbmc/SIMD1 perl -p -i -e 's/^_mm_subs_ep[iu]16\n//' __functions # cbmc/SIMD1 -ls ../../regression/cbmc-library/ | grep -- - | cut -f1 -d- | sort -u > __tests +ls ../../regression/cbmc-library/ | egrep -v '(Makefile|CMakeLists.txt)' | sort -u > __tests diff -u __tests __functions ec="${?}" rm __functions __tests