diff --git a/doc/code/style.css b/doc/code/style.css index 01d4b3f65529a76b83755e01adacb1a47b1f99bd..ad650ef54ef6ce3eb1506bb411d42ec244436726 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 0bd3eea830baf4120895a7c01d59b371f6aa7d3a..8025745abb3fbf52be0526cd62e77aee72af7720 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 3e3d00c7ad41a20bd43c51c786cfad21ab60630a..9817c70f3d09927af0e37d3707357e463a24f7ab 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 40ca7d12a90bb165ffc2db09202323b5c7bc21f3..95e3cb481eafa8ba4ed12f75a0faaceab026b62b 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 23d18f81308636a27529f070ea1bf3bb098e3f49..6169d8106572ddb4005a6acf767e0ae818149b9a 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 ab8088b4543b7d9dab8db1965049b7a05767b9f7..326a2b86485eba322838f12711fb224b339f58cc 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 4aec9ac2e844c4e43940e87990d026c3f7780064..5b8316b0ef0d0b1a85f91155b7ef0532ea2c3cf1 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 b09fdac2e90f18ea3354d88dbc2a1a948a92d88a..9decad039c19064deae6501be6541c906411ee43 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 0b249a798cde0ac98ddf522930d64ae366f42af5..023c136805c125f600b5aeb9730456c570991098 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 e9970b9edf55a846d4e161bede50adf8b0dcbe6a..46e8fe3a6ad1018564f6a782f6d6c8138e9a2011 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 399b60cd70c2148dbe7030a37ec4b6a0f8e304fa..37c0d97959f8ba8c997ec0305dc231ba9c045cef 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 84a2238ffb05617a8c0aa0ecf2c14b4e6becd347..15e5702665a57864d02072e6efbeacd6d761179c 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 0c42873864c1d7b89465dcc26403ac252afb3de3..29d5f5722f669f6c310f22beb537c2394a1e0aa3 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 bc38137d8f566ddabdc015a3eb4236cdbbf8ceda..74b4c5a2a44eadf208b1f0ebfdeaa444d25f1cca 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 5453030b537bb3bce02c11d39873e5682b598a20..2858275b1c56a325fab73aaa05bb1d85b05e41d9 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 839bfe24fb366099648c9b28fc6b3aac0058372e..8d39d57dd14023570b5d05dde72c51ea017f646f 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 75a3feca780f5a2a72fec437dff74625f9651cf8..60a0b3932093a2ffa52e0238d67784e70f26e864 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 d622c489166a7a8df533edcd45b97ca5e3330ef5..89fc0b30b91d7b27554a522b9b55d2ae38364d90 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 eb8610314f20e6899f7cd971d75f9db64b735f72..aa346323fa9fda86e4aa1f370065b0e5b2875b85 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 209cd4952633a90ad4061cfedff8d974d30f0589..610c77275b0b787cb6d97aa83b576ac83d3e96b4 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 a289de1d5a1c02e97bd12f1f5205a24c93639039..1bfbbb986b51f3aaa1e9fccccec9397b07987c22 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 dc75e26d1876b0a817f77381d8063753cbce7dc2..a915fc61b249ed381825662eecdb83418ae70384 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 382a1a64b9ef6fd97bc358a2ca031e1238d32935..180c70afd8bb5be37581ff25f00292ca0f34df63 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 bdb600fef3fe5c8ec148408a9a4207cfb5bf1239..80a939ea02713f1e0fb539f6bfb567096a7e2510 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 bb73475a6fbca63d3b9c38570ba4bafd575a71a5..3a3fc2c7e601d0b97416e7f858e9ddeee944102f 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 f63bc50c481ce6e32f517c41545ba6792b913088..872cba8db9d97a4cd3e2cf835109049747077274 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 89c8226676ab5212917925b305c0eeb1fde5c40f..3b5788f306a66a9598ba9e6c318fc94c8fde7aae 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 1e9a850621d652ac870027c530e189895df9ee6f..d18a7ffa8a40ff3a1b218dba6f23345013f13924 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 fa203195e799f12f2b2d1603defdec66bdb537b3..6c9a2d5554a89a7ceb890d3c51adff2ea0f9b1f2 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 5f3e2839f7510e61334ea67efb2550442f5a5b64..d55c56546d1153428145b8dfc8f73a5f7e64118c 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 d54998f4cedefdd31991f8557bb9119e683e3430..e5aafcf45632c91ff9e1cffe561d4f8bfde41cf4 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 93b9c90858aaca1db67542015efe50acabd61703..9aedd854e92c42e5808382b3ecce5c4eae0f2b05 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 b412a516663d5e3e228cfbeb7d43971796145812..a91a3fbef4b34b38d8e5fec4f651c709801f4bf6 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 ed343f06029c748895e17bcddb6652e4ddd3a8c6..5d6b6e6dc0b2651ec70e525372b15b8a8dc65e17 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 977a8a6c7d82b7edc35c5d88087d8dc07ed1e16b..97bcd60eadc035dc88e07d7176196f32c897b3c0 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 a2232653a6f719442070e6f515728d7e0a863c46..5de45901ce62a18d26c6309c170b943215b78b67 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 e0a6c6668c4b093cc3bcdf79b05693c024daa46f..56a2a5ae6dd90f45b6ec161eac41cf0e693f669d 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 a2232653a6f719442070e6f515728d7e0a863c46..5de45901ce62a18d26c6309c170b943215b78b67 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 a2232653a6f719442070e6f515728d7e0a863c46..5de45901ce62a18d26c6309c170b943215b78b67 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 a65693ff931e59aca07e59d82795546b00bb56f0..afbb9efd7c39c460d4aead0e2d0ca5a847cde8fe 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 004d0f5f22e6fee31cebca4a99b2dfba33d2eeae..20df6b9e707189225184b3cc2b134c0dce336c28 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 125ea27e9affb6da2ad8d94318302702e602d56c..27dc37fa59a03fe51d987bf0bccb84162ec451b0 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 568f3561f8b22dbb8022ed9baed7acb122ed7f0e..d3f776e538ad9fab7fb58da166532e67a394872e 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 386cc1080b5165c554a3b574e3b3834605e35360..3bc2da1b356c7916b579cc72d42623b0409a4f5b 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 90a4fb65484eb6b1f0b87ef22d7316f26c957f76..87084d55a6f8bf65ebb9dee4f0a8bc91f733d85e 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 fcab8e135d1e04408c95c695eba44eac20e22173..875006cd3a6d37b85f257a7acae2f2a9d36ca615 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 0eb5f933fd72a4e91afd78a35747fdd40008009f..68aead8c98f74e3723b06d2498ef78cd93af3f71 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 d32307648e30ce99f3e1bfd6e8e92ff6ae75612a..0de775a8e056e17559429eedc7ef5d26feb12bab 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 59398e76c9678148469ce901c0e35b6dc22ca4fc..a4e082cc80821e0c384ace856b36df57d72fd94c 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 00a3bc684d11d361b7351f74376970613f06e2c3..0fad3b59986a0a65ad22b21b9f9b170ed348b49e 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 990b2e21ea623e3b62852f3d58750d550691d74d..d78f5e54a4db97deda334fa64c48c5f8ca5fa827 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 5aae254922897843c44c6eca66dda28045391c43..b1caed2316819fca7f5298378248efc7d71dc111 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 57aaaec07570168108712920c0c82a484e65f31c..940d6b1100e454619a619dad2821d8a2268446e8 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 a2232653a6f719442070e6f515728d7e0a863c46..5de45901ce62a18d26c6309c170b943215b78b67 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 005c828797c2e60e680f880869d43e286272fd1c..b0c3b3a5b4beae1a522a0b84fc33cb86f61ec019 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 ecb8f7a623b9661f5f9a060e099dd289e5729dfc..2d7cb97cd85927ed6419667fe0ca66954bd70932 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