~/acslplusplus_frama-c/Playground/jochen ./gw 139.cpp rm: cannot remove ‘wp-out/typed’: Is a directory +++++ gcc 139.cpp +++++ 139.cpp: In function ‘int main()’: 139.cpp:18:15: warning: unused variable ‘a’ [-Wunused-variable] int const a = rp->area(); ^ +++++ frc 139.cpp +++++ Now output intermediate result [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function _frama_c_find_dynamic_cast [rte] annotating function _frama_c_find_dynamic_cast_aux [rte] annotating function Square::Ctor [rte] annotating function Square::Ctor [rte] annotating function Square::Dtor [rte] annotating function operator= [rte] annotating function Rectangle::Ctor [rte] annotating function Rectangle::Ctor [rte] annotating function Rectangle::Dtor [rte] annotating function operator= [rte] annotating function area [rte] annotating function area [rte] annotating function main 139.cpp:18:[rte] warning: no predicate available yet to check validity of function pointer dereferencing *((int (*)( struct Rectangle *))__virtual_tmp_0->method_ptr) 139.cpp:18:[wp] warning: Ignored function pointer (see -wp-dynamic) 139.cpp:2:[wp] warning: Missing assigns clause (assigns 'everything' instead) [wp] Computing [100 goals...] 139.cpp:18:[wp] warning: Missing assigns clause (assigns 'everything' instead) 139.cpp:8:[wp] warning: void object 139.cpp:8:[wp] warning: Cast with incompatible pointers types (source: _Z9Rectangle*) (target: sint8*) [wp] 117 goals scheduled [wp] [Qed] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____3 : Valid (1ms) [wp] [Qed] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____5 : Valid [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info____ : Unknown (1s) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____2 : Unknown (Qed:3ms) (3s) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____4 : Unknown (5s) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____6 : Timeout (Qed:7ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____7 : Timeout (Qed:2ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____8 : Timeout (Qed:1ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____9 : Timeout (Qed:23ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____12 : Valid (Qed:10ms) (173ms) (111) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10 : Timeout (Qed:10ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____11 : Timeout (Qed:3ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____16 : Valid (Qed:17ms) (188ms) (121) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____14 : Timeout (Qed:18ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____13 : Timeout (Qed:12ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____17 : Valid (Qed:40ms) (207ms) (87) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____19 : Valid (Qed:25ms) (139ms) (83) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____18 : Valid (Qed:37ms) (120ms) (83) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____15 : Timeout (Qed:13ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____20 : Timeout (Qed:43ms) [wp] [Qed] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____24 : Valid (32ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____21 : Timeout (Qed:41ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____22 : Timeout (Qed:56ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____26 : Valid (Qed:69ms) (92ms) (77) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____28 : Valid (Qed:41ms) (229ms) (106) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____23 : Timeout (Qed:54ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____25 : Timeout (Qed:45ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____27 : Timeout (Qed:74ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____29 : Timeout (Qed:39ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____30 : Timeout (Qed:40ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i___ : Unknown (Qed:5ms) (2s) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____31 : Timeout (Qed:62ms) [wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____3 : Valid (2ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____2 : Unknown (Qed:6ms) (3s) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____32 : Timeout (Qed:79ms) [wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____33 : Timeout (Qed:77ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____5 : Unknown (Qed:19ms) (6s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____6 : Unknown (Qed:12ms) (6s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____4 : Unknown (Qed:19ms) (9s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____7 : Unknown (Qed:17ms) (5s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____8 : Valid (Qed:15ms) (1.3s) (772) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____12 : Valid (Qed:14ms) (105ms) (71) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____9 : Unknown (Qed:27ms) (9s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____10 : Unknown (Qed:24ms) (8s) [wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____14 : Valid (9ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____11 : Unknown (8s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____13 : Unknown (Qed:23ms) (8s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____17 : Timeout (Qed:30ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____16 : Timeout (Qed:21ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____15 : Timeout (Qed:8ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____18 : Timeout (Qed:41ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____21 : Timeout (Qed:3ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____20 : Timeout (Qed:8ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____19 : Timeout (Qed:34ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____22 : Timeout (Qed:25ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____25 : Timeout (Qed:8ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____24 : Timeout (Qed:12ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____23 : Timeout (Qed:22ms) [wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____27 : Valid (17ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____26 : Timeout (Qed:28ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____30 : Timeout (Qed:33ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____29 : Timeout (Qed:16ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____28 : Timeout (Qed:14ms) [wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____34 : Valid [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____33 : Unknown (Qed:5ms) (5s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____35 : Unknown (Qed:12ms) (6s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____31 : Timeout (Qed:38ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____32 : Timeout (Qed:32ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____36 : Timeout (Qed:44ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____37 : Timeout (Qed:54ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____38 : Timeout (Qed:48ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____39 : Timeout (Qed:23ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____40 : Timeout (Qed:37ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____41 : Timeout (Qed:56ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____42 : Timeout (Qed:58ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____43 : Timeout (Qed:42ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____44 : Timeout (Qed:28ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____45 : Timeout (Qed:27ms) [wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____49 : Valid (44ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____46 : Timeout (Qed:49ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____47 : Timeout (Qed:67ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____48 : Timeout (Qed:64ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____50 : Timeout (Qed:91ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____51 : Timeout (Qed:83ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____52 : Timeout (Qed:70ms) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____56 : Valid (Qed:566ms) (193ms) (159) [wp] [Alt-Ergo] Goal typed__ZN6SquareEC1_assert_rte_mem_access : Unknown (1s) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____53 : Timeout (Qed:86ms) [wp] [Alt-Ergo] Goal typed__ZN6SquareEC1_call__ZN9RectangleEC1_pre : Valid (Qed:1ms) (73ms) (35) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____54 : Timeout (Qed:98ms) [wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_call__ZN9RectangleEC1RK9Rectangle_pre : Valid (Qed:2ms) (66ms) (38) [wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_assert_rte_mem_access : Unknown (Qed:3ms) (1s) [wp] [Qed] Goal typed__ZN6SquareED1_assert_rte_mem_access : Valid [wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_call__ZN9RectangleEC1RK9Rectangle____ : Valid (Qed:4ms) (77ms) (40) [wp] [Alt-Ergo] Goal typed__ZN6SquareED1_call__ZN9RectangleED1_pre : Valid (67ms) (35) [wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_call__ZN9RectangleEC1RK9Rectangle_____2 : Valid (Qed:6ms) (92ms) (31) [wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____55 : Timeout (Qed:76ms) [wp] [Qed] Goal typed__ZN9RectangleEC1_assert_rte_mem_access : Valid [wp] [Qed] Goal typed__ZN9RectangleEC1RK9Rectangle_assert_rte_mem_access : Valid [wp] [Alt-Ergo] Goal typed__ZN6SquareEaSRK6Square_call__ZN9RectangleEaSRK9Rectangle____ : Valid (78ms) (29) [wp] [Alt-Ergo] Goal typed__ZN6SquareEaSRK6Square_call__ZN9RectangleEaSRK9Rectangle_pre : Valid (Qed:1ms) (66ms) (38) [wp] [Alt-Ergo] Goal typed__ZN6SquareEaSRK6Square_post : Unknown (Qed:2ms) [wp] [Alt-Ergo] Goal typed__ZN9RectangleEC1RK9Rectangle_assert_rte_mem_access_2 : Valid (61ms) (40) [wp] [Qed] Goal typed__ZN9RectangleED1_assert_rte_mem_access : Valid [wp] [Qed] Goal typed__ZN9RectangleEaSRK9Rectangle_post : Valid (1ms) [wp] [Qed] Goal typed__ZNK6SquareE4area_post : Valid [wp] [Qed] Goal typed__ZNK6SquareE4area_assign : Valid [wp] [Alt-Ergo] Goal typed__ZN9RectangleEC1RK9Rectangle_assert_rte_mem_access_3 : Valid (Qed:3ms) (66ms) (31) [wp] [Qed] Goal typed__ZNK9RectangleE4area_assign : Valid [wp] [Qed] Goal typed_main_assert_rte_mem_access : Valid [wp] [Qed] Goal typed_main_assert_rte_mem_access_2 : Valid [wp] [Qed] Goal typed_main_assert_rte_mem_access_3 : Valid (6ms) [wp] [Qed] Goal typed_main_assert_rte_mem_access_4 : Valid (1ms) [wp] [Alt-Ergo] Goal typed__ZN9RectangleEaSRK9Rectangle_assert_rte_mem_access_2 : Valid (Qed:5ms) (68ms) (30) [wp] [Alt-Ergo] Goal typed__ZN9RectangleEaSRK9Rectangle_assert_rte_mem_access : Valid (Qed:2ms) (72ms) (39) [wp] [Qed] Goal typed_main_assert : Valid (1ms) [wp] [Qed] Goal typed_main_call__ZN6SquareEC1_pre : Valid (1ms) [wp] Proved goals: 43 / 117 Qed: 22 (1ms-566ms) Alt-Ergo: 21 (61ms-1.3s) (772) (interrupted: 56) (unknown: 18) ~/acslplusplus_frama-c/Playground/jochen