diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i index 3f9e7b87a8b42a5242bb74060cd129586b61042a..ccde8d32cf69e67cc1595503336e8a461d1b98aa 100644 --- a/src/plugins/wp/tests/wp_plugin/dynamic.i +++ b/src/plugins/wp/tests/wp_plugin/dynamic.i @@ -61,7 +61,7 @@ int h0(void); @ assigns X1; @ ensures X1==1; */ int behavior (int (*p)(void)) { - //@ calls h1, h2; + //@ calls h1, h2; // Shall not be proved in default behavior (known bug) return (*p)(); }