~/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
[wp] [Qed] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____5 : Valid (4ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info____ : Unknown (Qed:2ms) (1s)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____2 : Unknown (Qed:2ms) (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:4ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____7 : Timeout (Qed:4ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____8 : Timeout (Qed:2ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____12 : Valid (Qed:10ms) (158ms) (111)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____9 : Timeout (Qed:22ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10 : Timeout (Qed:16ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____11 : Timeout (Qed:9ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____16 : Valid (Qed:19ms) (192ms) (121)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____13 : Timeout (Qed:17ms)
[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_____17 : Valid (Qed:45ms) (208ms) (87)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____18 : Valid (Qed:34ms) (151ms) (83)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____19 : Valid (Qed:35ms) (151ms) (83)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____15 : Timeout (Qed:10ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____20 : Timeout (Qed:26ms)
[wp] [Qed] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____24 : Valid (29ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____22 : Timeout (Qed:65ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____21 : Timeout (Qed:35ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____26 : Valid (Qed:70ms) (63ms) (77)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____28 : Valid (Qed:54ms) (273ms) (106)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____23 : Timeout (Qed:58ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____25 : Timeout (Qed:48ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____27 : Timeout (Qed:53ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____29 : Timeout (Qed:30ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____30 : Timeout (Qed:39ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i___ : Unknown (Qed:3ms) (2s)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____31 : Timeout (Qed:56ms)
[wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____3 : Valid (2ms)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____32 : Timeout (Qed:95ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____2 : Unknown (Qed:14ms) (3s)
[wp] [Alt-Ergo] Goal typed__Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____33 : Timeout (Qed:74ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____5 : Unknown (Qed:19ms) (5s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____6 : Unknown (Qed:22ms) (5s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____4 : Unknown (Qed:15ms) (7s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____7 : Unknown (Qed:19ms) (5s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____8 : Valid (Qed:18ms) (1.3s) (772)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____12 : Valid (Qed:13ms) (115ms) (71)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____9 : Unknown (Qed:18ms) (7s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____10 : Unknown (Qed:26ms) (6s)
[wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____14 : Valid (8ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____11 : Unknown (Qed:19ms) (7s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____13 : Unknown (Qed:16ms) (8s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____16 : Timeout (Qed:9ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____15 : Timeout (Qed:11ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____17 : Timeout (Qed:25ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____18 : Timeout (Qed:34ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____20 : Timeout (Qed:2ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____19 : Timeout (Qed:27ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____21 : Timeout (Qed:20ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____22 : Timeout (Qed:30ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____24 : Timeout (Qed:13ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____23 : Timeout (Qed:21ms)
[wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____27 : Valid (9ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____25 : Timeout (Qed:24ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____26 : Timeout (Qed:29ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____29 : Timeout (Qed:36ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____28 : Timeout (Qed:28ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____30 : Timeout (Qed:37ms)
[wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____34 : Valid (11ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____33 : Unknown (Qed:7ms) (4s)
[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____35 : Unknown (Qed:14ms) (6s)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____32 : Timeout (Qed:39ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____36 : Timeout (Qed:45ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____37 : Timeout (Qed:30ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____38 : Timeout (Qed:50ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____39 : Timeout (Qed:37ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____40 : Timeout (Qed:32ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____41 : Timeout (Qed:55ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____42 : Timeout (Qed:33ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____43 : Timeout (Qed:55ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____44 : Timeout (Qed:55ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____45 : Timeout (Qed:44ms)
[wp] [Qed] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____49 : Valid (40ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____46 : Timeout (Qed:41ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____47 : Timeout (Qed:69ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____48 : Timeout (Qed:50ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____51 : Timeout (Qed:94ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____50 : Timeout (Qed:79ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____52 : Timeout (Qed:88ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____56 : Valid (Qed:507ms) (172ms) (159)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEC1_assert_rte_mem_access : Unknown (1s)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEC1_call__ZN9RectangleEC1_pre : Valid (62ms) (35)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____53 : Timeout (Qed:92ms)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_call__ZN9RectangleEC1RK9Rectangle_pre : Valid (53ms) (38)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_assert_rte_mem_access : Unknown (Qed:4ms) (1s)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_call__ZN9RectangleEC1RK9Rectangle____ : Valid (Qed:2ms) (85ms) (40)
[wp] [Qed] Goal typed__ZN6SquareED1_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed__ZN6SquareEC1RK6Square_call__ZN9RectangleEC1RK9Rectangle_____2 : Valid (83ms) (31)
[wp] [Alt-Ergo] Goal typed__ZN6SquareED1_call__ZN9RectangleED1_pre : Valid (69ms) (35)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____55 : Timeout (Qed:63ms)
[wp] [Alt-Ergo] Goal typed__Z30_frama_c_find_dynamic_cast_auxP28_frama_c_rtti_name_i____54 : Timeout (Qed:84ms)
[wp] [Qed] Goal typed__ZN9RectangleEC1_assert_rte_mem_access : Valid (3ms)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEaSRK6Square_call__ZN9RectangleEaSRK9Rectangle_pre : Valid (Qed:2ms) (81ms) (38)
[wp] [Alt-Ergo] Goal typed__ZN6SquareEaSRK6Square_post : Unknown (Qed:4ms) (1s)
[wp] [Qed] Goal typed__ZN9RectangleEC1RK9Rectangle_assert_rte_mem_access : Valid (2ms)
[wp] [Qed] Goal typed__ZN9RectangleED1_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed__ZN9RectangleEaSRK9Rectangle_post : Valid
[wp] [Alt-Ergo] Goal typed__ZN6SquareEaSRK6Square_call__ZN9RectangleEaSRK9Rectangle____ : Valid (Qed:1ms) (84ms) (29)
[wp] [Alt-Ergo] Goal typed__ZN9RectangleEC1RK9Rectangle_assert_rte_mem_access_3 : Valid (71ms) (31)
[wp] [Alt-Ergo] Goal typed__ZN9RectangleEC1RK9Rectangle_assert_rte_mem_access_2 : Valid (Qed:5ms) (73ms) (40)
[wp] [Qed] Goal typed__ZNK6SquareE4area_post : Valid
[wp] [Qed] Goal typed__ZNK6SquareE4area_assign : Valid
[wp] [Alt-Ergo] Goal typed__ZN9RectangleEaSRK9Rectangle_assert_rte_mem_access : Valid (80ms) (39)
[wp] [Qed] Goal typed__ZNK9RectangleE4area_assign : Valid
[wp] [Qed] Goal typed_main_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed__ZN9RectangleEaSRK9Rectangle_assert_rte_mem_access_2 : Valid (77ms) (30)
[wp] [Qed] Goal typed_main_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_main_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_main_assert_rte_mem_access_4 : Valid (7ms)
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Qed] Goal typed_main_call__ZN6SquareEC1_pre : Valid
[wp] Proved goals:   43 / 117
     Qed:            22  (0ms-507ms)
     Alt-Ergo:       21  (53ms-1.3s) (772) (interrupted: 56) (unknown: 18)

~/acslplusplus_frama-c/Playground/jochen