From 7ed77de2c58fdf1a821a6707c38a7396626636ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 Mar 2021 23:18:17 +0000 Subject: [PATCH 1/3] BV refinement: include XML output in schema Make sure tags do not cause validation errors. --- doc/assets/xml_spec.xsd | 3 +++ 1 file changed, 3 insertions(+) diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd index 40f7c078ea4..ba251ee4e29 100644 --- a/doc/assets/xml_spec.xsd +++ b/doc/assets/xml_spec.xsd @@ -181,6 +181,8 @@ + + @@ -190,6 +192,7 @@ + From 94138b56f925c82ed12803891c11ee956ece0bb2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Mar 2021 19:58:40 +0000 Subject: [PATCH 2/3] Add array-refinement regression tests Moving these tests from a dedicated folder to cbmc to run them, also making use of all three configurations that the cbmc folder is being tested with. (Unnecessary) GCC attributes were removed to make sure tests can be used on all platforms. --- regression/array-refinement/Makefile | 14 -------------- .../{array-refinement => cbmc}/Array_UF1/main.c | 0 .../{array-refinement => cbmc}/Array_UF1/test.desc | 0 .../{array-refinement => cbmc}/Array_UF10/main.c | 2 +- .../Array_UF10/test.desc | 0 .../{array-refinement => cbmc}/Array_UF11/main.c | 2 +- .../Array_UF11/test.desc | 0 .../{array-refinement => cbmc}/Array_UF12/main.c | 2 +- .../Array_UF12/test.desc | 0 .../{array-refinement => cbmc}/Array_UF13/main.c | 2 +- .../Array_UF13/test.desc | 0 .../{array-refinement => cbmc}/Array_UF14/main.c | 2 +- .../Array_UF14/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF15/main.c | 2 +- .../Array_UF18 => cbmc/Array_UF15}/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF16/main.c | 2 +- .../Array_UF16/test.desc | 0 .../{array-refinement => cbmc}/Array_UF17/main.c | 2 +- .../Array_UF17/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF18/main.c | 2 +- .../Array_UF15 => cbmc/Array_UF18}/test.desc | 0 .../{array-refinement => cbmc}/Array_UF19/main.c | 2 +- .../Array_UF6 => cbmc/Array_UF19}/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF2/main.c | 0 .../{array-refinement => cbmc}/Array_UF2/test.desc | 0 .../{array-refinement => cbmc}/Array_UF20/main.c | 2 +- .../Array_UF20/test.desc | 0 .../{array-refinement => cbmc}/Array_UF3/main.c | 0 .../{array-refinement => cbmc}/Array_UF3/test.desc | 0 .../{array-refinement => cbmc}/Array_UF4/main.c | 2 +- .../{array-refinement => cbmc}/Array_UF4/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF5/main.c | 2 +- .../{array-refinement => cbmc}/Array_UF5/test.desc | 0 .../{array-refinement => cbmc}/Array_UF6/main.c | 2 +- .../Array_UF7 => cbmc/Array_UF6}/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF7/main.c | 2 +- .../Array_UF19 => cbmc/Array_UF7}/test.desc | 0 .../{array-refinement => cbmc}/Array_UF8/main.c | 2 +- .../{array-refinement => cbmc}/Array_UF8/test.desc | 2 +- .../{array-refinement => cbmc}/Array_UF9/main.c | 2 +- .../{array-refinement => cbmc}/Array_UF9/test.desc | 0 41 files changed, 24 insertions(+), 38 deletions(-) delete mode 100644 regression/array-refinement/Makefile rename regression/{array-refinement => cbmc}/Array_UF1/main.c (100%) rename regression/{array-refinement => cbmc}/Array_UF1/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF10/main.c (80%) rename regression/{array-refinement => cbmc}/Array_UF10/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF11/main.c (84%) rename regression/{array-refinement => cbmc}/Array_UF11/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF12/main.c (88%) rename regression/{array-refinement => cbmc}/Array_UF12/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF13/main.c (85%) rename regression/{array-refinement => cbmc}/Array_UF13/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF14/main.c (93%) rename regression/{array-refinement => cbmc}/Array_UF14/test.desc (87%) rename regression/{array-refinement => cbmc}/Array_UF15/main.c (93%) rename regression/{array-refinement/Array_UF18 => cbmc/Array_UF15}/test.desc (87%) rename regression/{array-refinement => cbmc}/Array_UF16/main.c (88%) rename regression/{array-refinement => cbmc}/Array_UF16/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF17/main.c (97%) rename regression/{array-refinement => cbmc}/Array_UF17/test.desc (87%) rename regression/{array-refinement => cbmc}/Array_UF18/main.c (87%) rename regression/{array-refinement/Array_UF15 => cbmc/Array_UF18}/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF19/main.c (97%) rename regression/{array-refinement/Array_UF6 => cbmc/Array_UF19}/test.desc (87%) rename regression/{array-refinement => cbmc}/Array_UF2/main.c (100%) rename regression/{array-refinement => cbmc}/Array_UF2/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF20/main.c (89%) rename regression/{array-refinement => cbmc}/Array_UF20/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF3/main.c (100%) rename regression/{array-refinement => cbmc}/Array_UF3/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF4/main.c (86%) rename regression/{array-refinement => cbmc}/Array_UF4/test.desc (93%) rename regression/{array-refinement => cbmc}/Array_UF5/main.c (86%) rename regression/{array-refinement => cbmc}/Array_UF5/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF6/main.c (94%) rename regression/{array-refinement/Array_UF7 => cbmc/Array_UF6}/test.desc (87%) rename regression/{array-refinement => cbmc}/Array_UF7/main.c (90%) rename regression/{array-refinement/Array_UF19 => cbmc/Array_UF7}/test.desc (100%) rename regression/{array-refinement => cbmc}/Array_UF8/main.c (89%) rename regression/{array-refinement => cbmc}/Array_UF8/test.desc (93%) rename regression/{array-refinement => cbmc}/Array_UF9/main.c (87%) rename regression/{array-refinement => cbmc}/Array_UF9/test.desc (100%) diff --git a/regression/array-refinement/Makefile b/regression/array-refinement/Makefile deleted file mode 100644 index cb87039e7d3..00000000000 --- a/regression/array-refinement/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -default: tests.log - -TOOL = "../../../src/cbmc/cbmc" - -test: - @../test.pl -c $(TOOL) - -tests.log: ../test.pl - @../test.pl -c $(TOOL) - -clean: - find . -name '*.out' -execdir $(RM) '{}' \; - find . -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log diff --git a/regression/array-refinement/Array_UF1/main.c b/regression/cbmc/Array_UF1/main.c similarity index 100% rename from regression/array-refinement/Array_UF1/main.c rename to regression/cbmc/Array_UF1/main.c diff --git a/regression/array-refinement/Array_UF1/test.desc b/regression/cbmc/Array_UF1/test.desc similarity index 100% rename from regression/array-refinement/Array_UF1/test.desc rename to regression/cbmc/Array_UF1/test.desc diff --git a/regression/array-refinement/Array_UF10/main.c b/regression/cbmc/Array_UF10/main.c similarity index 80% rename from regression/array-refinement/Array_UF10/main.c rename to regression/cbmc/Array_UF10/main.c index 935392f577c..ca2bcca46c8 100644 --- a/regression/array-refinement/Array_UF10/main.c +++ b/regression/cbmc/Array_UF10/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); int __VERIFIER_nondet_int(); diff --git a/regression/array-refinement/Array_UF10/test.desc b/regression/cbmc/Array_UF10/test.desc similarity index 100% rename from regression/array-refinement/Array_UF10/test.desc rename to regression/cbmc/Array_UF10/test.desc diff --git a/regression/array-refinement/Array_UF11/main.c b/regression/cbmc/Array_UF11/main.c similarity index 84% rename from regression/array-refinement/Array_UF11/main.c rename to regression/cbmc/Array_UF11/main.c index f4a3234cf70..ff784c2e478 100644 --- a/regression/array-refinement/Array_UF11/main.c +++ b/regression/cbmc/Array_UF11/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF11/test.desc b/regression/cbmc/Array_UF11/test.desc similarity index 100% rename from regression/array-refinement/Array_UF11/test.desc rename to regression/cbmc/Array_UF11/test.desc diff --git a/regression/array-refinement/Array_UF12/main.c b/regression/cbmc/Array_UF12/main.c similarity index 88% rename from regression/array-refinement/Array_UF12/main.c rename to regression/cbmc/Array_UF12/main.c index 8932da571d6..a285be2addc 100644 --- a/regression/array-refinement/Array_UF12/main.c +++ b/regression/cbmc/Array_UF12/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF12/test.desc b/regression/cbmc/Array_UF12/test.desc similarity index 100% rename from regression/array-refinement/Array_UF12/test.desc rename to regression/cbmc/Array_UF12/test.desc diff --git a/regression/array-refinement/Array_UF13/main.c b/regression/cbmc/Array_UF13/main.c similarity index 85% rename from regression/array-refinement/Array_UF13/main.c rename to regression/cbmc/Array_UF13/main.c index d64444acb02..3518f564281 100644 --- a/regression/array-refinement/Array_UF13/main.c +++ b/regression/cbmc/Array_UF13/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF13/test.desc b/regression/cbmc/Array_UF13/test.desc similarity index 100% rename from regression/array-refinement/Array_UF13/test.desc rename to regression/cbmc/Array_UF13/test.desc diff --git a/regression/array-refinement/Array_UF14/main.c b/regression/cbmc/Array_UF14/main.c similarity index 93% rename from regression/array-refinement/Array_UF14/main.c rename to regression/cbmc/Array_UF14/main.c index 1335adf8785..903985606f2 100644 --- a/regression/array-refinement/Array_UF14/main.c +++ b/regression/cbmc/Array_UF14/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); extern void __VERIFIER_assume(int); void __VERIFIER_assert(int cond) { diff --git a/regression/array-refinement/Array_UF14/test.desc b/regression/cbmc/Array_UF14/test.desc similarity index 87% rename from regression/array-refinement/Array_UF14/test.desc rename to regression/cbmc/Array_UF14/test.desc index 3830439f347..2a5c51a9f90 100644 --- a/regression/array-refinement/Array_UF14/test.desc +++ b/regression/cbmc/Array_UF14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE thorough-paths main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 6 ^EXIT=10$ diff --git a/regression/array-refinement/Array_UF15/main.c b/regression/cbmc/Array_UF15/main.c similarity index 93% rename from regression/array-refinement/Array_UF15/main.c rename to regression/cbmc/Array_UF15/main.c index fb0e63d3b50..5760853643c 100644 --- a/regression/array-refinement/Array_UF15/main.c +++ b/regression/cbmc/Array_UF15/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); extern void __VERIFIER_assume(int); void __VERIFIER_assert(int cond) { diff --git a/regression/array-refinement/Array_UF18/test.desc b/regression/cbmc/Array_UF15/test.desc similarity index 87% rename from regression/array-refinement/Array_UF18/test.desc rename to regression/cbmc/Array_UF15/test.desc index 61e3418f5e6..15690b94615 100644 --- a/regression/array-refinement/Array_UF18/test.desc +++ b/regression/cbmc/Array_UF15/test.desc @@ -1,4 +1,4 @@ -CORE +CORE thorough-paths main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 11 ^EXIT=0$ diff --git a/regression/array-refinement/Array_UF16/main.c b/regression/cbmc/Array_UF16/main.c similarity index 88% rename from regression/array-refinement/Array_UF16/main.c rename to regression/cbmc/Array_UF16/main.c index aea6c758494..650fdcb2a24 100644 --- a/regression/array-refinement/Array_UF16/main.c +++ b/regression/cbmc/Array_UF16/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); extern int __VERIFIER_nondet_int(void); void __VERIFIER_assert(int cond) { diff --git a/regression/array-refinement/Array_UF16/test.desc b/regression/cbmc/Array_UF16/test.desc similarity index 100% rename from regression/array-refinement/Array_UF16/test.desc rename to regression/cbmc/Array_UF16/test.desc diff --git a/regression/array-refinement/Array_UF17/main.c b/regression/cbmc/Array_UF17/main.c similarity index 97% rename from regression/array-refinement/Array_UF17/main.c rename to regression/cbmc/Array_UF17/main.c index ec315007a04..d9de7f6c4a7 100644 --- a/regression/array-refinement/Array_UF17/main.c +++ b/regression/cbmc/Array_UF17/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF17/test.desc b/regression/cbmc/Array_UF17/test.desc similarity index 87% rename from regression/array-refinement/Array_UF17/test.desc rename to regression/cbmc/Array_UF17/test.desc index 4b585860724..e9939c1e8c3 100644 --- a/regression/array-refinement/Array_UF17/test.desc +++ b/regression/cbmc/Array_UF17/test.desc @@ -1,4 +1,4 @@ -CORE +CORE thorough-paths main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 9 ^EXIT=0$ diff --git a/regression/array-refinement/Array_UF18/main.c b/regression/cbmc/Array_UF18/main.c similarity index 87% rename from regression/array-refinement/Array_UF18/main.c rename to regression/cbmc/Array_UF18/main.c index 63362ce18d8..b8f912dd4c4 100644 --- a/regression/array-refinement/Array_UF18/main.c +++ b/regression/cbmc/Array_UF18/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF15/test.desc b/regression/cbmc/Array_UF18/test.desc similarity index 100% rename from regression/array-refinement/Array_UF15/test.desc rename to regression/cbmc/Array_UF18/test.desc diff --git a/regression/array-refinement/Array_UF19/main.c b/regression/cbmc/Array_UF19/main.c similarity index 97% rename from regression/array-refinement/Array_UF19/main.c rename to regression/cbmc/Array_UF19/main.c index 0b8ac7904eb..c64f5d897cb 100644 --- a/regression/array-refinement/Array_UF19/main.c +++ b/regression/cbmc/Array_UF19/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF6/test.desc b/regression/cbmc/Array_UF19/test.desc similarity index 87% rename from regression/array-refinement/Array_UF6/test.desc rename to regression/cbmc/Array_UF19/test.desc index c47f81c71cc..d92ab778129 100644 --- a/regression/array-refinement/Array_UF6/test.desc +++ b/regression/cbmc/Array_UF19/test.desc @@ -1,4 +1,4 @@ -CORE +CORE thorough-paths main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 3 ^EXIT=10$ diff --git a/regression/array-refinement/Array_UF2/main.c b/regression/cbmc/Array_UF2/main.c similarity index 100% rename from regression/array-refinement/Array_UF2/main.c rename to regression/cbmc/Array_UF2/main.c diff --git a/regression/array-refinement/Array_UF2/test.desc b/regression/cbmc/Array_UF2/test.desc similarity index 100% rename from regression/array-refinement/Array_UF2/test.desc rename to regression/cbmc/Array_UF2/test.desc diff --git a/regression/array-refinement/Array_UF20/main.c b/regression/cbmc/Array_UF20/main.c similarity index 89% rename from regression/array-refinement/Array_UF20/main.c rename to regression/cbmc/Array_UF20/main.c index d44354af92b..4a84870cd2a 100644 --- a/regression/array-refinement/Array_UF20/main.c +++ b/regression/cbmc/Array_UF20/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); extern char __VERIFIER_nondet_char(); diff --git a/regression/array-refinement/Array_UF20/test.desc b/regression/cbmc/Array_UF20/test.desc similarity index 100% rename from regression/array-refinement/Array_UF20/test.desc rename to regression/cbmc/Array_UF20/test.desc diff --git a/regression/array-refinement/Array_UF3/main.c b/regression/cbmc/Array_UF3/main.c similarity index 100% rename from regression/array-refinement/Array_UF3/main.c rename to regression/cbmc/Array_UF3/main.c diff --git a/regression/array-refinement/Array_UF3/test.desc b/regression/cbmc/Array_UF3/test.desc similarity index 100% rename from regression/array-refinement/Array_UF3/test.desc rename to regression/cbmc/Array_UF3/test.desc diff --git a/regression/array-refinement/Array_UF4/main.c b/regression/cbmc/Array_UF4/main.c similarity index 86% rename from regression/array-refinement/Array_UF4/main.c rename to regression/cbmc/Array_UF4/main.c index 02db0e1a5b1..2514f7aa237 100644 --- a/regression/array-refinement/Array_UF4/main.c +++ b/regression/cbmc/Array_UF4/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF4/test.desc b/regression/cbmc/Array_UF4/test.desc similarity index 93% rename from regression/array-refinement/Array_UF4/test.desc rename to regression/cbmc/Array_UF4/test.desc index cc6143ea6d1..72779529649 100644 --- a/regression/array-refinement/Array_UF4/test.desc +++ b/regression/cbmc/Array_UF4/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 2 ^EXIT=0$ diff --git a/regression/array-refinement/Array_UF5/main.c b/regression/cbmc/Array_UF5/main.c similarity index 86% rename from regression/array-refinement/Array_UF5/main.c rename to regression/cbmc/Array_UF5/main.c index 096648bf99c..af30761db42 100644 --- a/regression/array-refinement/Array_UF5/main.c +++ b/regression/cbmc/Array_UF5/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF5/test.desc b/regression/cbmc/Array_UF5/test.desc similarity index 100% rename from regression/array-refinement/Array_UF5/test.desc rename to regression/cbmc/Array_UF5/test.desc diff --git a/regression/array-refinement/Array_UF6/main.c b/regression/cbmc/Array_UF6/main.c similarity index 94% rename from regression/array-refinement/Array_UF6/main.c rename to regression/cbmc/Array_UF6/main.c index 641bf3bcad8..dffc8e211fe 100644 --- a/regression/array-refinement/Array_UF6/main.c +++ b/regression/cbmc/Array_UF6/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF7/test.desc b/regression/cbmc/Array_UF6/test.desc similarity index 87% rename from regression/array-refinement/Array_UF7/test.desc rename to regression/cbmc/Array_UF6/test.desc index c47f81c71cc..d92ab778129 100644 --- a/regression/array-refinement/Array_UF7/test.desc +++ b/regression/cbmc/Array_UF6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE thorough-paths main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 3 ^EXIT=10$ diff --git a/regression/array-refinement/Array_UF7/main.c b/regression/cbmc/Array_UF7/main.c similarity index 90% rename from regression/array-refinement/Array_UF7/main.c rename to regression/cbmc/Array_UF7/main.c index 7425e0dcd15..dd0bfdb9cba 100644 --- a/regression/array-refinement/Array_UF7/main.c +++ b/regression/cbmc/Array_UF7/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF19/test.desc b/regression/cbmc/Array_UF7/test.desc similarity index 100% rename from regression/array-refinement/Array_UF19/test.desc rename to regression/cbmc/Array_UF7/test.desc diff --git a/regression/array-refinement/Array_UF8/main.c b/regression/cbmc/Array_UF8/main.c similarity index 89% rename from regression/array-refinement/Array_UF8/main.c rename to regression/cbmc/Array_UF8/main.c index b8695b7848b..d18579af8b9 100644 --- a/regression/array-refinement/Array_UF8/main.c +++ b/regression/cbmc/Array_UF8/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF8/test.desc b/regression/cbmc/Array_UF8/test.desc similarity index 93% rename from regression/array-refinement/Array_UF8/test.desc rename to regression/cbmc/Array_UF8/test.desc index 715300a8de6..ba128759099 100644 --- a/regression/array-refinement/Array_UF8/test.desc +++ b/regression/cbmc/Array_UF8/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 6 ^EXIT=0$ diff --git a/regression/array-refinement/Array_UF9/main.c b/regression/cbmc/Array_UF9/main.c similarity index 87% rename from regression/array-refinement/Array_UF9/main.c rename to regression/cbmc/Array_UF9/main.c index 93cdba8bd31..661993f4933 100644 --- a/regression/array-refinement/Array_UF9/main.c +++ b/regression/cbmc/Array_UF9/main.c @@ -1,4 +1,4 @@ -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error(); void __VERIFIER_assert(int cond) { if (!(cond)) { diff --git a/regression/array-refinement/Array_UF9/test.desc b/regression/cbmc/Array_UF9/test.desc similarity index 100% rename from regression/array-refinement/Array_UF9/test.desc rename to regression/cbmc/Array_UF9/test.desc From c32457323e82accf8760555e22e4dcff2e2d3894 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 17 Mar 2021 00:31:27 +0000 Subject: [PATCH 3/3] clang-format recently moved tests --- regression/cbmc/Array_UF1/main.c | 11 ++-- regression/cbmc/Array_UF10/main.c | 15 ++++-- regression/cbmc/Array_UF11/main.c | 41 ++++++++------- regression/cbmc/Array_UF12/main.c | 61 ++++++++++++---------- regression/cbmc/Array_UF13/main.c | 23 +++++--- regression/cbmc/Array_UF14/main.c | 46 ++++++++-------- regression/cbmc/Array_UF15/main.c | 43 +++++++-------- regression/cbmc/Array_UF16/main.c | 21 ++++---- regression/cbmc/Array_UF17/main.c | 87 ++++++++++++++++++------------- regression/cbmc/Array_UF18/main.c | 15 +++--- regression/cbmc/Array_UF19/main.c | 84 ++++++++++++++++------------- regression/cbmc/Array_UF2/main.c | 11 ++-- regression/cbmc/Array_UF20/main.c | 17 +++--- regression/cbmc/Array_UF3/main.c | 10 ++-- regression/cbmc/Array_UF4/main.c | 26 +++++---- regression/cbmc/Array_UF5/main.c | 26 +++++---- regression/cbmc/Array_UF6/main.c | 69 +++++++++++++----------- regression/cbmc/Array_UF7/main.c | 51 ++++++++++-------- regression/cbmc/Array_UF8/main.c | 49 +++++++++-------- regression/cbmc/Array_UF9/main.c | 37 ++++++++----- 20 files changed, 420 insertions(+), 323 deletions(-) diff --git a/regression/cbmc/Array_UF1/main.c b/regression/cbmc/Array_UF1/main.c index 27c5f15cbd8..64742bcd719 100644 --- a/regression/cbmc/Array_UF1/main.c +++ b/regression/cbmc/Array_UF1/main.c @@ -1,13 +1,14 @@ int main() { int a[10], b[10]; - int x,y,z; - __CPROVER_assume(2<=y && y<=4); - __CPROVER_assume(6<=z && z<=8); + int x, y, z; + __CPROVER_assume(2 <= y && y <= 4); + __CPROVER_assume(6 <= z && z <= 8); b[y] = x; b[z] = x; - for(unsigned i = 0;i<10;i++) { + for(unsigned i = 0; i < 10; i++) + { a[i] = b[i]; } - __CPROVER_assert(a[y]==a[z], "a[y]==a[z]"); + __CPROVER_assert(a[y] == a[z], "a[y]==a[z]"); } diff --git a/regression/cbmc/Array_UF10/main.c b/regression/cbmc/Array_UF10/main.c index ca2bcca46c8..d55b6932cff 100644 --- a/regression/cbmc/Array_UF10/main.c +++ b/regression/cbmc/Array_UF10/main.c @@ -2,14 +2,16 @@ extern void __VERIFIER_error(); int __VERIFIER_nondet_int(); - char x[100], y[100]; - int i,j,k; +char x[100], y[100]; +int i, j, k; -void main() { +void main() +{ k = __VERIFIER_nondet_int(); i = 0; - while(x[i] != 0){ + while(x[i] != 0) + { y[i] = x[i]; i++; } @@ -17,5 +19,8 @@ void main() { if(k >= 0 && k < i) if(y[k] == 0) - {ERROR: __VERIFIER_error();} + { + ERROR: + __VERIFIER_error(); + } } diff --git a/regression/cbmc/Array_UF11/main.c b/regression/cbmc/Array_UF11/main.c index ff784c2e478..cb6f88fe814 100644 --- a/regression/cbmc/Array_UF11/main.c +++ b/regression/cbmc/Array_UF11/main.c @@ -1,32 +1,33 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } _Bool __VERIFIER_nondet_bool(); -int main(){ - int a[5]; - int len=0; - _Bool c=__VERIFIER_nondet_bool(); - int i; +int main() +{ + int a[5]; + int len = 0; + _Bool c = __VERIFIER_nondet_bool(); + int i; + while(c) + { + if(len == 4) + len = 0; - while(c){ - - if (len==4) - len =0; - - a[len]=0; - - len++; - } - __VERIFIER_assert(len==5); - return 1; - + a[len] = 0; + len++; + } + __VERIFIER_assert(len == 5); + return 1; } diff --git a/regression/cbmc/Array_UF12/main.c b/regression/cbmc/Array_UF12/main.c index a285be2addc..def2fa51b97 100644 --- a/regression/cbmc/Array_UF12/main.c +++ b/regression/cbmc/Array_UF12/main.c @@ -1,40 +1,47 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } int b; _Bool __VERIFIER_nondet_bool(); -int main(){ - _Bool k=__VERIFIER_nondet_bool(); - int i,n,j; - int a[1025]; +int main() +{ + _Bool k = __VERIFIER_nondet_bool(); + int i, n, j; + int a[1025]; - if (k){ - n=0; - } else { - n=1023; - } - - i=0; + if(k) + { + n = 0; + } + else + { + n = 1023; + } - while ( i <= n){ - i++; - j= j +2; - } + i = 0; - a[i]=0; - a[j]=0; - __VERIFIER_assert(j<1025); - a[b]=0; - if (b >= 0 && b < 1023) - a[b]=1; - else - a[b%1023] =1; + while(i <= n) + { + i++; + j = j + 2; + } - return 1; + a[i] = 0; + a[j] = 0; + __VERIFIER_assert(j < 1025); + a[b] = 0; + if(b >= 0 && b < 1023) + a[b] = 1; + else + a[b % 1023] = 1; + return 1; } diff --git a/regression/cbmc/Array_UF13/main.c b/regression/cbmc/Array_UF13/main.c index 3518f564281..b467c63f7f4 100644 --- a/regression/cbmc/Array_UF13/main.c +++ b/regression/cbmc/Array_UF13/main.c @@ -1,21 +1,26 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } int __VERIFIER_nondet_int(); - char x[100], y[100]; - int i,j,k; +char x[100], y[100]; +int i, j, k; -void main() { +void main() +{ k = __VERIFIER_nondet_int(); i = 0; - while(x[i] != 0){ + while(x[i] != 0) + { y[i] = x[i]; i++; } @@ -23,5 +28,7 @@ void main() { if(k >= 0 && k < i) if(y[k] != 0) - {__VERIFIER_assert(0);} + { + __VERIFIER_assert(0); + } } diff --git a/regression/cbmc/Array_UF14/main.c b/regression/cbmc/Array_UF14/main.c index 903985606f2..767bf718c96 100644 --- a/regression/cbmc/Array_UF14/main.c +++ b/regression/cbmc/Array_UF14/main.c @@ -1,59 +1,57 @@ extern void __VERIFIER_error(); extern void __VERIFIER_assume(int); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } - - extern char __VERIFIER_nondet_char(); main() { char string_A[5], string_B[5]; - int i, j, nc_A, nc_B, found=0; + int i, j, nc_A, nc_B, found = 0; + for(i = 0; i < 5; i++) + string_A[i] = __VERIFIER_nondet_char(); + __VERIFIER_assume(string_A[5 - 1] == '\0'); - for(i=0; i<5; i++) - string_A[i]=__VERIFIER_nondet_char(); - __VERIFIER_assume(string_A[5 -1]=='\0'); - - for(i=0; i<5; i++) - string_B[i]=__VERIFIER_nondet_char(); - __VERIFIER_assume(string_B[5 -1]=='\0'); + for(i = 0; i < 5; i++) + string_B[i] = __VERIFIER_nondet_char(); + __VERIFIER_assume(string_B[5 - 1] == '\0'); nc_A = 0; - while(string_A[nc_A]!='\0') + while(string_A[nc_A] != '\0') nc_A++; nc_B = 0; - while(string_B[nc_B]!='\0') + while(string_B[nc_B] != '\0') nc_B++; __VERIFIER_assume(nc_B >= nc_A); - - i=j=0; - while((inc_B-1)< nc_B - 1) << i; __VERIFIER_assert(found == 0 || found == 1); - } diff --git a/regression/cbmc/Array_UF15/main.c b/regression/cbmc/Array_UF15/main.c index 5760853643c..6849b8b3aff 100644 --- a/regression/cbmc/Array_UF15/main.c +++ b/regression/cbmc/Array_UF15/main.c @@ -1,56 +1,57 @@ extern void __VERIFIER_error(); extern void __VERIFIER_assume(int); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } - extern char __VERIFIER_nondet_char(); main() { char string_A[5], string_B[5]; - int i, j, nc_A, nc_B, found=0; + int i, j, nc_A, nc_B, found = 0; - for(i=0; i<5; i++) - string_A[i]=__VERIFIER_nondet_char(); - __VERIFIER_assume(string_A[5 -1]=='\0'); + for(i = 0; i < 5; i++) + string_A[i] = __VERIFIER_nondet_char(); + __VERIFIER_assume(string_A[5 - 1] == '\0'); - for(i=0; i<5; i++) - string_B[i]=__VERIFIER_nondet_char(); - __VERIFIER_assume(string_B[5 -1]=='\0'); + for(i = 0; i < 5; i++) + string_B[i] = __VERIFIER_nondet_char(); + __VERIFIER_assume(string_B[5 - 1] == '\0'); nc_A = 0; - while(string_A[nc_A]!='\0') + while(string_A[nc_A] != '\0') nc_A++; nc_B = 0; - while(string_B[nc_B]!='\0') + while(string_B[nc_B] != '\0') nc_B++; __VERIFIER_assume(nc_B >= nc_A); - - i=j=0; - while((inc_B-1); + found = (j > nc_B - 1); __VERIFIER_assert(found == 0 || found == 1); } diff --git a/regression/cbmc/Array_UF16/main.c b/regression/cbmc/Array_UF16/main.c index 650fdcb2a24..6fac8ee376e 100644 --- a/regression/cbmc/Array_UF16/main.c +++ b/regression/cbmc/Array_UF16/main.c @@ -1,9 +1,12 @@ extern void __VERIFIER_error(); extern int __VERIFIER_nondet_int(void); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } @@ -15,15 +18,15 @@ int main() int A[M], B[M], C[M]; unsigned int i; - for(i=0;i=2) { + while((str[start] == ' ') || (str[start] == '\t')) + start++; + if(str[start] == '"') + start++; + j = i - 1; + while((0 < j) && ((str[j] == ' ') || (str[j] == '\t'))) + j--; + if((0 < j) && (str[j] == '"')) + j--; + if(start <= j) + { + if(j - start + 1 >= 2) + { return -1; } - r_strncpy(str2, str+start, j-start+1); - str2[j-start+1] = 0; - } else { + r_strncpy(str2, str + start, j - start + 1); + str2[j - start + 1] = 0; + } + else + { return -1; } - start = i+1; + start = i + 1; } - } while (str[i] != 0); + } while(str[i] != 0); return 0; } -int main () +int main() { - char A [2 + 2 + 4 +1]; + char A[2 + 2 + 4 + 1]; A[2 + 2 + 4] = 0; - parse_expression_list (A); + parse_expression_list(A); return 0; } diff --git a/regression/cbmc/Array_UF18/main.c b/regression/cbmc/Array_UF18/main.c index b8f912dd4c4..e60e37d6bf2 100644 --- a/regression/cbmc/Array_UF18/main.c +++ b/regression/cbmc/Array_UF18/main.c @@ -1,12 +1,15 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } -int main (void) +int main(void) { char in[11]; char *s; @@ -18,7 +21,7 @@ int main (void) s = in; i = 0; c = in[idx_in]; - while (('0' <= c) && (c <= '9')) + while(('0' <= c) && (c <= '9')) { j = c - '0'; i = i * 10U + j; @@ -26,6 +29,6 @@ int main (void) c = in[idx_in]; } - __VERIFIER_assert (i >= 0); + __VERIFIER_assert(i >= 0); return 0; } diff --git a/regression/cbmc/Array_UF19/main.c b/regression/cbmc/Array_UF19/main.c index c64f5d897cb..40b092cda2e 100644 --- a/regression/cbmc/Array_UF19/main.c +++ b/regression/cbmc/Array_UF19/main.c @@ -1,8 +1,11 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } @@ -11,31 +14,32 @@ typedef int bool; char *strchr(const char *s, int c); char *strrchr(const char *s, int c); char *strstr(const char *haystack, const char *needle); -char *strncpy (char *dest, const char *src, size_t n); -char *strncpy_ptr (char *dest, const char *src, size_t n); -char *strcpy (char *dest, const char *src); +char *strncpy(char *dest, const char *src, size_t n); +char *strncpy_ptr(char *dest, const char *src, size_t n); +char *strcpy(char *dest, const char *src); unsigned strlen(const char *s); -int strncmp (const char *s1, const char *s2, size_t n); -int strcmp (const char *s1, const char *s2); +int strncmp(const char *s1, const char *s2, size_t n); +int strcmp(const char *s1, const char *s2); char *strcat(char *dest, const char *src); void *memcpy(void *dest, const void *src, size_t n); -int isascii (int c); -int isspace (int c); -int getc ( ); -char *strrand (char *s); -int istrrand (char *s); +int isascii(int c); +int isspace(int c); +int getc(); +char *strrand(char *s); +int istrrand(char *s); int istrchr(const char *s, int c); int istrrchr(const char *s, int c); -int istrncmp (const char *s1, int start, const char *s2, size_t n); +int istrncmp(const char *s1, int start, const char *s2, size_t n); int istrstr(const char *haystack, const char *needle); -char *r_strncpy (char *dest, const char *src, size_t n); -char *r_strcpy (char *dest, const char *src); +char *r_strncpy(char *dest, const char *src, size_t n); +char *r_strcpy(char *dest, const char *src); char *r_strcat(char *dest, const char *src); char *r_strncat(char *dest, const char *src, size_t n); void *r_memcpy(void *dest, const void *src, size_t n); typedef unsigned int u_int; typedef unsigned char u_int8_t; -struct ieee80211_scan_entry { +struct ieee80211_scan_entry +{ u_int8_t *se_rsn_ie; }; typedef int NSS_STATUS; @@ -46,34 +50,44 @@ struct sockaddr_un }; static int parse_expression_list(char *str) { - int start=0, i=-1, j=-1; + int start = 0, i = -1, j = -1; char str2[2]; - if (!str) return -1; - do { + if(!str) + return -1; + do + { i++; - switch(str[i]) { + switch(str[i]) + { case 0: - while ((str[start] == ' ') || (str[start] == '\t')) start++; - if (str[start] == '"') start++; - j = i-1; - while ((0 < j) && ((str[j] == ' ') || (str[j] == '\t'))) j--; - if ((0 < j) && (str[j] == '"')) j--; - if (start<=j) { - r_strncpy(str2, str+start, j-start+1); + while((str[start] == ' ') || (str[start] == '\t')) + start++; + if(str[start] == '"') + start++; + j = i - 1; + while((0 < j) && ((str[j] == ' ') || (str[j] == '\t'))) + j--; + if((0 < j) && (str[j] == '"')) + j--; + if(start <= j) + { + r_strncpy(str2, str + start, j - start + 1); __VERIFIER_assert(j - start + 1 < 2); - str2[j-start+1] = 0; - } else { + str2[j - start + 1] = 0; + } + else + { return -1; } - start = i+1; + start = i + 1; } - } while (str[i] != 0); + } while(str[i] != 0); return 0; } -int main () +int main() { - char A [2 + 2 + 4 +1]; + char A[2 + 2 + 4 + 1]; A[2 + 2 + 4] = 0; - parse_expression_list (A); + parse_expression_list(A); return 0; } diff --git a/regression/cbmc/Array_UF2/main.c b/regression/cbmc/Array_UF2/main.c index b2f11c543c0..e3ddf0d1d64 100644 --- a/regression/cbmc/Array_UF2/main.c +++ b/regression/cbmc/Array_UF2/main.c @@ -1,13 +1,14 @@ int main() { int a[4], b[4]; - int x,y,z; - __CPROVER_assume(1<=y && y<=3); - __CPROVER_assume(0<=z && z<=2); + int x, y, z; + __CPROVER_assume(1 <= y && y <= 3); + __CPROVER_assume(0 <= z && z <= 2); b[y] = x; b[z] = x; - for(unsigned i = 0;i<4;i++) { + for(unsigned i = 0; i < 4; i++) + { a[i] = b[i]; } - __CPROVER_assert(a[y]==a[z], "a[y]==a[z]"); + __CPROVER_assert(a[y] == a[z], "a[y]==a[z]"); } diff --git a/regression/cbmc/Array_UF20/main.c b/regression/cbmc/Array_UF20/main.c index 4a84870cd2a..baa7d5a216a 100644 --- a/regression/cbmc/Array_UF20/main.c +++ b/regression/cbmc/Array_UF20/main.c @@ -2,28 +2,31 @@ extern void __VERIFIER_error(); extern char __VERIFIER_nondet_char(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } -int main (void) +int main(void) { char in[11]; char *s; unsigned char c; int i, j; int idx_in; - for (i = 0; i < 11; i++) + for(i = 0; i < 11; i++) in[i] = __VERIFIER_nondet_char(); in[10] = 0; idx_in = 0; s = in; i = 0; c = in[idx_in]; - while (('0' <= c) && (c <= '9')) + while(('0' <= c) && (c <= '9')) { j = c - '0'; i = i * 10U + j; @@ -31,6 +34,6 @@ int main (void) c = in[idx_in]; } - __VERIFIER_assert (i >= 0); + __VERIFIER_assert(i >= 0); return 0; } diff --git a/regression/cbmc/Array_UF3/main.c b/regression/cbmc/Array_UF3/main.c index 4db1610f46e..fb705f95364 100644 --- a/regression/cbmc/Array_UF3/main.c +++ b/regression/cbmc/Array_UF3/main.c @@ -1,19 +1,19 @@ main() { unsigned int N; - __CPROVER_assume(N>0); + __CPROVER_assume(N > 0); - unsigned int j,k; + unsigned int j, k; int matrix[N], max; max = __VERIFIER_nondet_int(); - for(j=0;j=max) + if(matrix[j] >= max) max = matrix[j]; } - assert(matrix[0]=menor); + __VERIFIER_assert(array[0] >= menor); } diff --git a/regression/cbmc/Array_UF5/main.c b/regression/cbmc/Array_UF5/main.c index af30761db42..6b4142b5e36 100644 --- a/regression/cbmc/Array_UF5/main.c +++ b/regression/cbmc/Array_UF5/main.c @@ -1,8 +1,11 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } @@ -10,18 +13,19 @@ int __VERIFIER_nondet_int(); main() { - unsigned int SIZE=1; - unsigned int j,k; + unsigned int SIZE = 1; + unsigned int j, k; int array[SIZE], menor; menor = __VERIFIER_nondet_int(); - for(j=0;jmenor); + __VERIFIER_assert(array[0] > menor); } diff --git a/regression/cbmc/Array_UF6/main.c b/regression/cbmc/Array_UF6/main.c index dffc8e211fe..1d5a83e93a7 100644 --- a/regression/cbmc/Array_UF6/main.c +++ b/regression/cbmc/Array_UF6/main.c @@ -1,60 +1,67 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } int INFINITY = 899; unsigned int __VERIFIER_nondet_uint(); -void main(){ +void main() +{ int nodecount = __VERIFIER_nondet_int(); int edgecount = __VERIFIER_nondet_int(); __VERIFIER_assume(0 <= nodecount <= 4); __VERIFIER_assume(0 <= edgecount <= 19); int source = 0; - int Source[20] = {0,4,1,1,0,0,1,3,4,4,2,2,3,0,0,3,1,2,2,3}; - int Dest[20] = {1,3,4,1,1,4,3,4,3,0,0,0,0,2,3,0,2,1,0,4}; - int Weight[20] = {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}; + int Source[20] = {0, 4, 1, 1, 0, 0, 1, 3, 4, 4, 2, 2, 3, 0, 0, 3, 1, 2, 2, 3}; + int Dest[20] = {1, 3, 4, 1, 1, 4, 3, 4, 3, 0, 0, 0, 0, 2, 3, 0, 2, 1, 0, 4}; + int Weight[20] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, + 10, 11, 12, 13, 14, 15, 16, 17, 18, 19}; int distance[5]; - int x,y; - int i,j; + int x, y; + int i, j; - for(i = 0; i < nodecount; i++){ - if(i == source){ + for(i = 0; i < nodecount; i++) + { + if(i == source) + { distance[i] = 0; } - else { + else + { distance[i] = INFINITY; } } for(i = 0; i < nodecount; i++) + { + for(j = 0; j < edgecount; j++) { - for(j = 0; j < edgecount; j++) - { - x = Dest[j]; - y = Source[j]; - if(distance[x] > distance[y] + Weight[j]) - { - distance[x] = -1; - } - } + x = Dest[j]; + y = Source[j]; + if(distance[x] > distance[y] + Weight[j]) + { + distance[x] = -1; + } } + } for(i = 0; i < edgecount; i++) + { + x = Dest[i]; + y = Source[i]; + if(distance[x] > distance[y] + Weight[i]) { - x = Dest[i]; - y = Source[i]; - if(distance[x] > distance[y] + Weight[i]) - { - return; - } + return; } + } for(i = 0; i < nodecount; i++) - { - __VERIFIER_assert(distance[i]>=0); - } - + { + __VERIFIER_assert(distance[i] >= 0); + } } diff --git a/regression/cbmc/Array_UF7/main.c b/regression/cbmc/Array_UF7/main.c index dd0bfdb9cba..e0d9e5b702d 100644 --- a/regression/cbmc/Array_UF7/main.c +++ b/regression/cbmc/Array_UF7/main.c @@ -1,35 +1,42 @@ extern void __VERIFIER_error(); -void __VERIFIER_assert(int cond) { - if (!(cond)) { - ERROR: __VERIFIER_error(); +void __VERIFIER_assert(int cond) +{ + if(!(cond)) + { + ERROR: + __VERIFIER_error(); } return; } char __VERIFIER_nondet_char(); unsigned int __VERIFIER_nondet_uint(); -int main() { - int MAX = __VERIFIER_nondet_uint(); - char str1[MAX], str2[MAX]; - int cont, i, j; - cont = 0; +int main() +{ + int MAX = __VERIFIER_nondet_uint(); + char str1[MAX], str2[MAX]; + int cont, i, j; + cont = 0; - for (i=0; i= 0; i--) { - str2[j] = str1[0]; - j++; - } + for(i = MAX - 1; i >= 0; i--) + { + str2[j] = str1[0]; + j++; + } - j = MAX-1; - for (i=0; i= 0; i--) { - str2[j] = str1[i]; - j++; - } + for(i = max - 1; i >= 0; i--) + { + str2[j] = str1[i]; + j++; + } - j = max-1; - for (i=0; i