From 791ce7463b6891e74fff844ecf53ec398f119c8d Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Fri, 27 Nov 2020 16:07:23 +0100 Subject: [PATCH] add newlines at end of text files --- doc/code/style.css | 2 +- src/plugins/aorai/tests/ltl/call_tree.ltl | 2 +- src/plugins/aorai/tests/ltl/test_boucle.ltl | 2 +- src/plugins/aorai/tests/ya/assigns.ya | 2 +- src/plugins/aorai/tests/ya/assigns_det.ya | 2 +- src/plugins/aorai/tests/ya/deterministic.ya | 2 +- src/plugins/aorai/tests/ya/incorrect.ya | 2 +- src/plugins/aorai/tests/ya/other.ya | 2 +- src/plugins/aorai/tests/ya/single_call.ya | 2 +- .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h | 2 +- .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c | 2 +- src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h | 2 +- src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c | 2 +- src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h | 2 +- src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c | 2 +- src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h | 2 +- .../bittree_model/e_acsl_bittree_omodel_debug.c | 2 +- src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h | 2 +- .../e-acsl/observation_model/internals/e_acsl_heap_tracking.h | 2 +- .../observation_model/internals/e_acsl_timestamp_retrieval.h | 2 +- src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c | 2 +- src/plugins/e-acsl/tests/builtin/test_config_dev | 2 +- src/plugins/e-acsl/tests/examples/functions_contiki.c | 2 +- src/plugins/e-acsl/tests/full-mtracking/test_config_dev | 2 +- src/plugins/e-acsl/tests/gmp-only/test_config_dev | 2 +- src/plugins/e-acsl/tests/memory/separated.c | 2 +- src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c | 2 +- src/plugins/wp/share/why3/frama_c_wp/vset.mlw | 2 +- .../wp/tests/wp_acsl/assigned_not_initialized_memtyped.i | 2 +- src/plugins/wp/tests/wp_acsl/inductive.i | 2 +- src/plugins/wp/tests/wp_acsl/predicates_functions.i | 2 +- src/plugins/wp/tests/wp_acsl/struct_fields.i | 2 +- src/plugins/wp/tests/wp_acsl/unsupported_builtin.i | 2 +- src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml | 2 +- src/plugins/wp/tests/wp_plugin/abs.driver | 2 +- tests/builtins/.gitignore | 2 +- tests/crowbar/input/testcase | 2 +- tests/float/.gitignore | 2 +- tests/idct/.gitignore | 2 +- tests/misc/issue_191.ml | 2 +- tests/misc/tests.sh | 2 +- tests/pretty_printing/ghost_parameters.c | 2 +- tests/spec/Extend_short_print.i | 2 +- tests/spec/Extend_short_print.ml | 2 +- tests/spec/assigns_from_kf.i | 2 +- tests/spec/assigns_from_kf.ml | 2 +- tests/spec/logic_functions_sets.ml | 2 +- tests/syntax/ghost_cv_incompat.i | 2 +- tests/syntax/ghost_cv_invalid_use.i | 2 +- tests/syntax/ghost_else_bad.c | 2 +- tests/syntax/ghost_else_bad_oneline.i | 2 +- tests/syntax/ghost_parameters.c | 2 +- tests/syntax/preprocessed.ci | 2 +- tests/value/.gitignore | 2 +- tests/value/implies.i | 2 +- tests/verisec/suite/programs/apps/Makefile | 2 +- 56 files changed, 56 insertions(+), 56 deletions(-) diff --git a/doc/code/style.css b/doc/code/style.css index 01d4b3f6552..ad650ef54ef 100644 --- a/doc/code/style.css +++ b/doc/code/style.css @@ -161,4 +161,4 @@ div.sig_block {margin-left: 2em} li { margin-left: 2em } .copyright { margin-top: 5mm; font-size:10px; padding-top: 2mm; border-top: thin solid #404040; } .copyright a:visited { color:darkred } -.copyright a:link { color:darkred } \ No newline at end of file +.copyright a:link { color:darkred } diff --git a/src/plugins/aorai/tests/ltl/call_tree.ltl b/src/plugins/aorai/tests/ltl/call_tree.ltl index 0bd3eea830b..8025745abb3 100644 --- a/src/plugins/aorai/tests/ltl/call_tree.ltl +++ b/src/plugins/aorai/tests/ltl/call_tree.ltl @@ -1 +1 @@ -CALL(main) && _X_ ((x == 0 && CALL(f) && _X_ (RETURN(f) && _X_ (CALL(g) && _X_ RETURN(g)))) || (x!=0 && (CALL(g) && _X_ RETURN(g)))) \ No newline at end of file +CALL(main) && _X_ ((x == 0 && CALL(f) && _X_ (RETURN(f) && _X_ (CALL(g) && _X_ RETURN(g)))) || (x!=0 && (CALL(g) && _X_ RETURN(g)))) diff --git a/src/plugins/aorai/tests/ltl/test_boucle.ltl b/src/plugins/aorai/tests/ltl/test_boucle.ltl index 3e3d00c7ad4..9817c70f3d0 100644 --- a/src/plugins/aorai/tests/ltl/test_boucle.ltl +++ b/src/plugins/aorai/tests/ltl/test_boucle.ltl @@ -1 +1 @@ -_G_(CALL(b) => (CALL_OR_RETURN(b) _U_ CALL(a))) \ No newline at end of file +_G_(CALL(b) => (CALL_OR_RETURN(b) _U_ CALL(a))) diff --git a/src/plugins/aorai/tests/ya/assigns.ya b/src/plugins/aorai/tests/ya/assigns.ya index 40ca7d12a90..95e3cb481ea 100644 --- a/src/plugins/aorai/tests/ya/assigns.ya +++ b/src/plugins/aorai/tests/ya/assigns.ya @@ -9,4 +9,4 @@ S_in_f: { RETURN(f) } -> in_main; in_main: { RETURN(main) } -> S2; -S2: -> S2; \ No newline at end of file +S2: -> S2; diff --git a/src/plugins/aorai/tests/ya/assigns_det.ya b/src/plugins/aorai/tests/ya/assigns_det.ya index 23d18f81308..6169d810657 100644 --- a/src/plugins/aorai/tests/ya/assigns_det.ya +++ b/src/plugins/aorai/tests/ya/assigns_det.ya @@ -10,4 +10,4 @@ S_in_f: { RETURN(f) } -> in_main; in_main: { RETURN(main) } -> S2; -S2: -> S2; \ No newline at end of file +S2: -> S2; diff --git a/src/plugins/aorai/tests/ya/deterministic.ya b/src/plugins/aorai/tests/ya/deterministic.ya index ab8088b4543..326a2b86485 100644 --- a/src/plugins/aorai/tests/ya/deterministic.ya +++ b/src/plugins/aorai/tests/ya/deterministic.ya @@ -19,4 +19,4 @@ S4: { RETURN(g) } -> S3; S5: { RETURN(g) } -> S1; -Sf: -> Sf; \ No newline at end of file +Sf: -> Sf; diff --git a/src/plugins/aorai/tests/ya/incorrect.ya b/src/plugins/aorai/tests/ya/incorrect.ya index 4aec9ac2e84..5b8316b0ef0 100644 --- a/src/plugins/aorai/tests/ya/incorrect.ya +++ b/src/plugins/aorai/tests/ya/incorrect.ya @@ -3,4 +3,4 @@ %deterministic; s0: { f() } -> OK; -OK: -> OK; \ No newline at end of file +OK: -> OK; diff --git a/src/plugins/aorai/tests/ya/other.ya b/src/plugins/aorai/tests/ya/other.ya index b09fdac2e90..9decad039c1 100644 --- a/src/plugins/aorai/tests/ya/other.ya +++ b/src/plugins/aorai/tests/ya/other.ya @@ -11,4 +11,4 @@ step1: { x == 4 } -> last last: { x == 3 } -> step1 | { x == 4 } -> init | other -> last - ; \ No newline at end of file + ; diff --git a/src/plugins/aorai/tests/ya/single_call.ya b/src/plugins/aorai/tests/ya/single_call.ya index 0b249a798cd..023c136805c 100644 --- a/src/plugins/aorai/tests/ya/single_call.ya +++ b/src/plugins/aorai/tests/ya/single_call.ya @@ -2,4 +2,4 @@ %accept: Sf; S0: { [main()] } -> Sf; -Sf: -> Sf; \ No newline at end of file +Sf: -> Sf; diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h index e9970b9edf5..46e8fe3a6ad 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h @@ -52,4 +52,4 @@ void eacsl_runtime_assert(int pred, const char *kind, const char *fct, const char *pred_txt, const char * file, int line) __attribute__((FC_BUILTIN)); -#endif // E_ACSL_ASSERT_H \ No newline at end of file +#endif // E_ACSL_ASSERT_H diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c index 399b60cd70c..37c0d97959f 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c @@ -138,4 +138,4 @@ int temporal_valid(void *ptr, void *addr_of_ptr) { } /* }}} */ -#endif // E_ACSL_TEMPORAL \ No newline at end of file +#endif // E_ACSL_TEMPORAL diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h index 84a2238ffb0..15e5702665a 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h @@ -179,4 +179,4 @@ static inline void clearbits_right(size_t size, void *ptr) { clearbits64_right(size%64, *(lp-i)); } -#endif // E_ACSL_BITS_H \ No newline at end of file +#endif // E_ACSL_BITS_H diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c index 0c42873864c..29d5f5722f6 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c @@ -91,4 +91,4 @@ void describe_run() { rtl_printf(" * Format Checks: %s\n", E_ACSL_FORMAT_VALIDITY_DESC); rtl_printf("/* ========================================================= */\n"); #endif -} \ No newline at end of file +} diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h index bc38137d8f5..74b4c5a2a44 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h @@ -140,4 +140,4 @@ int is_pow_of_2(size_t x); /* }}} */ -#endif // E_ACSL_MALLOC_H \ No newline at end of file +#endif // E_ACSL_MALLOC_H diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c index 5453030b537..2858275b1c5 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c @@ -404,4 +404,4 @@ int rtl_vsprintf(char *s, char *fmt, va_list vlist) { _format(&s, putcp, fmt, vlist); putcp(&s,0); return 1; -} \ No newline at end of file +} diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h index 839bfe24fb3..8d39d57dd14 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h @@ -95,4 +95,4 @@ int rtl_vdprintf(int fd, char *fmt, va_list vlist); int rtl_vformat_stderr(); -#endif // E_ACSL_RTL_IO_H \ No newline at end of file +#endif // E_ACSL_RTL_IO_H diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c index 75a3feca780..60a0b393209 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c @@ -47,4 +47,4 @@ int readonly (void *ptr) { int writeable(uintptr_t addr, long size, uintptr_t base_ptr) { return allocated(addr, size, base_ptr) && !readonly((void*)addr); -} \ No newline at end of file +} diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h index d622c489166..89fc0b30b91 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h @@ -49,4 +49,4 @@ size_t eacsl_get_heap_allocation_size() size_t eacsl_get_heap_allocated_blocks() __attribute__((FC_BUILTIN)); -#endif // E_ACSL_HEAP \ No newline at end of file +#endif // E_ACSL_HEAP diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h index eb8610314f2..aa346323fa9 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h @@ -43,4 +43,4 @@ void update_heap_allocation(long size); * some allocated memory on the heap. */ void report_heap_leacks(); -#endif // E_ACSL_HEAP_TRACKING \ No newline at end of file +#endif // E_ACSL_HEAP_TRACKING diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h index 209cd495263..610c77275b0 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h @@ -50,4 +50,4 @@ void store_temporal_referent(void *ptr, uint32_t ref); #endif // E_ACSL_TEMPORAL -#endif // E_ACSL_TIMESTAMP_RETRIEVAL_H \ No newline at end of file +#endif // E_ACSL_TIMESTAMP_RETRIEVAL_H diff --git a/src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c index a289de1d5a1..1bfbbb986b5 100644 --- a/src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c +++ b/src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c @@ -66,4 +66,4 @@ int main(void) { \at(n + i == 10, L); */ ; return 0; -} \ No newline at end of file +} diff --git a/src/plugins/e-acsl/tests/builtin/test_config_dev b/src/plugins/e-acsl/tests/builtin/test_config_dev index dc75e26d187..a915fc61b24 100644 --- a/src/plugins/e-acsl/tests/builtin/test_config_dev +++ b/src/plugins/e-acsl/tests/builtin/test_config_dev @@ -1 +1 @@ -MACRO: ROOT_EACSL_GCC_OPTS_EXT --libc-replacements \ No newline at end of file +MACRO: ROOT_EACSL_GCC_OPTS_EXT --libc-replacements diff --git a/src/plugins/e-acsl/tests/examples/functions_contiki.c b/src/plugins/e-acsl/tests/examples/functions_contiki.c index 382a1a64b9e..180c70afd8b 100644 --- a/src/plugins/e-acsl/tests/examples/functions_contiki.c +++ b/src/plugins/e-acsl/tests/examples/functions_contiki.c @@ -25,4 +25,4 @@ int main (void) { node2.next = &node3; struct list *l = &node1; /*@ assert length(l) == 3; */ ; -} \ No newline at end of file +} diff --git a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev index bdb600fef3f..80a939ea027 100644 --- a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev +++ b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev @@ -1 +1 @@ -MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking \ No newline at end of file +MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config_dev b/src/plugins/e-acsl/tests/gmp-only/test_config_dev index bb73475a6fb..3a3fc2c7e60 100644 --- a/src/plugins/e-acsl/tests/gmp-only/test_config_dev +++ b/src/plugins/e-acsl/tests/gmp-only/test_config_dev @@ -1 +1 @@ -MACRO: ROOT_EACSL_GCC_OPTS_EXT --gmp \ No newline at end of file +MACRO: ROOT_EACSL_GCC_OPTS_EXT --gmp diff --git a/src/plugins/e-acsl/tests/memory/separated.c b/src/plugins/e-acsl/tests/memory/separated.c index f63bc50c481..872cba8db9d 100644 --- a/src/plugins/e-acsl/tests/memory/separated.c +++ b/src/plugins/e-acsl/tests/memory/separated.c @@ -65,4 +65,4 @@ int main() { } return 0; -} \ No newline at end of file +} diff --git a/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c index 89c8226676a..3b5788f306a 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c @@ -4,4 +4,4 @@ */ int main() { return 0; -} \ No newline at end of file +} diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw index 1e9a850621d..d18a7ffa8a4 100644 --- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw +++ b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw @@ -98,4 +98,4 @@ theory Vset (* -------------------------------------------------------------------------- *) -end \ No newline at end of file +end diff --git a/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i index fa203195e79..6c9a2d5554a 100644 --- a/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i +++ b/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i @@ -59,4 +59,4 @@ void assigned_glob_array(void){ for(int i = 0; i < 10; ++i){} //@ check FAIL: \initialized(pg_array); //@ check OK: \initialized(cg_array); -} \ No newline at end of file +} diff --git a/src/plugins/wp/tests/wp_acsl/inductive.i b/src/plugins/wp/tests/wp_acsl/inductive.i index 5f3e2839f75..d55c56546d1 100644 --- a/src/plugins/wp/tests/wp_acsl/inductive.i +++ b/src/plugins/wp/tests/wp_acsl/inductive.i @@ -65,4 +65,4 @@ typedef struct _list { int element; struct _list* next; } list; same_elements{L1, L2}(a, b, b1, e1) ==> same_elements{L2, L3}(b, a, b2, e2) ==> \false ; -*/ \ No newline at end of file +*/ diff --git a/src/plugins/wp/tests/wp_acsl/predicates_functions.i b/src/plugins/wp/tests/wp_acsl/predicates_functions.i index d54998f4ced..e5aafcf4563 100644 --- a/src/plugins/wp/tests/wp_acsl/predicates_functions.i +++ b/src/plugins/wp/tests/wp_acsl/predicates_functions.i @@ -11,4 +11,4 @@ /*@ logic integer F(integer i) = i * 2 ; */ /*@ logic integer RF(integer i) = (i <= 0) ? 0 : F(i) + RF(i-1) ; */ -/*@ lemma foo: \forall integer i ; i > 0 ==> RP(RF(i)) ; */ \ No newline at end of file +/*@ lemma foo: \forall integer i ; i > 0 ==> RP(RF(i)) ; */ diff --git a/src/plugins/wp/tests/wp_acsl/struct_fields.i b/src/plugins/wp/tests/wp_acsl/struct_fields.i index 93b9c90858a..9aedd854e92 100644 --- a/src/plugins/wp/tests/wp_acsl/struct_fields.i +++ b/src/plugins/wp/tests/wp_acsl/struct_fields.i @@ -14,4 +14,4 @@ struct X { void foo(struct X* p){ struct X r = *p ; *p = r ; -} \ No newline at end of file +} diff --git a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i index b412a516663..a91a3fbef4b 100644 --- a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i +++ b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i @@ -10,4 +10,4 @@ void foo(void); int main(void){ foo(); //@ assert \true ; -} \ No newline at end of file +} diff --git a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml index ed343f06029..5d6b6e6dc0b 100644 --- a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml +++ b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml @@ -9,4 +9,4 @@ let builtin = { } let () = - Logic_builtin.add builtin \ No newline at end of file + Logic_builtin.add builtin diff --git a/src/plugins/wp/tests/wp_plugin/abs.driver b/src/plugins/wp/tests/wp_plugin/abs.driver index 977a8a6c7d8..97bcd60eadc 100644 --- a/src/plugins/wp/tests/wp_plugin/abs.driver +++ b/src/plugins/wp/tests/wp_plugin/abs.driver @@ -3,4 +3,4 @@ logic integer ABS (integer) = "my_abs" ; coq.file := "Abs.v"; altergo.file := "abs.mlw"; -why3.file := "abs.why"; \ No newline at end of file +why3.file := "abs.why"; diff --git a/tests/builtins/.gitignore b/tests/builtins/.gitignore index a2232653a6f..5de45901ce6 100644 --- a/tests/builtins/.gitignore +++ b/tests/builtins/.gitignore @@ -1 +1 @@ -/oracle_* \ No newline at end of file +/oracle_* diff --git a/tests/crowbar/input/testcase b/tests/crowbar/input/testcase index e0a6c6668c4..56a2a5ae6dd 100644 --- a/tests/crowbar/input/testcase +++ b/tests/crowbar/input/testcase @@ -1 +1 @@ -fo \ No newline at end of file +fo diff --git a/tests/float/.gitignore b/tests/float/.gitignore index a2232653a6f..5de45901ce6 100644 --- a/tests/float/.gitignore +++ b/tests/float/.gitignore @@ -1 +1 @@ -/oracle_* \ No newline at end of file +/oracle_* diff --git a/tests/idct/.gitignore b/tests/idct/.gitignore index a2232653a6f..5de45901ce6 100644 --- a/tests/idct/.gitignore +++ b/tests/idct/.gitignore @@ -1 +1 @@ -/oracle_* \ No newline at end of file +/oracle_* diff --git a/tests/misc/issue_191.ml b/tests/misc/issue_191.ml index a65693ff931..afbb9efd7c3 100644 --- a/tests/misc/issue_191.ml +++ b/tests/misc/issue_191.ml @@ -1,4 +1,4 @@ let norm1 = Filepath.normalize ~base_name:"/dir1/" "dir/file" in let norm2 = Filepath.normalize ~base_name:"/dir2/" "dir/file" in (* norm2 should be different than norm1 *) -Printf.printf "norm1: %s\nnorm2: %s\n" norm1 norm2 \ No newline at end of file +Printf.printf "norm1: %s\nnorm2: %s\n" norm1 norm2 diff --git a/tests/misc/tests.sh b/tests/misc/tests.sh index 004d0f5f22e..20df6b9e707 100755 --- a/tests/misc/tests.sh +++ b/tests/misc/tests.sh @@ -60,4 +60,4 @@ if [ "${Res}" != 0 ] ; then exit ${Res} fi Compare ${PreFix} ${PostFix1} stdout -Compare ${PreFix} ${PostFix2} stderr \ No newline at end of file +Compare ${PreFix} ${PostFix2} stderr diff --git a/tests/pretty_printing/ghost_parameters.c b/tests/pretty_printing/ghost_parameters.c index 125ea27e9af..27dc37fa59a 100644 --- a/tests/pretty_printing/ghost_parameters.c +++ b/tests/pretty_printing/ghost_parameters.c @@ -49,4 +49,4 @@ int main(void) { decl_variadic(2, 1, 2, 3, 4, 4); def_variadic(2, 1, 2, 3, 4, 4); */ -} \ No newline at end of file +} diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i index 568f3561f8b..d3f776e538a 100644 --- a/tests/spec/Extend_short_print.i +++ b/tests/spec/Extend_short_print.i @@ -6,4 +6,4 @@ OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs /*@ without_short \true ; has_short \true ; -*/ \ No newline at end of file +*/ diff --git a/tests/spec/Extend_short_print.ml b/tests/spec/Extend_short_print.ml index 386cc1080b5..3bc2da1b356 100644 --- a/tests/spec/Extend_short_print.ml +++ b/tests/spec/Extend_short_print.ml @@ -11,4 +11,4 @@ let process_global _ = function | Dextended(e, _, _) -> Kernel.feedback "%a" Cil_printer.pp_short_extended e | _ -> () -let () = Db.Main.extend (fun () -> Annotations.iter_global process_global) \ No newline at end of file +let () = Db.Main.extend (fun () -> Annotations.iter_global process_global) diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i index 90a4fb65484..87084d55a6f 100644 --- a/tests/spec/assigns_from_kf.i +++ b/tests/spec/assigns_from_kf.i @@ -44,4 +44,4 @@ void reference(void) { g_both(0, 1, 0, 2); g_both_r(0, 1, 0, 2); */ -} \ No newline at end of file +} diff --git a/tests/spec/assigns_from_kf.ml b/tests/spec/assigns_from_kf.ml index fcab8e135d1..875006cd3a6 100644 --- a/tests/spec/assigns_from_kf.ml +++ b/tests/spec/assigns_from_kf.ml @@ -1,4 +1,4 @@ let run () = Globals.Functions.iter (fun kf -> ignore (Annotations.funspec kf)) -let () = Db.Main.extend run \ No newline at end of file +let () = Db.Main.extend run diff --git a/tests/spec/logic_functions_sets.ml b/tests/spec/logic_functions_sets.ml index 0eb5f933fd7..68aead8c98f 100644 --- a/tests/spec/logic_functions_sets.ml +++ b/tests/spec/logic_functions_sets.ml @@ -13,4 +13,4 @@ let check = function | _ -> () let () = - Db.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g)) \ No newline at end of file + Db.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g)) diff --git a/tests/syntax/ghost_cv_incompat.i b/tests/syntax/ghost_cv_incompat.i index d32307648e3..0de775a8e05 100644 --- a/tests/syntax/ghost_cv_incompat.i +++ b/tests/syntax/ghost_cv_incompat.i @@ -187,4 +187,4 @@ void ghost_calls(void){ //@ ghost int g; //@ ghost ghost_decl_nothing(&g); //@ ghost ghost_def_nothing(&g); -} \ No newline at end of file +} diff --git a/tests/syntax/ghost_cv_invalid_use.i b/tests/syntax/ghost_cv_invalid_use.i index 59398e76c96..a4e082cc808 100644 --- a/tests/syntax/ghost_cv_invalid_use.i +++ b/tests/syntax/ghost_cv_invalid_use.i @@ -157,4 +157,4 @@ void ghost_calls_to_non_ghost_functions(){ int x2 = int_assigns_nothing(&g); int x3 = int_assigns_parameter(&g); */ -} \ No newline at end of file +} diff --git a/tests/syntax/ghost_else_bad.c b/tests/syntax/ghost_else_bad.c index 00a3bc684d1..0fad3b59986 100644 --- a/tests/syntax/ghost_else_bad.c +++ b/tests/syntax/ghost_else_bad.c @@ -52,4 +52,4 @@ void test(int x, int y){ */ } -#endif \ No newline at end of file +#endif diff --git a/tests/syntax/ghost_else_bad_oneline.i b/tests/syntax/ghost_else_bad_oneline.i index 990b2e21ea6..d78f5e54a4d 100644 --- a/tests/syntax/ghost_else_bad_oneline.i +++ b/tests/syntax/ghost_else_bad_oneline.i @@ -7,4 +7,4 @@ void if_ghost_else_one_line_bad(int x, int y) { x++; } //@ ghost else y++; -} \ No newline at end of file +} diff --git a/tests/syntax/ghost_parameters.c b/tests/syntax/ghost_parameters.c index 5aae2549228..b1caed23168 100644 --- a/tests/syntax/ghost_parameters.c +++ b/tests/syntax/ghost_parameters.c @@ -205,4 +205,4 @@ void function_non_void(int x) /*@ ghost (void) */ { } -#endif \ No newline at end of file +#endif diff --git a/tests/syntax/preprocessed.ci b/tests/syntax/preprocessed.ci index 57aaaec0757..940d6b1100e 100644 --- a/tests/syntax/preprocessed.ci +++ b/tests/syntax/preprocessed.ci @@ -9,4 +9,4 @@ int foo() { int FOO = 42; return FOO; } Local Variables: mode: C End: -*/ \ No newline at end of file +*/ diff --git a/tests/value/.gitignore b/tests/value/.gitignore index a2232653a6f..5de45901ce6 100644 --- a/tests/value/.gitignore +++ b/tests/value/.gitignore @@ -1 +1 @@ -/oracle_* \ No newline at end of file +/oracle_* diff --git a/tests/value/implies.i b/tests/value/implies.i index 005c828797c..b0c3b3a5b4b 100644 --- a/tests/value/implies.i +++ b/tests/value/implies.i @@ -8,4 +8,4 @@ int main(int c, int d) /*@ assert c ==> \false; */ return 1 + c; -} \ No newline at end of file +} diff --git a/tests/verisec/suite/programs/apps/Makefile b/tests/verisec/suite/programs/apps/Makefile index ecb8f7a623b..2d7cb97cd85 100644 --- a/tests/verisec/suite/programs/apps/Makefile +++ b/tests/verisec/suite/programs/apps/Makefile @@ -43,4 +43,4 @@ edbrowse: $(EDBROWSE_DIR)/strchr_bad.c openser:openser_6876 openser_6876:$(OPENSER_6876_DIR)/full_bad.c - $(FRAMAC) -val $(STUBS) $(OPENSER_6876_DIR)/full_bad.c -slevel 500 >$(OPENSER_6876_DIR)/full_bad.log 2>$(OPENSER_6876_DIR)/full_bad.err \ No newline at end of file + $(FRAMAC) -val $(STUBS) $(OPENSER_6876_DIR)/full_bad.c -slevel 500 >$(OPENSER_6876_DIR)/full_bad.log 2>$(OPENSER_6876_DIR)/full_bad.err -- GitLab